• Nitpick

  • Referenced in 61 articles [sw00622]
  • finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally...
  • CoCasl

  • Referenced in 26 articles [sw13076]
  • systems in terms of inductive datatypes as well as of co-inductive process types. Here...
  • Coq

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

  • Referenced in 514 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • PVS

  • Referenced in 614 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Haskell

  • Referenced in 844 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • SMT-LIB

  • Referenced in 182 articles [sw04103]
  • SMT-LIB was created with the expectation that...
  • z3

  • Referenced in 496 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • HOL

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

  • Referenced in 3387 articles [sw07248]
  • The On-Line Encyclopedia of Integer Sequence. The...
  • LCF

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

  • Referenced in 35 articles [sw08839]
  • StarExec: Starexec is a cross community logic solving...
  • CVC4

  • Referenced in 104 articles [sw09485]
  • CVC4 is an efficient open-source automatic theorem...
  • Agda

  • Referenced in 182 articles [sw09689]
  • Agda is a dependently typed functional programming language...
  • RADA

  • Referenced in 4 articles [sw20732]
  • RADA: a tool for reasoning about algebraic data...
  • GitHub

  • Referenced in 1503 articles [sw23170]
  • GitHub (originally known as Logical Awesome LLC)[3...