Supporting Higher-Order Approaches to Symbolic Computation

题目：支持符号计算的高阶方法摘要：软件认证和使用的新趋势表明，在编程环境中，对规范、程序和证明等对象的显式处理越来越重要。已经开发了一些优雅的方法，使用lambda演算以逻辑可验证的方式表示和操作这些结构。本研究关注的是在计算设置中灵活有效地利用由此产生的高阶方法来处理符号结构。其中一个重点是理解并获得使用受控但通用的操作来分解lambda项的效率优势，这是该方法的核心。将开发用于部署此操作的新算法，利用其中的显式替换处理的方法以及适当的编译技术。在另一个方向上，将评估lambda项的机器表示中的选择，并设计实现对它们的优化约简策略的机器。研究结果将应用于目前正在几个验证和程序操作项目中开发的系统。该系统将用于课堂环境中正式方法的亲身实践。还设想在软件开发的正式技术的广泛领域对研究生和本科生进行培训。

PROPOSAL NUMBER: CPA 0429572TITLE: Supporting Higher-Order Approaches to Symbolic ComputationPI: Gopalan NadathurABSTRACT:Emerging trends in software authentication and use indicate a growing importance for the explicit treatment of objects such as specifications, programs and proofs in programming contexts. Elegant methods have been developed that employ lambda calculi for representing and manipulating such structures in logically certifiable ways. This research concerns the flexible and efficient utilization within computational settings of the resulting higher-order approach to dealing with symbolic structures. One focus is that of understanding and reaping the efficiency benefits of using a controlled but versatile operation for decomposing the lambda terms that are central to the approach. New algorithms for deploying this operation, methods for exploiting explicit treatments of substitution within them and appropriate compilation techniques will be developed. In another direction, choices in the machine representation of lambda terms will be evaluated and machinery for realizing optimized reduction strategies over them will be designed. The research resultswill be applied to a system that is currently being exploited in several verification and program manipulation projects. This system will be used in a hands-on exposure of formal methods in the classroom setting. The training of graduate and undergraduate students in the broad area of formal techniques in software development is also envisaged.