MetaPRL is two things: it is a logical framework where multiple logics can be defined and related, and it is a system implementation with support for interactive proof and automated reasoning. A primary feature of MetaPRL is a semantic connection to programming languages, that allows the system to be used as a logical programming environment, where programs are constructed as a mixture of specifications, implementations, and verifications.

System goals

The MetaPRL system was implemented with the purpose of supporting relations between logics. There is a huge investment in formal work in systems like PVS, HOL, Coq, ELF, Nuprl, and others. These systems use different logics and different methodologies, but they have common goals and their results share fundamental mathematical underpinnings. Mathematical developments are expensive; our first goal is to expose the logical foundations that the systems share, to allow the results to be shared between systems. MetaPRL supports sharing with three features:

• Programs and logics are developed as modules that define computational, heuristic, and mathematical properties.
• Modules are constructed incrementally by adding formal properties to existing modules (the empty module is the root of every logic). Just as object-oriented programming allows code re-use, incremental module construction allows logical re-use: logics can share a common core with properties that are inherited as the logics are extended.
• Modules are first-class: relations between logics are either constructed by inheritance, or explicitly constructed as functions between modules.

This first goal give formal underpinnings to logical sharing; our next goal is to provide practical impact. Work is underway to relate the PVS, HOL, Isabelle, and Nuprl mathematical foundations. Precursors to these developments are available in the MetaPRL distribution, including logics for:

• constructive type theory (ITT), based on the Martin-Lof style Nuprl type theory,
• constructive set theory, based on Aczel's axiomatization,
• the LF logical framework,
• first order logic.

These logics provide the principles of formal logical relations. Aczel's set theory is modeled in the type theory (as is first-order logic). The LF work is less complete.

Our work focuses specifically on programming: even though large-scale programming is unreliable, the advantage of high-speed automation has pushed computation into our safety-critical infrastructure, including the telephone system, the power grid, the financial sector, and the transportation industry. The reliability of critical systems must be ensured--while retaining productivity. MetaPRL addresses the problem in two ways:

• The system provides a semantic framework to allow program development in an environment of mixed specification and implementation. Logical foundations are used both to guide the development and to ensure the reliability of developing software. The distribution contains a semantic account of core OCaml that allows ML programs to be intermixed with specifications in type theory.
• The majority of existing code is poorly documented and poorly structured. While this is the most speculative of our projects, MetaPRL supports the hardening of existing code by developing program-specific type systems that verify program abstractions.

Finally, our goal is speed. Higher-order formal systems require a mixture of interactive and automated proving; the load on the programmer is proportional to how efficient the system is in deriving formal properties. MetaPRL focuses on this problem at its foundation (hence the name "light") with these features:

• Modularity is used to provide domain-specific heuristics and algorithms, and to restrict the logical search complexity.
• The implementation language, OCaml, provides performance close to C, but with a formal semantics, type safety, modularity, and extensive checking to assist code modification and development.
• Abstract data structures provide optimized domain-specific logical operations.
• MetaPRL is a fully-distributed, fault-tolerant theorem prover. The distribution over Ensemble scales to over 100 machines over a wide-area network (depending on the parallel properties of the domain problem). Faults are tolerated transparently: processors may join and leave a process group arbitrarily--problem outcomes are not affected by process failures. Furthermore, the distribution is transparent: programmers use the standard search language.

Documentation

Here are some places where you can find out more about MetaPRL.

People gives a list of people know to be working on the project.

Links provides links to the other related systems and software.

Downloading describes how to download, configure, and install MetaPRL.

Logical framework presents the logical properties of the system.

System description gives an overview of MetaPRL's architecture and features.

User guide provides instructions on using MetaPRL.