Member since 1 year
Specialises In (based on submitted proposals)
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.