Supporting Higher-Order Approaches to Symbolic Computation

点击翻译按钮获取中文摘要

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.