Chapitre 3  Typage d'un mini-ML

Un compilateur ML se décompose de manière classique en : On se propose dans cette section de définir la syntaxe abstraite d'un langage appelé mini-ML, qui est un sous-ensemble de Caml-light et de montrer son mécanisme de typage, qui à des simplifications près est celui de Caml-light. Mini-ML correspond au noyau fonctionnel de Caml-light sans le filtrage. Il ne contient ni exceptions ni traits impératifs. Cette dernière restriction simplifie le vérificateur de types sans en changer la nature profonde. L'algorithme d'unification est assez différent de celui déjà vu pour le typage du l-calcul car il appliquera directement, en faisant une modification physiques sur les types, les substitutions de variables de type. Le programme de vérification de types s'inspire des deux exemples de Michel Mauny que l'on peut lire dans la présentation d'une ``spécification CAML d'un sous-ensemble de CAML'' et du langage ASL de la documentation Caml-light (voir bibliographie).

Chapitre 4  Typage des traits impératifs


Ce document a été traduit de LATEX par HEVEA et HACHA.