MetaPRL is a part of the Cornell Prl Automated Reasoning Project.
MetaPRL is implemented in the OCaml language. OCaml has proved to an efficient and reliable ML implementation, thanks to Xavier Leroy and the Project Cristal group at INRIA.
The MetaPRL language is an extension of the OCaml programming language. The syntax extensions are implemented with CamlP4, a pretty-printer pre-processor for OCaml, developed by Daniel de Rauglaudre.
MetaPRL is listed in the Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks section of the Open Directory