Introduction to the seL4 integrity theorems

11 Dec 2022

• seL4
• verification
• talk

Introduction to the seL4 proofs

28 Dec 2021

• seL4
• verification
• screencast

Pattern-matching dependent types in Coq

21 May 2015

• Coq
• dependent types
• screencast

Difference lists

23 Sep 2014

• Haskell
• data structures

C++11 universal reference pop-quiz

02 Aug 2013

• C++

B-trees with GADTs

15 May 2013

• Haskell
• data structures
• dependent types
• screencast

Hole-driven Haskell

26 Feb 2013

• Haskell
• screencast