News for hackers. Stuff that matters.

A comment on The Z3 Theorem Prover released under MIT license. Parent comment

Re:The Z3 Theorem Prover released under MIT license by javra on Thursday March 26, 2015 @06:14PM (#9273504)
One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/
[ Parent | on HN ]
Re:The Z3 Theorem Prover released under MIT license by NotableAlamode on Thursday March 26, 2015 @07:11PM (#9273778)
Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?
[ Parent | on HN ]