
Nuprl
 Referenced in 390 articles
[sw06751]
 Nuprl system is a framework for reasoning about mathematics and programming. Over the years ... meet the demands of largescale applications. Nuprl LPE, the newest release, features an open...

Automath
 Referenced in 406 articles
[sw07127]
 which the better known current ones are Nuprl...

Agda
 Referenced in 191 articles
[sw09689]
 dependent types, such as Coq, Epigram and NuPRL. This package includes both a commandline...

CLAM
 Referenced in 39 articles
[sw19619]
 proof editor closely based on the Cornell NuPRL system, but implemented in Prolog. CLAM...

JProver
 Referenced in 13 articles
[sw09978]
 proof objects, and its integration into the Nuprl proof development system...

NuprlLight
 Referenced in 1 article
[sw31982]
 NuprlLight: an implementation framework for higherorder logics. this paper we describe NuprlLight ... descendent of the Nuprl [2] theorem prover, that addresses the issues of diversity and sharing ... call it an implementation framework. Instead, NuprlLight provides a metaframework where logical frameworks ... such as LF, Nuprl, set theory, and other theories can be defined and developed. Since...

RedPRL
 Referenced in 2 articles
[sw23593]
 cubical computational type theory, which extends the Nuprl semantics by higherdimensional features inspired...

AXIOM
 Referenced in 172 articles
[sw00063]
 Axiom is a general purpose Computer Algebra system...

Coq
 Referenced in 1818 articles
[sw00161]
 Coq is a formal proof management system. It...

Dafny
 Referenced in 66 articles
[sw00183]
 Dafny is an imperative objectbased language with...

Refiner
 Referenced in 5 articles
[sw00790]
 The science and engineering disciplines rely heavily on...

PVS
 Referenced in 624 articles
[sw03484]
 PVS is a verification system: that is, a...

Eiffel
 Referenced in 290 articles
[sw03522]
 Eiffel is an ISOstandardized, objectoriented programming...

KeYmaera
 Referenced in 41 articles
[sw03709]
 KeYmaera: A hybrid theorem prover for hybrid systems...

MetaPRL
 Referenced in 26 articles
[sw04624]
 MetaPRL is two things: it is a logical...

HOL
 Referenced in 514 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

LCF
 Referenced in 157 articles
[sw08360]
 Edinburgh LCF. A mechanized logic of computation. From...

CakeML
 Referenced in 46 articles
[sw08799]
 Cakeml, a verified implementation of ML. We have...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof...