• Coq

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

  • Referenced in 19 articles [sw00421]
  • Hybrid: a package for higher-order syntax in...
  • Isabelle

  • Referenced in 714 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Ott

  • Referenced in 31 articles [sw00663]
  • Semantic definitions of full-scale programming languages are...
  • ML

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

  • Referenced in 26 articles [sw01321]
  • Our main interest in this project is to...
  • SHOGUN

  • Referenced in 104 articles [sw03517]
  • The SHOGUN machine learning toolbox. We have developed...
  • Haskell

  • Referenced in 884 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • HOL

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

  • Referenced in 9 articles [sw05575]
  • ProActive is a Java library for parallel, distributed...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • TPS and ETPS are, respectively, the Theorem Proving...
  • OCaml

  • Referenced in 276 articles [sw06363]
  • OCaml is the most popular variant of the...
  • Nuprl

  • Referenced in 396 articles [sw06751]
  • The Nuprl system is a framework for reasoning...
  • Twelf

  • Referenced in 173 articles [sw06888]
  • Twelf is a language used to specify, implement...
  • LCF

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

  • Referenced in 50 articles [sw08992]
  • FreshML: programming with binders made simple. FreshML extends...
  • Bedwyr

  • Referenced in 23 articles [sw09460]
  • The Bedwyr System for Model Checking over Syntactic...
  • Abella

  • Referenced in 52 articles [sw09461]
  • The Abella Interactive Theorem Prover (System Description). Abella...