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