Patrick Bahr IT University of Copenhagen

The Calculated Typer

Zac Garby, Patrick Bahr and Graham Hutton
Submitted for peer review, February 2025.

Abstract

We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. In addition, we show how the calculations can be simplified by taking an algebraic approach based on fold fusion, and further improved by taking a constraint-based approach to solving and composing fusion preconditions. We illustrate our methodology with three examples of increasing complexity, starting with a simple expression language, then adding support for exceptions, and finally considering a version of the lambda calculus.

Categories: Type Systems, Formal Verification

Tags: Program Calculation, Type Checker