Small induction recursion

DOI10.1007/978-3-642-38946-7_13MaRDI QIDQ5300900zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch

Publication date 28 June 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38946-7_13

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Positive inductive-recursive definitions
• Positive inductive-recursive definitions
• Containers, monads and induction recursion
• Fibred data types
• Induction-recursion and initial algebras.

Cited in

(15)

• Constructing a universe for the setoid model
• Positive inductive-recursive definitions
• Turing-Completeness Totally Free
• How to reason coinductively informally
• scientific article; zbMATH DE number 1371691 (Why is no real title available?)
• Cubical syntax for reflection-free extensional equality
• Positive inductive-recursive definitions
• Fibred data types
• Indexed containers
• Interactive programming in Agda -- objects and graphical user interfaces
• Containers, monads and induction recursion
• Subtyping without reduction
• Impredicative encodings of inductive-inductive data in Cedille
• ``Upon this quote I will build my Church thesis
• Broad infinity and generation principles

This page was built for publication: Small induction recursion

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