Impredicative encodings of inductive-inductive data in Cedille
From MaRDI portal
Publication:6535795
DOI10.1007/978-3-031-38938-2_1zbMATH Open1547.68104MaRDI QIDQ6535795FDOQ6535795
Authors: Andrew Marmaduke, Larry Diehl, Aaron Stump 
Publication date: 28 February 2024
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
- Innovations in computational type theory using Nuprl
- Inductive-inductive definitions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Induction-recursion and initial algebras.
- Title not available (Why is that?)
- Quotient inductive-inductive types
- The calculus of dependent lambda eliminations
- Efficient Mendler-style lambda-encodings in Cedille
- Syntax and semantics of quantitative type theory
- Indexed induction-recursion
- Positive inductive-recursive definitions
- Small induction recursion
- For Finitary Induction-Induction, Induction is Enough
- From realizability to induction via dependent intersection
- Title not available (Why is that?)
- A categorical semantics for inductive-inductive definitions
- A finite axiomatisation of inductive-inductive definitions
- Quotients by idempotent functions in Cedille
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)
