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.