Matthew Brecknell
Senior Proof EngineerCSIRO'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.
Talks I've Given
-
Schrödinger’s Hats: A Puzzle about Parities and Permutations
Featuring Matthew Brecknell
Meet Schrödinger, who travels the world with an unusually clever clowder of n talking cats. In their latest show, the cats stand in a line. Schrödinger asks a volunteer to take n+1 hats, numbered zero to n, and randomly assign one to each cat, so that there is one spare. Each cat sees...
practice -
Pattern matching dependent types in Coq
Featuring Matthew Brecknell
Pattern matching with dependent types in Coq can be awkward, while the same program in Agda might be straightforward and elegant. Yet despite the awkwardness, there may still be reasons to choose Coq for your next dependently-typed development, for example if you want a tactic language to develop...
technique -
Getting Data Structures Right with GADTs and nested types
Featuring Matthew Brecknell
Learn about GADTs and nested data types, and how you can use them to encode structural invariants in your Haskell types. You’ll also gain some insight into the inner workings of efficient functional data structures.
In the talk, I’ll show a B-tree, using a GADT to maintain balance....
algorithm -
Kiama: Domain-Specific Languages for Language Implementation in Scala
Featuring Matthew Brecknell
In this talk we give an overview of our Kiama language processing library (https://code.google.com/p/kiama/) for Scala. Kiama-based programs use high-level domain-specific languages to describe structured input for parsing, static analysis of programs via attribute grammars, program...
technique