|
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. |
||
|
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 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" } | |||