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.

@article{paperbot1128,
  title = {Calculating dependently-typed compilers (functional pearl)},
  author = {Mitchell Pickard and Graham Hutton},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {ICFP},
  year = {2021},
  doi = {10.1145/3473587}
}