Skip to main content

Research Repository

Advanced Search

Monadic compiler calculation (functional pearl)

Bahr, Patrick; Hutton, Graham

Monadic compiler calculation (functional pearl) Thumbnail


Patrick Bahr


Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers converging behaviour of the source language, which means that the compiler could potentially produce arbitrary, erroneous code for source programs that diverge. In this article, we show how the methodology can naturally be extended to support the calculation of compilers that address both convergent and divergent behaviour simultaneously, without the need for separate reasoning for each aspect. Our approach is based on the use of the partiality monad to make divergence explicit, together with the use of strong bisimilarity to support equational-style calculations, but also generalises to other forms of effect by changing the underlying monad.


Bahr, P., & Hutton, G. (2022). Monadic compiler calculation (functional pearl). Proceedings of the ACM on Programming Languages, 6(ICFP), 80-108.

Journal Article Type Article
Acceptance Date Jul 1, 2022
Online Publication Date Aug 31, 2022
Publication Date Aug 29, 2022
Deposit Date Sep 5, 2022
Publicly Available Date Sep 6, 2022
Journal Proceedings of the ACM on Programming Languages
Electronic ISSN 2475-1421
Publisher Association for Computing Machinery (ACM)
Peer Reviewed Peer Reviewed
Volume 6
Issue ICFP
Article Number 93
Pages 80-108
Keywords Safety, Risk, Reliability and Quality, Software
Public URL
Publisher URL


You might also like

Downloadable Citations