Categories: research



I work on program verification, formal methods and theorem proving. In general, I am interested in what we can prove about the systems we can build, and what those proofs say about the systems we should build. My current focus is on:

Please look at my publications and software

Past projects

Related articles:

  • 2018-07-02 Funded PhD places
  • 2018-06-14 A typed DSL for parsing
  • 2018-05-30 Potential improvements in filesystem performance
  • 2018-05-22 First Python program: an Earley parser!
  • 2018-02-01 New OCaml library: path resolution
  • 2017-09-06 ICFP most influential paper from 10 years ago
  • 2017-03-16 tjr-btree: a CoW B-tree library in OCaml
  • 2015-04-27 Why operational models?
  • 2014-11-26 Isabelle on 64bit ubuntu with 32bit libraries