29/04/2004
Sylvain Lippi (IML)
Une implantation d'une machine de Krivine

La machine de Krivine est habituellement présentée comme une machine à environnement permettant d'exécuter des lambda-termes écrits en notation de De Bruijn. Nous donnons une version « naïve » (mais correcte !) de cette machine sans utiliser les indices de De Bruijn. Nous la codons ensuite dans les réseaux d'interaction; on obtient ainsi une machine de Krivine graphique avec glaneur de cellules intégré que nous comparons avec d'autres codages connus. Nous terminons par une implantation efficace directement dérivée de cette machine de Krivine graphique.