A presheaf model of parametric type theory

DOI10.1016/j.entcs.2015.12.006zbMath1351.68146OpenAlexW2148275052WikidataQ113317736 ScholiaQ113317736MaRDI QIDQ5971392

Guilhem Moulin, Thierry Coquand, Jean-Philippe Bernardy

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.006

zbMATH Keywords

type theoryparametricitypresheaf semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Related Items (11)

Proof-Relevant Parametricity ⋮ Unnamed Item ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Comprehensive Parametric Polymorphism: Categorical Models and Type Theory ⋮ Unnamed Item ⋮ Towards a Cubical Type Theory without an Interval ⋮ Unnamed Item ⋮ Syntax and models of Cartesian cubical type theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs for free
• Nominal Sets
• A Computational Interpretation of Parametricity
• Realizability and Parametricity in Pure Type Systems
• Parametricity and dependent types
• Nameless, painless
• Parametric higher-order abstract syntax for mechanized semantics
• Type-theory in color
• A relationally parametric model of dependent type theory

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