Matthew Brecknell

Share

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 –  VIEW SLIDES

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 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 saying a single number from the set {0..n}, without repeating any number said previously, and without any other communication. The cats are allowed a single incorrect guess, but otherwise every cat must say the number on its own hat.

In this talk, we’ll methodically derive a solution, 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.

For more information on the topic, see the GitHub repository.