First Class Call Stacks: Exploring Head Reduction

Weak-head normalization is inconsistent with functional extensionality in the call-by-name λ-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the λ-calculus with control, we derive and justify alternative operationa...

Full description

Bibliographic Details
Main Authors: Philip Johnson-Freyd, Paul Downen, Zena M. Ariola
Format: Article
Language:English
Published: Open Publishing Association 2016-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1606.06378v1