• ProofPower

  • Referenced in 57 articles [sw06339]
  • ProofPower is a specification and proof tool based on an implementation of Higher Order Logic ... following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof...
  • OpenTheory

  • Referenced in 17 articles [sw32625]
  • order logic, including HOL Light, HOL4 and ProofPower. It is hoped that OpenTheory packages...
  • ArcAngelC

  • Referenced in 6 articles [sw06338]
  • discuss its mechanisation in a theorem prover, ProofPower...
  • Coq

  • Referenced in 1906 articles [sw00161]
  • Coq is a formal proof management system. It...
  • ArcAngel

  • Referenced in 14 articles [sw01812]
  • ArcAngel: a tactic language for refinement. Morgan’s...
  • Z

  • Referenced in 286 articles [sw10291]
  • Using Z. Specification, refinement, and proof. The book...
  • Circus

  • Referenced in 90 articles [sw21828]
  • The Semantics of Circus. Circus is a concurrent...