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, Xin Yu.

In D. Basin, B. Wolff eds., 16th International Conference on Theorem Proving in Higher Order Logics ((TPHOLs'03),
LNAI 2758, pp. 287-303, Springer Verlag, 2003.


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 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 overview of papers

Bibtex Entry

@InProceedings{inp:Hickey+03a, author = "Jason Hickey and Aleksey Nogin and Robert L. Constable and Brian E. Aydemir and Eli Barzilay and Yegor Bryukhov and Richard Eaton and Adam Granicz and Alexei Kopylov and Christoph Kreitz and Vladimir N. Krupski and Lori Lorigo and Stephan Schmitt and Carl Witty and Xin Yu", title = "{MetaPRL} --- A Modular Logical Environment", booktitle = "16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03)", year = 2003, editor = "D. Basin and B. Wolff", volume = 2758, series = "Lecture Notes in Artificial Intelligence", pages = "287--303", publisher = "Springer Verlag" }