Preuves, Types et Sous-types

This thesis is about the theoretical and practical study of a type system applied to functionnal programming certification. The base system is system ST invented by C.Raffalli; this system embeds polymorphism, subtyping and omission of non-algorithmic content. We firstly study models of this theory defined by the type system, building an axiomatic basis based on lattices that allows to express both calculus and logic. On this base, we study the type system itself, prove subject reduction, and the possibility of defining inside the system normalisability and reducibility properties. In the continuation, more applied, we study encoding of rich datatypes inspired from functionnal languages -including first-order modules- into Lambda-Calculus, and show that they behave well in the system through an embedding. The methodology of this part allows to extend the language preserving a consistency criterion ensuring the safety of the typed code.Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé