Récursion généralisée et inférence de types avec intersection

Dans une première partie, nous définissons un nouveau langage à base fonctionnelle et avec récursion généralisée, en utilisant le système de types avec degrés de Boudol pour éliminer les récursions dangereuses. Ce langage est ensuite étendu par des enregistrements récursifs, puis par des mixins, per...

Full description

Bibliographic Details
Main Author: ZIMMER, Pascal
Language:FRE
Published: Université de Nice Sophia-Antipolis 2004
Subjects:
ML
Online Access:http://tel.archives-ouvertes.fr/tel-00006314
http://tel.archives-ouvertes.fr/docs/00/04/68/94/PDF/tel-00006314.pdf
http://tel.archives-ouvertes.fr/docs/00/04/68/94/ANNEX/tel-00006314.pdf
Description
Summary:Dans une première partie, nous définissons un nouveau langage à base fonctionnelle et avec récursion généralisée, en utilisant le système de types avec degrés de Boudol pour éliminer les récursions dangereuses. Ce langage est ensuite étendu par des enregistrements récursifs, puis par des mixins, permettant ainsi de mêler totalement les paradigmes fonctionnels et objets. Nous présentons également une implémentation, MlObj, ainsi que la machine abstraite servant à son exécution.<br /><br />Dans une deuxième partie, nous présentons un nouvel algorithme d'inférence pour les systèmes de types avec intersection, dans le cadre d'une extension du lambda-calcul. Après avoir prouvé sa correction, nous étudions sa généralisation aux références et à la récursion, nous le comparons aux algorithmes d'inférence déjà existants, notamment à celui de Système I, et nous montrons qu'il devient décidable à rang fini.