• 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...
  • HOL

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

  • Referenced in 160 articles [sw06302]
  • TPS and ETPS are, respectively, the Theorem Proving...
  • 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...
  • Agda

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

  • Referenced in 91 articles [sw15222]
  • seL4: formal verification of an OS kernel. Complete...