3 ms·
One should also mention Isabelle/HOL [1] and Concrete Semantics [2]. As of May 2018, Isabelle/HOL has the best proof automation, in case you want to get things
by YorkshireSeason 8y ago
One should also mention Isabelle/HOL [1] and Concrete Semantics
[2]. As of May 2018, Isabelle/HOL has the best proof automation, in case you want to get things done.
[1] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/
- unboxed_type 8y agoTrue. It is worth pointing out that Isabelle/HOL does not have dependent types in its underlying logic making framework building a (much?) harder work.
- YorkshireSeason 8y agoI'm not sure what you mean by "framework building" in this context.
- YorkshireSeason 8y agoWhoops, forgot to link to _Concrete Semantics_. [2] http://www.concrete-semantics.org http://www.concrete-semantics.org