Krivine Machine Can someone please point out online resources to learn about Krivine Machine?
My professor briefly touched it while teaching a course in Computer logic. google did not turn up much except some papers which seemed hard to follow. Neither was there anything on it over at Wikipedia.
 A: The Krivine machine (or K-machine) [1] is a simple and natural
implementation of the weak-head call-by-name reduction strategy for
pure λ-terms. It can be described in just three or four rules with
minimal machinery (an environment and a stack).  It is an
abstract machines for the implementation of functional languages.
It has been used in many variants. The paper [2] gives an overview
of the Krivine-machine variants. 
[1] A call-by-name lambda-calculus machine, J.-L. Krivine.
[2] The Next 700 Krivine Machines, R. Douence, P. Fradet.
A: I found this paper that explains the Krivine machine and relates it with the call-by-name lambda calculus:
Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano, "A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language", http://drops.dagstuhl.de/opus/volltexte/2014/4634/pdf/13.pdf
It defines a call-by-name lambda calculus of closures and then briefly describes the Krivine machine, that appears natural once you understand the calculus of closures. I found it readable and it can complement the very succint description of the Krivine machine in the slides proposed by Ankit. Note that it supposes that you already know what De Bruijn indices are. However the Krivine machine by itself is not very useful, since most programming languages have not call-by-name semantics (Algol 60 was one, and was deemed unusable exactly for this reason). You may therefore want to study the version of the Krivine machine for strict or lazy semantics. The paper above also discusses a Krivine machine for call-by-name with numbers and operations. For strict semantics the typical variant is the Krivine machine with marks on the stack; You can find a description of it at section 3.2 of the ZINC paper:
Xavier Leroy, "The ZINC experiment: An economical implementation of the ML language", http://gallium.inria.fr/~xleroy/publi/ZINC.pdf
A: The original paper by Jean-Louis Krivine that describes the machine can be found here (PDF):A call-by-name lambda-calculus machine.
