An abstract machine for Lambda-terms normalization

1 May 1990

proceedings article
Published by Association for Computing Machinery (ACM)

p. 333-340
https://doi.org/10.1145/91556.91681

Abstract

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 &lgr;&sgr;-calculus [Cur89].

Keywords

FULL NORMAL FORM
ABSTRACT MACHINE
FUNCTION CALL
LAMBDA-TERMS NORMALIZATION
ABSTRACT FRAMEWORK
NORMAL FORM

This publication has 4 references indexed in Scilit:

A representation of Lambda terms suitable for operations on their intensions
Published by Association for Computing Machinery (ACM) ,1990
Explicit substitutions
Published by Association for Computing Machinery (ACM) ,1990
Improving the three instruction machine
Published by Association for Computing Machinery (ACM) ,1989
A Transformation System for Developing Recursive Programs
Journal of the ACM, 1977