This development formalizes proofs of normalization of administrative reductions in CPS-translated lambda terms under call-by-value and with 3 different axiomatizations: with eta-expanded continuation variables, eta-reduced continuation variables, and generalized beta reduction. The code extracted from the proofs are higher-order one-pass CPS transformations. The development accompanies the following paper

Installation instructions

The formalization is compatible with Coq v.8.4. The appropriate version of Coq can be downloaded from In addition, an external library TLC is used that is available from The library is also included in this repository as a subdirectory tlc. To compile this development and obtain extracted OCaml programs you can use make with the provided Makefile. You can also consult the commented files containing extracted programs that have been transformed by hand to make them more readable (.ml files in the repository).