On the correctness of the Krivine machine

Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991) Summary in ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, 1990 Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. In: Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 8–19 (2003) Crégut, P.: An abstract machine for the normalization of λ-terms. In: Proc. 1990 ACM Symposium on Lisp and Functional Programming, pp. 333–340 (1990) Hannan, J., Miller, D.: From operational semantics to abstract machines: preliminary results. In: Proc. 1990 ACM Symposium on Lisp and Functional Programming, pp. 323–332 (1990) Krivine, J.-L.: Un interpréteur du lambda-calcul. Unpublished note, at http://www.pps.jussieu.fr/~krivine/articles/interprt.pdf (1985) Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA (1991) Randell, B., Russell, L.J.: Algol 60 Implementation. Academic, New York (1964) Streicher, T., Reus, B.: Classical logic, continutation semantics and abstract machines. J. Funct. Program. 8(6), 543–572 (1998)