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.
| Identifer | oai:union.ndltd.org:umontreal.ca/oai:papyrus.bib.umontreal.ca:1866/19108 |
| Date | 03 1900 |
| Creators | Delaunay, Pierre |
| Contributors | Monnier, Stefan |
| Source Sets | Université de Montréal |
| Language | French |
| Detected Language | French |
| Type | Thèse ou Mémoire numérique / Electronic Thesis or Dissertation |
Page generated in 0.0065 seconds