Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#27 Formalizing an OS: The seL4

Gerwin Klein

Apr 11th 2024   |  119 min
0:00
0:00

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine.

Links