Hacker News new | past | comments | ask | show | jobs | submit login

Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :)

If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/

There is also a recent book that might interest you: http://www.concrete-semantics.org/




Sweet, thanks!




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: