3 ms·

Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving

Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.

mcguire 9y ago
As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it. (And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
- auggierose 9y ago
  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/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
  - mcguire 9y ago
    Sweet, thanks!