MetaPRL — A Modular Logical Environment.

Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu.
MetaPRL — A Modular Logical Environment.
In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2003.
Springer page, PDF (283 KB), PostScript (208 KB).

Abstract

MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project involving several universities in several countries. The MetaPRL system combines the properties of an interactive LCF-style tactic-based proof assistant, a logical framework, a logical programming environment, and a formal methods programming toolkit. MetaPRL is distributed under an open-source license and can be downloaded from http://metaprl.org/. This paper provides an overview of the system focusing on the features that did not exist in the previous generations of PRL systems.

Back to my publications

Last update: Sunday, December 07, 2003 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)