MetaPRL history and people


MetaPRL is the latest in the PRL family of systems developed over the last 25 years as a part of the Cornell PRL project. MetaPRL was conceived in January 1996 to address the concerns of scalability in formal systems. In the early part of the decade, NuPRL formalizations were mostly limited to smaller problems that focused on basic data structures and mathematical foundations. As the foundations were implemented, it became possible to formalize larger problems, like the verification of Ensemble being performed by Kreitz, Hayden, and Hickey. As with any growing system, scalability became a major concern: how do we share our results with other systems; how do we design domain-specific logics; how do we get the computational speed for proving properties of large systems? These questions led to the modular design on MetaPRL, where logical theories are treated as formal objects that include both the logical knowledge and domain-specific heuristics needed to use that knowledge. As more effort was put into the system MetaPRL eventually grew into a very general modern system whose modularity on all levels gives it flexibility to support a very wide range of applications.


Jason Hickey is the main author and architect of MetaPRL. The system was a large part of his PhD thesis "The MetaPRL Logical Programming Environment".

Aleksey Nogin joined the MetaPRL project in 1998. After Jason graduated from Cornell in 1999, Aleksey took over the coordination of the project. The system was a large part of his PhD thesis "Theory and Implementation of an Efficient Tactic-Based Logical Framework".

Robert Constable is the head of the Cornell PRL Group.

Alexei Kopylov is working on better understanding and improving MetaPRL Type Theory. In particular, he came up with and have implemented in MetaPRL a novel theory of extensible records.

Sergei Artemov is the head of the CUNY branch of the MetaPRL group.

Xin Yu is working on formalizing abstract algebra in MetaPRL.

Lori Lorigo and Richard Eaton are working on connecting MetaPRL and NuPRL LPE systems.

Stephan Schmitt and Christoph Kreitz implemented a first order prover ("JProver") in MetaPRL.

Vladimir Krupski is the coordinator of the Moscow branch of the MetaPRL group. He is working on improving MetaPRL unification algorithms.

Yegor Bryuhov implemented term cons-hashing using weak pointers and explicit DAG representations for terms. He is currently working on the arithmetical theories in MetaPRL Type Theory.

Eli Barzilay is working on implementing reflection in NuPRL and MetaPRL.

Carl Witty have contributed an extensive reference to MetaPRL Type Theory and lots of very helpful feedback.

Brian Aydemir is working on formalizing the functional intermediate reprsentation (FIR) of the MC compiler being developed at the California Institue of Technology by Jason Hickey. The goal is to be able to reason about code and code transformations.

Adam Granicz is working on generic parsing and formal compilation using the MetaPRL rewriring engine.

Nathan Gray and Cristian Tapus are working on implementing an extensible compiler (with special features like speculations and migration) using MetaPRL.