Mitchell Pickard

I'm a PhD Student in Computer Science at the University of Nottingham, in the Functional Programming Lab, supervised by Graham Hutton.

My research interests include functional programming, compilers, dependent types, program verification, and systems programming.

I'm the organiser of the FP Lab's seminar programme, and a represenative for the CS postgraduate researcher Learning Community Forum.


Dependently-Typed Compilers Don't Go Wrong (pdf, Agda formalisation)

Mitchell Pickard and Graham Hutton. In preparation, March 2020

Compilers are difficult to write, and difficult to get right. Bahr and Hutton recently developed a new technique for calculating compilers directly from specifications of their correctness, which ensures that the resulting compilers are correct-by-construction. To date, however, this technique has only been applicable to source languages that are untyped. In this article, we show that moving to a dependently-typed setting allows us to naturally support typed source languages, ensure that all compilation components are type-safe, and make the resulting calculations easier to mechanically check using a proof assistant.


Teaching assistant: