@article{mococa,
  author = {Bahr, Patrick and Hutton, Graham},
  title = {Monadic Compiler Calculation (Functional Pearl)},
  year = {2022},
  issue_date = {August 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {ICFP},
  url = {https://doi.org/10.1145/3547624},
  doi = {10.1145/3547624},
  abstract = {Bahr and Hutton recently developed a new approach to calculating correct
compilers directly from specifications of their correctness.  However, the
methodology only considers \emph{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 \emph{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.
},
  journal = {Proceedings of the ACM on Programming Languages},
  month = aug,
  articleno = {93},
  numpages = {29},
  Keywords = {program calculation, verified compiler, virtual machine, Agda, bisimulation, monad}
}