9504288 Mairson The goal of this research is to investigate the computational resources required to implement correct, optimal evaluation mechanisms for the lambda calculus. Because lambda calculus is a foundation for the design and implementation of programming languages, such research could contribute to the understanding of programming language implementation. Moreover, it would integrate approaches to computation that emphasize semantic issues as well as those of computational complexity. The solution to optimality proposed by Gonthier, Abadi, and L vy will be analyzed. The computational correctness of this scheme in an elementary, first-principles sense will be established and its computational complexity will be analyzed. Ultimately, a version of a correct evaluator whose complexity is polynomial in a reasonable cost model for lambda calculus will be put forward that the lambda calculus may be regarded as a "first class" formalism in the sense of the invariance thesis, the computationally efficient version of the Church-Turing thesis. The static semantics as a possible foundation for a lazy environment model will also be investigated. ***
