Mitchell Pickard

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.


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

Mitchell Pickard and Graham Hutton. Submitted to the International Conference on Functional Programming, 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.