# Matthew Brecknell

Proof Engineer at Data61 (formerly NICTA)

matthew.brecknell.net

@mbrcknl

mbrcknl

mbrcknl

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.

## YOW! Lambda Jam 2017 Sydney

**Schrödinger’s Hats: A Puzzle about Parities and Permutations**

TALK – 30 mins.

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 (not a plant!) 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 all of the hats in front of it, but not its own hat, nor those behind, nor the spare hat. The cats then take turns, each calling out a single number from the set {0..*n*}, without repeating any number previously called, and without any other communication. Although the first call is allowed to be wrong, the remaining cats always call out the numbers on their own hats.

In this talk, we’ll figure out how they do this, from first principles, and we’ll formally prove that the method always works. Along the way, we’ll reinvent some elementary theory of permutation groups, in particular, a parity property. You’ll get a taste of what it’s like to formally model a problem in Isabelle/HOL, and prove properties of interest. This is the same theorem prover we use to prove the functional correctness of the seL4 microkernel.