On: Ask HN: What was the best CS paper you read in 2017?

[auggierose]

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/

[mcguire → auggierose]

Sweet, thanks!