Indexed induction-recursion

DOI10.1016/J.JLAP.2005.07.001MaRDI QIDQ2577476zbMATH OpenOpenAlexFDO

Authors Peter Dybjer, Anton Setzer

Publication date 22 December 2005

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2005.07.001

zbMATH Keywords

dependent type theorygeneric programminginductive definitionsinductive familiesinductive-recursive definitionsinitial algebrasMartin-Löf type theorynormalisation proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Inductive definability (03D70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2006633
• Positive inductive-recursive definitions
• Induction-recursion and initial algebras.
• scientific article; zbMATH DE number 1342277
• Positive inductive-recursive definitions

Cites work

• A general formulation of simultaneous inductive-recursive definitions in type theory
• Constructive mathematics and computer programming
• Extending Martin-Löf type theory by one Mahlo-universe
• Generic Programming
• scientific article; zbMATH DE number 1696616 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3722625 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 1302063 (Why is no real title available?)
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 2006633 (Why is no real title available?)
• scientific article; zbMATH DE number 1863381 (Why is no real title available?)
• scientific article; zbMATH DE number 2100542 (Why is no real title available?)
• scientific article; zbMATH DE number 2111733 (Why is no real title available?)
• scientific article; zbMATH DE number 1424014 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Induction-recursion and initial algebras.
• Inductive families
• Proof theory of Martin-Löf type theory. An overview

Cited in

(19)

• Finitary higher inductive types in the groupoid model
• Continuous functions on final coalgebras
• A Brief Overview of Agda – A Functional Language with Dependent Types
• How to reason coinductively informally
• Hoare type theory, polymorphism and separation
• Inductive-inductive definitions
• scientific article; zbMATH DE number 2006633 (Why is no real title available?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Variations on inductive-recursive definitions
• Dependent Types at Work
• Program testing and the meaning explanations of intuitionistic type theory
• Coalgebras as types determined by their elimination rules
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Indexed containers
• Containers, monads and induction recursion
• Impredicative encodings of inductive-inductive data in Cedille
• A syntax for mutual inductive families
• Interpretation of inaccessible sets in Martin-Löf type theory with one Mahlo universe
• Broad infinity and generation principles

Describes a project that uses

Uses Software

• ALF
• Polyp
• Agda

This page was built for publication: Indexed induction-recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2577476)