A relationally parametric model of dependent type theory
DOI10.1145/2535838.2535852zbMATH Open1284.68163OpenAlexW2042204873MaRDI QIDQ5408445FDOQ5408445
Authors: Robert Atkey, Neil Ghani, Patricia Johann 
Publication date: 10 April 2014
Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)
Full work available at URL: http://libres.uncg.edu/ir/asu/f/Johann_Patricia_2014_A_Relationally_Parametric_Model_Of_Dependent_Type_Theory..pdf
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Cited In (32)
- Models for polymorphism over physical dimension
- Transpension: the right adjoint to the Pi-type
- Relational parametricity for higher kinds
- Title not available (Why is that?)
- Graded modal dependent type theory
- Abstraction and invariance for algebraically indexed types
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Title not available (Why is that?)
- 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
- GADTs, functoriality, parametricity: pick two
- A syntax for higher inductive-inductive types
- Parametricity and dependent types
- Parametricity in an impredicative sort
- Title not available (Why is that?)
- 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
- A presheaf model of parametric type theory
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)
