In recent years, dependent type systems have gathered interest because they make it possible to express stronger properties about programs. However, they are also very verbose. In this thesis, we show how to eliminate some of this verbosity (for the user) by doing reconstruction over dependent types. More precisely, we present the work done in the implementation of the Beluga programming language. Our goal is to present the key issues arising in reconstruction and give a formal and accessible description of ideas that have been around for some time but never given the spotlight. We also prove the soundness of our reconstruction algorithm. / Au cours des dernières années, les types dépendants ont reçu un intérêt particulier parce qu'ils permettent d'exprimer des propriétés plus précises sur les programmes. Cependant, ces systèmes de typage sont aussi très redondants. Dans cette thèse, nous allons expliquer comment éliminer une partie de cette redondance en reconstruisant ces types dépendants. Plus précisément, nous présenterons le travail fait sur l'implémentation du langage Beluga. Notre but est de présenter les problématiques importantes liées à la reconstruction de types dépendants et de présenter de façon formelle et accessible certaines idées qui, malgré le fait qu'elle ne sont pas toutes récentes, sont toujours restées dans l'ombre jusqu'à maintenant. Une preuve de correction de notre algorithme de reconstruction est aussi donnée.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QMM.92350 |
| Date | January 2010 |
| Creators | Germain, Renaud |
| Contributors | Brigitte Pientka (Internal/Supervisor) |
| Publisher | McGill University |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Coverage | Master of Science (School of Computer Science) |
| Rights | All items in eScholarship@McGill are protected by copyright with all rights reserved unless otherwise indicated. |
| Relation | Electronically-submitted theses. |
Page generated in 0.0021 seconds