A Calculational Approach to Type Checker Design

This paper presents a calculational approach to designing type checkers, deriving them from behavioral specifications using equational reasoning. The authors simplify calculations using an algebraic approach based on fold fusion and further improve it with a constraint-based approach to solving and composing fusion preconditions. The methodology is illustrated with three examples of increasing complexity: a simple expression language, one with exceptions, and a version of the lambda calculus.