A relationally parametric model of dependent type theory
From MaRDI portal
Publication:5408445
Recommendations
- Relational parametricity for higher kinds
- A general framework for relational parametricity
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- Proofs for free. Parametricity for dependent types
- Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
Cited in
(32)- A presheaf model of parametric type theory
- Models for polymorphism over physical dimension
- Transpension: the right adjoint to the Pi-type
- Relational parametricity for higher kinds
- scientific article; zbMATH DE number 7779294 (Why is no real title available?)
- Graded modal dependent type theory
- Abstraction and invariance for algebraically indexed types
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- Universal properties for universal types in bifibrational parametricity
- Towards a cubical type theory without an interval
- From realizability to induction via dependent intersection
- A general framework for relational parametricity
- Extensional and Intensional Semantic Universes
- The calculus of dependent lambda eliminations
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- Relational parametricity and quotient preservation for modular (co)datatypes
- On generically stable types in dependent theories
- Relational and Kleene-Algebraic Methods in Computer Science
- Internalizing relational parametricity in the extensional calculus of constructions
- Computer Science Logic
- Proofs for free. Parametricity for dependent types
- Proof-Relevant Parametricity
- Internal parametricity for cubical type theory
- A syntax for higher inductive-inductive types
- GADTs, functoriality, parametricity: pick two
- Parametricity and dependent types
- Parametricity in an impredicative sort
- scientific article; zbMATH DE number 2087549 (Why is no real title available?)
- For Finitary Induction-Induction, Induction is Enough
- Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
- Pointers in Recursion: Exploring the Tropics
This page was built for publication: A relationally parametric model of dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408445)
