Matthew Brecknell

Expert Overview

Senior Proof Engineer
CSIRO's Data61

Matthew began programming in C++, but became curious about functional programming when he realised that template metaprogramming was probably a rudimentary form of FP. Via Haskell, he became interested in type theory, and then via Coq, in theorem proving. He now has his dream job working with some of the world leaders in formal verification, where he uses Isabelle/HOL to prove things about the C implementation of the seL4 microkernel.


Things I'm Doing
Talks I've Given

Talks I've Given