Я немного не понял - алгоритм abstraction elimination дан Тёрнером в 79 году (и, судя по названию статьи, не первый такой, просто тот, который сейчас все знают). Все модели лямбда-исчисления разные, но эквивалентные. (И интересны только алгебраистам - но это наглое оценочное суждение, конечно! Хотя покажите мне кого-нибудь, кто читал все это в Хиндли или Барендрегте, не вставив спички в глаза.) А в чем цимес, цимес-то в чем? Где новизна, и почему бы не обратиться вместо этого к первоисточникам, которым не требовался сопряженный функтор дабы дойти до нужника?