(Joint work with Kevin Millikin and Johan Munk)
We apply (1) the functional correspondence between evaluation functions and abstract machines and (2) the syntactic correspondence between one-step reduction functions and abstract machines to “normalizing under lambdas”, i.e., the issue of strong normalization in the lambda-calculus. We show that abstract machines for strong normalization correspond, on the one hand, to normalization functions in the area of normalization by evaluation, and on the other hand, to a particular normalization strategy in the corresponding calculus. Our running example is Curien's abstract machine for strong normalization in “Categorical Combinators, Sequential Algorithms and Functional Programming” (1993). We connect it, on the one hand, to a normalization function with an environment, and, on the other hand, to a normalization strategy in Curien's original calculus of closures.