@inproceedings{calctyper,
  author = {Zac Garby and Patrick Bahr and Graham Hutton},
  title = {The Calculated Typer},
  abstract = {We present a calculational approach to the design of type checkers,
showing how they can be derived from behavioural specifications using
equational reasoning.  We focus on languages whose semantics can be
expressed as a fold, and show how the calculations can be simplified
using fold fusion.  This approach enables the compositional derivation
of correct-by-construction type checkers based on solving and composing
fusion preconditions.  We introduce our approach using a simple 
expression language, to which we then add support for exception
handling and checked exceptions.},
  booktitle = {Proceedings of the 18th ACM SIGPLAN International Haskell Symposium},
  pages = {17–29},
  numpages = {13},
  keywords = {program calculation, type checking},
  location = {Singapore, Singapore},
  isbn = {9798400721472},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3759164.3759346},
  doi = {10.1145/3759164.3759346},
  month = oct,
  Date = {2025-10-09},
  year = {2025}
}