Welcome to MetaPRL

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:

• computational 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 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.

MetaPRL Documentation

Here is the listing of some information provided in MetaPRL documentation. If you want to print MetaPRL documentation or read in Postscript or PDF format, you can either download it from http://files.metaprl.org/doc/ (updated nightly) or compile it yourself. To compile it yourself, you'll need to download and install MetaPRL sources and the htmldoc utility and than run omake docs from the MetaPRL top-level directory.

People

gives a list of people known 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.

Tutorial

will help you to get started using the system.

Logical Theories

is a daily updated PDF file that gives a listing of most of the logical theories implemented in MetaPRL together with some documentation.

Developer Guide

should be your first stop when you decide to add or update some MetaPRL code.

MetaPRL-Announce

mailing list is a low-volume list for announcing major MetaPRL developments.

MetaPRL-CVS

mailing list receives all the MetaPRL Commit messages and is ideal for tracking day-to-day development of MetaPRL.

Commit Logs

show MetaPRL revision history.

Bugzilla

MetaPRL bug reports repository — use it to file new bug reports and to browse existing ones.