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