Investigation on the typing of equality in type systems

Vincent Siles 1, 2, 3
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, INRIA Paris-Rocquencourt, UP7 - Université Paris Diderot - Paris 7, CNRS : UMR7126
Abstract : This dissertation is about the investigation of the concept of conversion that lies within any kind of dependently typed systems. Several presentations of those systems have been studied for various purposes: typing, proof search, logical coherence... Each presentation embeds its own notion of equality, tuned for its own goal. However, the question to know whereas all those representations in fact reflecting the same theory is not yet proved. We will focus here on a quite large family of systems called Pure Type Systems, and we will prove that all of their usual presentations are equivalent, by exhibiting a constructive translation from a representation to the other. All of those translations are based on the behaviour of the equality and the ways to translate them. Therefore, this work will focus on the properties of the equality, and we will prove that it is possible to type any syntactic equality into a semantic one, which is enough to translate any system into another one. Moreover, all of this thesis has been verified and proved correct with the Coq proof assistant, which has also been used during the development of the proofs.
Document type :
Theses
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2010. English


https://pastel.archives-ouvertes.fr/pastel-00556578
Contributor : Vincent Siles <>
Submitted on : Monday, January 17, 2011 - 11:59:25 AM
Last modification on : Friday, January 21, 2011 - 10:33:29 AM

Identifiers

  • HAL Id : pastel-00556578, version 1

Collections

Citation

Vincent Siles. Investigation on the typing of equality in type systems. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2010. English. <pastel-00556578>

Export

Share

Metrics

Consultation de
la notice

214

Téléchargement du document

69