Calculating dependently-typed compilers (functional pearl)

Pickard, Mitchell; Hutton, Graham

Abstract

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.

Citation

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

• 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
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 5
• Issue: ICFP
• Article Number: 82
• Pages: 1-27
• DOI: https://doi.org/10.1145/3473587
• Public URL: https://nottingham-repository.worktribe.com/output/5805202
• Publisher URL: https://dl.acm.org/doi/10.1145/3473587