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

Cette thèse porte sur l'adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d'un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

Cette thèse porte sur l’adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d’un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques. / This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics.