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 FP Lab's represenative for the CS postgraduate researcher Learning Community Forum.
Mitchell Pickard and Graham Hutton. Proceedings of the ACM on Programming Languages, Volume 5, Issue ICFP, Article 82, August 2021.
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.