Equality Is Typable in Semi-full Pure Type Systems

—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.

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Vincent Siles, Hugo Herbelin
• Keywords: Automated Reasoning, LICS 2010, PTSs, Pure Type Systems, Semi-full Ptss