The MetaPRL Logical Programming Environment
by Jason Hickey
Cornell University Ph.D. Thesis
This thesis is primarily about the design of formal programming environments for building large software systems. This work articulates two principles and uses them to guide the design, implementation, and study of a specific formal programming environment. First, design methods for large software systems will 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 also presents the the MetaPRL formal system. MetaPRL was built to provide a modular, abstract logical framework where multiple designs 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.
- The development of an untyped meta-logic using explicit substitution.
- The definition of a very-dependent function type in the Nuprl type theory.
- A system architecture for generic multi-logical development.
- A generic refiner that provides automation and enforcement for the multiple logical theories in logical environment.
- A module system for logics and theories.
- A generic distributed interactive theorem prover.
bibTex ref: Hic01