An abstract machine for Lambda-terms normalization
Pierre Crégut · 1990
Two abstract machines reducing terms to their full normal form are presented in this paper. They are based on Krivine's abstract machine [Kri85] which uses an environment to store arguments of function calls. A proof of their correctness is then stated in the abstract framework of λσ-calculus [Cur89].