Ce mémoire présente l'implémentation d'un nouveau langage de programmation nommé Typer. Typer est un langage fonctionnel orienté vers la méta programmation. Il a été conçu pour augmenter la productivité du programmeur et lui permettre d'écrire des applications plus fiables grâce à son système de types. Pour arriver à ses fins, Typer utilise l'inférence de types et implémente un puissant système de macros. L'inférence de types permet à l'utilisateur d'omettre certains éléments, le système de macros, quant à lui, permet de compléter le programme pendant la compilation lorsque l'inférence n'est pas suffisante ou pour générer du code. Typer utilise les types dépendants pour permettre à l'utilisateur de créer des types très expressifs pouvant même être utilisés pour représenter des preuves formelles. De plus, l'expressivité des types dépendants permet au compilateur d'effectuer des vérifications plus approfondies pendant la compilation même. Ces mécaniques permettent au code source d'être moins verbeux, plus concis et plus simple à comprendre, rendant, ainsi l'écriture de programmes ou/et de preuves plus plaisante. Ces fonctionnalités sont implémentées dans l'étape que nous appelons l'élaboration, à l'intérieur de laquelle de nombreuses transformations du code source ont lieu. Ces transformations incluent l'élimination des aides syntaxiques, la résolution des identificateurs, l'expansion des macros, la propagation et l'inférence des types. / This dissertation present the implementation of a new programming language named Typer Typer is a functional programming language oriented towards meta programming. It has been created to increase the programmer productivity and enable him to write safer programs thanks to his type system. To achieve his goal, Typer use type inference and a powerful macro system. Type inference enable to user to elide some elements while the macro system enable us to complete the program during compilation. Typer use dependent type which enable the user to create very expressive types which can even be used to represent formal proofs. Furthermore, dependent type's expressivity enable the compiler to perform a in-depth checks during compilation. Those mechanics enable the source code to be less verbose, shorter and easier to understand, making the writing of new programmes more enjoyable. Those functionalities are implemented during the step we call the elaboration in which numerous transformations occur. Those transformations include the removal of syntactic sugar, identifier resolution, macro expansion and the propagation and the inference of types.

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.