Higher-Order and Symbolic Computation

We present a particularly simple lazy lambda-calculus machine, which was introduced twenty-five years ago. It has been, since, used and implemented by several authors, but remained unpublished. We also build an extension, with a control instruction and ...

We present two variants of the Krivine abstract machine that reduce lambda-terms to full normal form. We give a proof of their correctness by interpreting their behaviour in the -calculus.

We provide a short proof of the correctness of the Krivine machine by showing how it simulates weak head reduction.

The Krivine machine is a simple and natural implementation of the normal weak-head reduction strategy for pure -terms. While its original description has remained unpublished, this machine has served as a basis for many variants, extensions and ...

In a previous paper, Benaissa, Lescanne, and Rose, have extended the weak lambda-calculus of explicit substitution _w with addresses, so that it gives an account of the sharing implemented by lazy functional language interpreters. We show in ...

Krivine presents the $\mathcal {K}$ machine, which produces weak head normal form results. Sestoft introduces several call-by-need variants of the ${\mathcal {K}}$ machine that implement result sharing via pushing update markers on the stack in a way similar to the TIM and the STG ...

We present a natural implementation of the Krivine machine in interaction nets: one rule for each transition and the usual rules for duplication and erasing. There is only one rule devoted to the so-called administration. This way, we obtain a graphical ...

The process of compiler generation from lambda-calculus definitions is studied. The compiling schemes developed utilize as their object language the set of state transition machines ( STMs ): automata-like transition sets using first-order ...

History and context are given regarding the development of the WNF-machine, the first example of a Krivine machine.