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...
Main Authors: | , , |
---|---|
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 |