Deriving Interpretations of the Gradually-Typed Lambda Calculus

Siek and Garcia (2012) have explored the dynamic semantics of the gradually-typed lambda calculus by means of definitional in-terpreters and abstract machines. The correspondence between the calculus’s mathematically described small-step reduction seman-tics and the implemented big-step definitional interpreters was left as a conjecture. We prove and generalise Siek and Garcia’s con-jectures using program transformation. We establish the correspon-dence between the definitional interpreters and the reduction se-mantics of a closure-converted gradually-typed lambda calculus that unifies and amends various versions of the calculus. We use a layered approach and two-level continuation-passing style so that the correspondence is parametric on the subsidiary coercion calcu-lus. We have implemented the whole derivation for the eager error-detection policy and the downcast blame-tracking strategy. The cor-respondence can be established for other choices of error-detection policies and blame-tracking strategies, by plugging in the appropri-ate artefacts for the particular subsidiary coercion calculus