Skip to main content

Research Repository

Advanced Search

Calculating dependently-typed compilers (functional pearl)

Pickard, Mitchell; Hutton, Graham

Calculating dependently-typed compilers (functional pearl) Thumbnail


Mitchell Pickard


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.


Pickard, M., & Hutton, G. (2021). Calculating dependently-typed compilers (functional pearl). Proceedings of the ACM on Programming Languages, 5(ICFP), 1-27.

Journal Article Type Article
Acceptance Date Jun 19, 2021
Online Publication Date Aug 18, 2021
Publication Date Aug 18, 2021
Deposit Date Jul 19, 2021
Publicly Available Date Aug 18, 2021
Journal Proceedings of the ACM on Programming Languages
Electronic ISSN 2475-1421
Peer Reviewed Peer Reviewed
Volume 5
Issue ICFP
Article Number 82
Pages 1-27
Public URL
Publisher URL


You might also like

Downloadable Citations