• Beluga

  • Referenced in 26 articles [sw01321]
  • played an important role in mechanizing the meta-theory of programming languages, it has been...
  • Lincx

  • Referenced in 2 articles [sw20270]
  • resources. However, mechanizing the meta-theory of such systems remains a challenge, as we need ... first-class (linear) contexts and an equational theory of context joins that can otherwise ... canonical forms and show that our equational theory of context joins is associative and commutative ... practical foundation for mechanizing the meta-theory of stateful systems...
  • PAL+

  • Referenced in 3 articles [sw21366]
  • notions to provide schematic mechanisms for specification of type theories and their use in practice ... implementation of type theories, such as Martin-Löf’s type theory ... correct meta-language for specifying type theories (e.g., dependent type theories ... type theories, and that its implementation reflects the actual use of type theories in practice...
  • Coq

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

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

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

  • Referenced in 6 articles [sw19139]
  • Coq Modulo Theory. Coq Modulo Theory (CoqMT) is...