Impredicative encodings of inductive-inductive data in Cedille
From MaRDI portal
Publication:6535795
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
- 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?)
- 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
- 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)
