
Beluga
 Referenced in 26 articles
[sw01321]
 played an important role in mechanizing the metatheory of programming languages, it has been...

Lincx
 Referenced in 2 articles
[sw20270]
 resources. However, mechanizing the metatheory of such systems remains a challenge, as we need ... firstclass (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 metatheory 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 MartinLöf’s type theory ... correct metalanguage 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...

MetaPRL
 Referenced in 26 articles
[sw04624]
 MetaPRL is two things: it is a logical...

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

miniML
 Referenced in 17 articles
[sw22714]
 A simple applicative language: miniML. ...