Investigation on the typing of equality in type systems
Etude sur le typage de l'égalité dans les systèmes de types
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.
Le travail présenté dans cette thèse concerne l'étude de la notion de conversion inhérente à tous système de types dépendants. Plusieurs présentations de ces systèmes ont été étudiées pour des usages variés: typage, recherche de preuve, cohérence de logique... Chacune de ces représentation est accompagnée d'une notion d'égalité différente, suivant les besoins du moment. Mais il n'est pas certains que toutes ces représentations parlent en fin de compte d'une seule et même logique. Nous nous intéressons ici à une famille assez conséquente de systèmes de types, appelés Systèmes de Types Purs, et nous allons prouver que pour ces systèmes, toutes les représentations habituellement utilisées sont en fait équivalentes, c'est à dire qu'il existe des traductions constructives entre chacune de ces présentations. Ces traductions reposent toutes sur la manière de porter une égalité d'un système à l'autre. Ce travail se concentre donc sur les mécanismes de ces égalités, et prouve qu'il est possible de typer n'importe quelle égalité syntaxique en égalité sémantique, et ainsi qu'il est donc possible de passer d'un système à l'autre. L'intégralité de cette thèse a en outre été vérifiée et certifiée correcte à l'aide de l'assistant à la preuve Coq, qui a activement été utilisé tout au long de l'élaboration des preuves. ~
Loading...