• Nuprl

  • Referenced in 390 articles [sw06751]
  • Nuprl system is a framework for reasoning about mathematics and programming. Over the years ... meet the demands of large-scale 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 command-line...
  • 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...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • Nuprl-Light: an implementation framework for higher-order logics. this paper we describe Nuprl-Light ... descendent of the Nuprl [2] theorem prover, that addresses the issues of diversity and sharing ... call it an implementation framework. Instead, Nuprl-Light provides a meta-framework 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 higher-dimensional 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 object-based 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 ISO-standardized, object-oriented programming...
  • KeYmaera

  • Referenced in 41 articles [sw03709]
  • KeYmaera: A hybrid theorem prover for hybrid systems...
  • 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...