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


Authors

Mitchell Pickard



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
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

Files




You might also like



Downloadable Citations