Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
Álvaro García-Pérez, Pablo Nogueira, Juan José Moreno-Navarro · 2013
We derive by program transformation Pierre Crégut's full-reducing Krivine machine KN from the structural operational semantics of the normal order reduction strategy in a closure-converted pure lambda calculus. We thus establish the correspondence between the strategy and the machine, and showcase our technique for deriving full-reducing abstract machines. Actually, the machine we obtain is a slightly optimised version that can work with open terms and may be used in implementations of proof assistants.