Développement : Algorithme de type principal

Détails/Enoncé :

Algorithme de typage du lambda calcul à la Curry, qui teste la typabilité d'un $\lambda$-terme, et construit un type principal si il existe.

Auteur :
sieghttct
Remarque :
Le programme ne parle que de $\lambda$-calcul pur, ça peut donc paraître étonnant de mettre du typage ici. Néanmoins, le typage d'un terme est une méthode efficace pour prouver qu'il est (fortement) normalisant ! C'est l'intérêt du théorème rappelé en début de développement.
Pour la leçon 923, le rapport 2017 rappelle aussi qu'on peut introduire des bouts d'analyse sémantique, cet algo y trouve donc aussi toute sa place.
Références :
- Lectures on the Curry-Howard Isomorphism, M. H. Sørensen, P. Urzyczyn
- Term rewriting and All That, Franz Baader
Fichier :
- di5.pdf