Automating the Functional Correspondence between Higher-Order Evaluators and Abstract Machines

Maciej Buszka, Dariusz Biernacki

The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists…