• 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 ... logical foundations of Abella, outlines the style of theorem proving that it supports and finally...
  • Coq

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

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