Welcome to MetaPRL

MetaPRL Banner

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:

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:

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:

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:

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.

This work is supported in part by the DoD Multidisciplinary University Research Initiative (MURI) program administered by the Office of Naval Research (ONR) under Grant N00014-01-1-0765, the Defense Advanced Research Projects Agency (DARPA), the United States Air Force, and the Lee Center.