Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy to a two-level type theory.

Mon 14 Jan

CPP-2019
11:00 - 12:30: CPP 2019 - Research Papers: Proof Theory, Theory of Programming Languages at Sala XII
Chair(s): Assia MahboubiINRIA
CPP-201911:00 - 11:30
Research paper
Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MilerINRIA Saclay and LIX
DOI
CPP-201911:30 - 12:00
Research paper
Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, Germany
DOI
CPP-201912:00 - 12:30
Research paper
Theo WinterhalterGallinette / Inria / LS2N, Nicolas TabareauInria, Matthieu SozeauInria
DOI