À compter du 6 février, nous devrons procéder à une interruption temporaire du dépôt de documents dans Papyrus, y compris les thèses et mémoires, le temps d’effectuer une migration de la plateforme vers le service de dépôt institutionnel canadien Scholaris. Le jeudi 6 février, le site sera inaccessible à partir de 7h00 et il sera de retour en fin d’après-midi. Par la suite, tout le contenu de Papyrus sera accessible durant les travaux qui devraient durer environ deux semaines. Pour toute question, contactez depot@bib.umontreal.ca -------- As of February 6, we will be temporarily suspending the deposit of documents in Papyrus, including theses and dissertations, while we migrate the platform to the Canadian institutional deposit service Scholaris. On Thursday February 6, the site will be inaccessible from 7:00 a.m. until late afternoon. Afterwards, all Papyrus content will be accessible during the work, which is expected to last around two weeks. If you have any questions, please contact depot@bib.umontreal.ca
Typer a de la classe : le polymorphisme ad hoc dans un langage avec des types dépendants et de la métaprogrammation
dc.contributor.advisor | Monnier, Stefan | |
dc.contributor.author | Barszcz, Jean-Alexandre | |
dc.date.accessioned | 2022-01-24T20:46:22Z | |
dc.date.available | NO_RESTRICTION | fr |
dc.date.available | 2022-01-24T20:46:22Z | |
dc.date.issued | 2021-10-21 | |
dc.date.submitted | 2021-05 | |
dc.identifier.uri | http://hdl.handle.net/1866/26064 | |
dc.subject | polymorphisme ad hoc | fr |
dc.subject | classes de types | fr |
dc.subject | types dépendants | fr |
dc.subject | métaprogrammation | fr |
dc.subject | ad hoc polymorphism | fr |
dc.subject | type classes | fr |
dc.subject | dependent types | fr |
dc.subject | metaprogramming | fr |
dc.subject.other | Applied Sciences - Computer Science / Sciences appliqués et technologie - Informatique (UMI : 0984) | fr |
dc.title | Typer a de la classe : le polymorphisme ad hoc dans un langage avec des types dépendants et de la métaprogrammation | fr |
dc.type | Thèse ou mémoire / Thesis or Dissertation | |
etd.degree.discipline | Informatique | fr |
etd.degree.grantor | Université de Montréal | fr |
etd.degree.level | Maîtrise / Master's | fr |
etd.degree.name | M. Sc. | fr |
dcterms.abstract | La modularité est un enjeu important en programmation, surtout quand on l’enrichit avec des preuves, comme dans les langages avec des types dépendants. Typer est un tel langage, et afin d’augmenter sa modularité et de lui ajouter un moyen de faire la surcharge d’opérateurs, on s’inspire d’Agda et Coq et on l’étend avec les arguments instances, qui généralisent les classes de types de Haskell. Un aspect qui distingue notre conception est que comme Typer généralise les définitions, la généralisation des contraintes de classe est grandement facilitée. Pour pouvoir faire les preuves de lois de classes, on doit également ajouter l’élimination dépendante des types inductifs au langage, dont certains aspects sont en retour facilités par les arguments instances. Sur la base de ces deux fonctionnalités, on offre également une solution au problème de la cécité booléenne, tel que décrit par Harper. | fr |
dcterms.abstract | Modularity is an important concern for software development, especially when the latter is enriched with proofs in a language with dependent types. Typer is such a language, and in order to increase its modularity, and also provide a way to overload operators, we take inspiration from Agda and Coq and extend it with instance arguments, a generalization of Haskell’s type classes. An aspect that sets our design apart is that since Typer generalizes definitions, it greatly simplifies the generalization of class constraints. In order to allow writing proofs for class laws, we must also implement the dependent elimination of inductive types. In return, instance arguments facilitate some details of dependent elimination. Using both features, we suggest a solution to the problem of Boolean Blindness. | fr |
dcterms.language | fra | fr |
Fichier·s constituant ce document
Ce document figure dans la ou les collections suivantes
Ce document diffusé sur Papyrus est la propriété exclusive des titulaires des droits d'auteur et est protégé par la Loi sur le droit d'auteur (L.R.C. (1985), ch. C-42). Il peut être utilisé dans le cadre d'une utilisation équitable et non commerciale, à des fins d'étude privée ou de recherche, de critique ou de compte-rendu comme le prévoit la Loi. Pour toute autre utilisation, une autorisation écrite des titulaires des droits d'auteur sera nécessaire.