  Herman et al. pointed out that the insertion of run-time checks into a
gradually typed program could hamper tail-call optimization and, as a result,
worsen the space complexity of the program. To address the problem, they
proposed a space-efficient coercion calculus, which was subsequently improved
by Siek et al. The semantics of these calculi involves eager composition of
run-time checks expressed by coercions to prevent the size of a term from
growing. However, it relies also on a nonstandard reduction rule, which does
not seem easy to implement. In fact, no compiler implementation of gradually
typed languages fully supports the space-efficient semantics faithfully.
  In this paper, we study coercion-passing style, which Herman et al. have
already mentioned, as a technique for straightforward space-efficient
implementation of gradually typed languages. A program in coercion-passing
style passes "the rest of the run-time checks" around---just like
continuation-passing style (CPS), in which "the rest of the computation" is
passed around---and (unlike CPS) composes coercions eagerly. We give a formal
coercion-passing translation from $\lambda$S by Siek et al. to $\lambda$S$_1$,
which is a new calculus of first-class coercions tailored for coercion-passing
style, and prove correctness of the translation. We also implement our
coercion-passing style transformation for the Grift compiler developed by
Kuhlenschmidt et al. An experimental result shows stack overflow can be
prevented properly at the cost of up to 3 times slower execution for most
partially typed practical programs.
