Formal Design Environments.

Brian Aydemir, Adam Granicz, and Jason Hickey.
Formal Design Environments.
Theorem Proving in Higher-Order Logics (TPHOLs), 2002. Appears in NASA technical report NASA/CP-2002-211736.
PostScript (359 KB).

Abstract

We present the design of a formal integrated design environment. The long-term goal of this effort is to allow seamless interaction between software production tools and formal design and analysis tools, especially between compilers and higher-order theorem provers. The work in this report is the initial design and architecture for integration of

1. the MetaPRL logical framework,
2. a multi-language compiler we call Mojave, and
3. a generic extensible parser we call Phobos.

The integration is currently performed at the level of the Mojave functional intermediate representation, allowing the use of the theorem prover for program analysis, transformation, and optimization.