A relationally parametric model of dependent type theory

DOI10.1145/2535838.2535852zbMath1284.68163OpenAlexW2042204873MaRDI QIDQ5408445

Neil Ghani, Robert Atkey, 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

zbMATH Keywords

relational parametricitydependent type theory

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (14)

From realizability to induction via dependent intersection ⋮ Proof-Relevant Parametricity ⋮ Unnamed Item ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ The calculus of dependent lambda eliminations ⋮ Unnamed Item ⋮ A presheaf model of parametric type theory ⋮ Unnamed Item ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Graded modal dependent type theory ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory ⋮ Pointers in Recursion: Exploring the Tropics ⋮ Towards a Cubical Type Theory without an Interval

This page was built for publication: A relationally parametric model of dependent type theory