Explaining the lazy Krivine machine using explicit substitution and addresses

Frederic Lang 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : In a previous paper, Benaissa, Lescanne, and Rose, have extended the weak lambda-calculus of explicit substitution lambda-sigma-w with addresses, so that it gives an account of the sharing implemented by lazy functional language interpreters. We show in this paper that their calculus, called lambda-sigma-w-a, fits well to the lazy Krivine machine, which describes the core of a lazy (call-by-need) functional programming language implementation. The lazy Krivine machine implements term evaluation sharing, that is essential for efficiency of such languages. The originality of our proof is that it gives a very detailed account of the implemented strategy.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2007
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00198756
Contributeur : Frederic Lang <>
Soumis le : lundi 17 décembre 2007 - 18:54:55
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 12 avril 2010 - 08:14:47

Fichier

Lang-07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00198756, version 1

Collections

Citation

Frederic Lang. Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation, Springer Verlag, 2007. 〈inria-00198756〉

Partager

Métriques

Consultations de la notice

585

Téléchargements de fichiers

236