Positive inductive-recursive definitions

DOI10.1007/978-3-642-40206-7_3MaRDI QIDQ2848936zbMATH OpenOpenAlexFDO

Authors Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg

Publication date 13 September 2013

Published in Algebra and Coalgebra in Computer Science (Search for Journal in Brave)

Full work available at URL https://strathprints.strath.ac.uk/52999/

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)

Recommendations

• Positive inductive-recursive definitions
• Variations on inductive-recursive definitions
• Small induction recursion
• Induction-recursion and initial algebras.
• scientific article; zbMATH DE number 2006633

Cited in

(12)

• Finitary higher inductive types in the groupoid model
• A categorical semantics for inductive-inductive definitions
• Small induction recursion
• Constructing a universe for the setoid model
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• Indexed induction-recursion
• Indexed containers
• Fibred data types
• Positive inductive-recursive definitions
• Variations on inductive-recursive definitions
• Impredicative encodings of inductive-inductive data in Cedille
• For Finitary Induction-Induction, Induction is Enough

This page was built for publication: Positive inductive-recursive definitions

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