Systèmes de types purs et substitutions explicites
Institution:
École normale supérieure (Lyon ; 1987-2009)Disciplines:
Directors:
Abstract EN:
Type theory is currently considered as a fundamental tool in computer science, since it establishes a link between a calculus on the one hand and a logical system on the other hand, which allows to state various properties. Pure type systems are a very general formalism in terms of which many logical systems may be expressed. This thesis presents the extension of those systems in two frameworks: a calculus with explicit substitutions and a classical sequent calculus, and studies the properties of the obtained systems, especially type correction, derivation reconstruction, subject reduction, and strong normalisation. In the first case, a new typing rule is introduced, inspired by type inference considerations, and also a new proof method, relying on an order upon derivations. In the second case, the notion of well-formedness is more particularly studied, and one also considers perpetual reorganisations of reduction paths
Abstract FR:
La théorie des types est actuellement considérée comme un outil fondamental en informatique, car elle établit un lien entre un calcul d'une part et un système logique d'autre part, ce qui permet d'exprimer des propriétés variées. Les systèmes de types purs sont un formalisme général dans lequel on peut définir un grand nombre de systèmes logiques. Cette thèse présente l'extension de ces systèmes dans deux cadres : un calcul à substitutions explicites et un calcul de séquents classique, et étudie les propriétés des systèmes obtenus, en particulier la correction des types, la reconstruction de dérivations, la réduction du sujet et la normalisation forte. Dans le premier cas, on introduit une nouvelle règle d'inférence de type inspirée de la synthèse de type et une nouvelle technique de démonstration avec un ordre sur les dérivations. Dans le second cas, on étudie en particulier la notion de bonne formation et l'on s'intéresse à des réorganisations perpétuelles de chemin de réduction.