Strongly reducing variants of the Krivine abstract machine

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. This article is an extended version of a paper presented at the ‘Lisp and Functional Programming’ Conference in 1990 and the work was done at Ecole Normale Supérieure between 1989 and 1991.