Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Frederic Lang Connect in order to contact the contributor
Submitted on : Monday, December 17, 2007 - 6:54:55 PM
Last modification on : Wednesday, July 6, 2022 - 4:24:00 AM
Long-term archiving on: : Monday, April 12, 2010 - 8:14:47 AM


Files produced by the author(s)


  • HAL Id : inria-00198756, version 1



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



Record views


Files downloads