From Reduction-based to Reduction-free Normalization

The construction builds on previous work on refocusing and on a functional correspondence between evaluators and abstract machines. It is also reversible.