Indexed induction-recursion

DOI10.1016/j.jlap.2005.07.001zbMath1080.68014OpenAlexW2132221175MaRDI QIDQ2577476

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

Martin-Löf type theoryinitial algebrasdependent type theoryinductive definitionsgeneric programminginductive-recursive definitionsinductive familiesnormalisation proofs

Mathematics Subject Classification ID

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

Related Items (12)

Finitary higher inductive types in the groupoid model ⋮ A Brief Overview of Agda – A Functional Language with Dependent Types ⋮ Indexed containers ⋮ Hoare type theory, polymorphism and separation ⋮ How to Reason Coinductively Informally ⋮ Containers, monads and induction recursion ⋮ Dependent Types at Work ⋮ Continuous Functions on Final Coalgebras ⋮ Variations on inductive-recursive definitions ⋮ 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

Uses Software

• ALF
• Polyp
• Agda

Cites Work

• Inductive families
• Induction-recursion and initial algebras.
• Extending Martin-Löf type theory by one Mahlo-universe
• Constructive mathematics and computer programming
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Generic Programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Indexed induction-recursion