Modular Program Analyses for Higher-Order Programming Languages

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

9619756 The basic goal of the project is to develop an automatic theorem prover that can reason about properties of programs in high- level, mathematical programming languages. The theorem prover will supply the results of its analysis to programmers by adding hyperlinks to annotations and drawing diagrams to the program text. The annotations will describe sets of values; the diagrams will explain the anticipated flow of these values. Both can be used to understand the program's behavior before it runs. As a result, programmers will be able to create programs that either do not fail at all or only fail at a small, well-defined set of program points. While many of the basic properties of such theorem provers are understood, it is an open question whether they can be applied to programs of hundreds or thousands of modules with mutual dependencies. Hence, the central goal of the project is to design a modular, scalable proof system, to prove its correctness, to engineer a suitable programming environment, and to apply the theorem prover to itself and its programming environment. ***