An implementation of Hoare and He's Unifying Theories of Programming in Isabelle

Isabelle LLVM Code Generator and Refinement

My solutions to exercises in "Concrete Semantics" (Tobias Nipkow, Gerwin Klein) These are for 2014-2015 version of the book.

Isabelle/HOL proofs about the eChronos RTOS

A formal definition and verification of System F. To be extended to System Fc

Isabelle formalization of binary consensus

Learning Isabelle