Verifying Compiler Algorithms

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

9404646 Wand Because compilers are trusted components of almost every computer system, it is important to have trustworthy proofs of their correctness. This project would continue research on the development and verification of compilers based on formal specifications of programming languages. A major area of activity would extend semantics and compiler correctness proofs to languages for parallel computation. Some effort would also be directed toward the study of fundamental theories for object- oriented programming. Cross-fertilization with related research is expected. Techniques for optimization and concretization would be applied in the parallel setting, and the parallel setting would raise new problems for studies of optimization. Similarly, existing activity in type theory is concerned primarily with complexity of type inference algorithms. It is expected that some of these results to be applied in the object-oriented setting, and that studies of OOP would raise new theoretical questions in type theory. ***