Skip to main content
PRL Project

Other Systems

Over the past two decades, this project and our worldwide associates in projects around systems like ACL2, Alf, Coq, Elf, HOL, IMPS, Isabelle, Kiv, LA, Lego, Mizar, NqThm, Otter, Oyster, and PVS have created a new field which we call here Formalized Mathematics (see also Automath and Qed ). We have become devoted to its growth and applications. This has led to the goal of supporting a Common Mathematics Library and the goal of enabling cooperation among theorem proving systems. We are building on the work of Howe which has combined HOL and Nuprl.

Projects: Description:

The Oyster system at Edinburgh University's AI department is based on the Nuprl type theory; it currently uses the logic from Nuprl 3. This is one of the systems that Alan Bundy's research group at Edinburgh uses to study proof planning. They call it the Oyster program development system. Alan Bundy said in his paper Automatic Guidance of Program Synthesis Proofs,

"We have built our own version of Nuprl, which we call Oyster. It differs from Nuprl by being implemented in Prolog rather than Lisp, being considerably smaller and more transparent, and using Prolog rather than ML as the tactic language."


Coq at INRIA


There are three other major provers based on constructive type theory: Alf at Gothenburg, Sweden; Coq at INRIA in France; and Lego, a system closely related to Coq built by Randy Pollock at Edinburgh. Alf is based on Martin-Löf type theory while Coq and Lego are based on Girard's impredicative type theory.


Kestrel Institute is a non-profit computer science research center whose mission is to advance the art and practice of synthesizing provably correct code from high-level specifications, to increase assurance, productivity and performance.


Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrized modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program.

Agda is also a proof assistant, an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. ~ description source »



There are three other tactic-oriented provers which like Nuprl are descended from Edinburgh LCF. HOL is one of the early descendants. The HOL88 systems use the same ML as Nuprl 4 for its tactic language. HOL90 uses SML as its tactic language. Isabelle also uses SML as its tactic language.

PVS system

The PVS system shares a number of features of Nuprl 4. It is based on a classical type theory with a dependent product type. Like its predecessor EHDM, it uses decision procedures extensively and, like Nuprl, it integrates them with a method for programming proof building that is similar to tactics, but is written in Lisp. PVS is the only other prover that generates what we call well-formedness goals and they call type checking conditions, or tcc's.