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
Liste complète des métadonnées

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00496988
Contributor : Vincent Siles <>
Submitted on : Friday, July 2, 2010 - 10:36:24 AM
Last modification on : Thursday, April 4, 2019 - 1:15:48 AM
Document(s) archivé(s) le : Tuesday, October 23, 2012 - 9:36:18 AM

File

herbelin.siles.LICS2010.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00496988, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

250

Files downloads

123