Gradual typing aims at combining static and dynamic type checking by introducing a dynamic type and cast expressions. The dynamic type is assigned to expressions whose type is unknown until run time. A typed-based cast expression <S<=T>^l e specifies that the value of expression e is to be coerced form type T to S at run time. If such a coercion cannot be performed, the cast fails returning the blame label l. Recent works on the area deal with the dynamic semantics of gradual typing, where the choice of error-detection policy (eager or lazy) and of blame-tracking strategy (upcast-downcast or downcast), as well as the space efficiency issues make up a rich design space for dynamically typed lambda calculi with higher-order casts (Siek et al. 2009).

The gradually-typed lambda calculus is a version of the simply-typed lambda calculus with higher-order casts and blame labels. Henglein’s coercion calculus (Henglein 1993) underlies the casts in the gradually-typed lambda calculus. Coercions consist of some atomic operations that can be composed in a sequence or in an arrow. The coercion contraction rules specify how to reduce coercions, obtaining a normal coercion.

We establish by program transformation the correspondence between the reduction semantics of a closure-converted gradually-typed lambda calculus and the definitional interpreters presented by Siek and García. Thus we prove, for the case of the eager error-detection policy and the downcast blame-tracking strategy, Siek and Garcia’s conjectures concerning the correctness of their interpretation with respect to the calculus. The proof of correctness is easily generalised for other choices of error-detection policies and blame-tracking strategies by plugging a different set of coercion contraction rules at the start of the derivation.

This is joint work with Ilya Sergei and Pablo Nogueira.