Impredicative encodings of inductive-inductive data in Cedille

DOI10.1007/978-3-031-38938-2_1MaRDI QIDQ6535795zbMATH OpenFDO

Authors Andrew Marmaduke, Larry Diehl, Aaron Stump

Publication date 28 February 2024

Full work available at URL https://doi.org/10.1007/978-3-031-38938-2_1

zbMATH Keywords

Cedilleimpredicative encodinginduction-induction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Efficient Mendler-style lambda-encodings in Cedille
• Impredicative encodings of (higher) inductive types
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• A categorical semantics for inductive-inductive definitions
• Monotone recursive types and recursive data representations in Cedille

Cites work

• A categorical semantics for inductive-inductive definitions
• A finite axiomatisation of inductive-inductive definitions
• Efficient Mendler-style lambda-encodings in Cedille
• For Finitary Induction-Induction, Induction is Enough
• From realizability to induction via dependent intersection
• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• scientific article; zbMATH DE number 1722663 (Why is no real title available?)
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• scientific article; zbMATH DE number 1354162 (Why is no real title available?)
• Indexed induction-recursion
• Induction-recursion and initial algebras.
• Inductive-inductive definitions
• Innovations in computational type theory using Nuprl
• Positive inductive-recursive definitions
• Quotient inductive-inductive types
• Quotients by idempotent functions in Cedille
• Small induction recursion
• Syntax and semantics of quantitative type theory
• The calculus of dependent lambda eliminations

This page was built for publication: Impredicative encodings of inductive-inductive data in Cedille

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