19 stycznia 2017 14:00
Małgorzata Biernacka: On the extraction of one-pass CPS transformations from normalization proofs
A straightforward translation from the lambda calculus into continuation-passing style introduces so-called administrative redices that can be optimized away in a second pass over the translated term. By a careful analysis of CPS terms one can instead write optimized variants of the transformation that avoid the construction of administrative redices -- there exist a number of such algorithms in the literature.
In this talk, I will present a method to mechanically obtain one-pass, higher-order transformations of lambda terms into CPS. Given a naive, non-optimizing translation from the source to the target language, we prove the normalization property a la Tait in the target language with respect to administrative reductions; the computational content of the proof is an optimized transformation. The applicability of this approach will be illustrated with three variants of the CPS transformation: eta-reduced call-by-value CPS, eta-expanded call-by-value CPS, and call-by-value CPS with generalized beta- reduction. This approach has been formalized in Coq and the programs extracted from the proofs coincide with previously known transformations written by hand.