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.
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:
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.
- gives a list of people known to be working on the project.
- provides links to the other related systems and software.
- 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.
- 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.
- mailing list is a low-volume list for announcing major MetaPRL developments.
- 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.
- MetaPRL bug reports repository — use it to file new bug reports and to browse existing ones.