The metaprl logical programming environment
Robert L. Constable, Jason J. Hickey · 2000
This thesis is primarily about the design of formal programming environments for building large software systems. The work presented here is based on two essential concepts. First, design methods for large software systems must include multiple languages, methodologies, and refinement techniques that are suited to problem subdomains. This means that any formal system must provide the ability to define multiple logics, and it is by definition a logical framework. Second, the framework must provide the ability to express formal relations between logical theories to address the problem of system decomposition. This thesis presents the design of the MetaPRL formal system. The MetaPRL design goal has been to provide a modular, abstract logical framework where multiple design methods can be expressed and related. The MetaPRL design builds on our experience with logical frameworks and with structured programming concepts like inheritance and re-use to provide an efficient, highly abstract, logical machine. The contribution includes several parts. (1) The development of an untyped meta-logic using explicit substitution. (2) The definition of a very-dependent function type in the Nuprl type theory. The very-dependent function type provides the logical specification of theories and modules, and it provides the basis for compositional reasoning. (3) A system architecture for generic multi-logical development. The architecture ties together a refiner (the theorem prover in a PRL system), a logical library of system components, an interactive proof system, and a compiler. (4) A generic refiner that provides automation and enforcement for the multiple logical theories in logical environment. The refiner provides the basis for defining and relating logics, and it is also critical performance bottleneck. We have been able to keep the refiner generic but efficient. (5) A module system for logics and theories. The module system provides an inheritance mechanism that is the basis for re-use of proofs and programs as well as for expressing relations between theories. (6) A generic distributed interactive theorem prover. The distribution mechanism is tactic-based, interactive, and multi-logical. System faults, such as machine and network failures, are handled transparently, allowing a developer to make maximum use of the available computational resources for development.