First Class Call Stacks: Exploring Head Reduction

Philip Johnson-Freyd, Paul Downen, Zena M. Ariola

Weak-head normalization is inconsistent with functional extensionality in the call-by-name $\lambda$-calculus. We explore this problem from a new angle via the conflict between extension…