CISE Postdoctoral Program: Computational Efficiency of Optimal Reduction in Lambda Calculus

小行星9504288 本研究的目标是调查所需的计算资源，实现正确的，最佳的评价机制的lambda演算。 由于lambda演算是设计和实现编程语言的基础，这样的研究可以有助于理解编程语言的实现。 此外，它将整合强调语义问题以及计算复杂性的计算方法。 Gonthier，Abadi和L vy提出的最优性解决方案将被分析。 该方案的计算正确性在一个基本的，第一原理的意义将建立和其计算复杂性进行分析。 最后，一个正确的评价，其复杂性是多项式在一个合理的成本模型的lambda演算的版本将被提出，lambda演算可以被视为一个“一流”的形式主义的意义上的不变性论文，计算效率的版本的教会图灵论文。 静态语义作为一个可能的基础，懒惰的环境模型也将进行调查。 ***

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. ***