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 (24)
- Transpension: the right adjoint to the Pi-type
- Relational parametricity for higher kinds
- Title not available (Why is that?)
- Graded modal dependent type theory
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Title not available (Why is that?)
- From realizability to induction via dependent intersection
- A Syntax for Higher Inductive-Inductive Types
- Title not available (Why is that?)
- Extensional and Intensional Semantic Universes
- The calculus of dependent lambda eliminations
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- On generically stable types in dependent theories
- Relational and Kleene-Algebraic Methods in Computer Science
- Computer Science Logic
- Proofs for free. Parametricity for dependent types
- Proof-Relevant Parametricity
- GADTs, functoriality, parametricity: pick two
- Towards a Cubical Type Theory without an Interval
- Parametricity in an impredicative sort
- Title not available (Why is that?)
- For Finitary Induction-Induction, Induction is Enough
- 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)
