Introduction to the seL4 proofs

28 Dec 2021

• seL4
• verification
• screencast

Pattern-matching dependent types in Coq

21 May 2015

• Coq
• dependent types
• screencast

B-trees with GADTs

15 May 2013

• Haskell
• data structures
• dependent types
• screencast

Hole-driven Haskell

26 Feb 2013

• Haskell
• screencast