• Abella

  • Referenced in 52 articles [sw09461]
  • Abella Interactive Theorem Prover (System Description). Abella [3] is an interactive system for reasoning about ... through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach ... binding in object languages. Amongst other things, Abella has been used to prove normalizability properties ... This paper discusses the logical foundations of Abella, outlines the style of theorem proving that...
  • Coq

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

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

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

  • Referenced in 17 articles [sw21364]
  • System description: Teyjus—a compiler and abstract machine...
  • Lolli

  • Referenced in 51 articles [sw40831]
  • Lolli is a logic programming language based on...