Skip to Main content Skip to Navigation
Conference papers

Equality is typable in Semi-Full Pure Type Systems

Vincent Siles 1, 2, 3 Hugo Herbelin 1, 2 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed judgement of beta-equality directly in the typing system. After being an open problem for some time, the general equivalence between both approaches has been solved by Adams for a class of pure type systems (PTSs) called functional. In this paper, we relax the functionality constraint and prove the equivalence for all semi-full PTSs by combining the ideas of Adams with a study of the general shape of types in PTSs. As one application, an extension of this result to systems with sub-typing would be a first step toward bringing closer the theory behind a proof assistant such as Coq to its implementation.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Vincent Siles Connect in order to contact the contributor
Submitted on : Friday, July 2, 2010 - 10:36:24 AM
Last modification on : Friday, January 21, 2022 - 3:22:25 AM
Long-term archiving on: : Tuesday, October 23, 2012 - 9:36:18 AM


Files produced by the author(s)


  • HAL Id : inria-00496988, version 1



Vincent Siles, Hugo Herbelin. Equality is typable in Semi-Full Pure Type Systems. Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p. ⟨inria-00496988⟩



Record views


Files downloads