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: | 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 |
Similar Items
-
Exploring the use of call stack depth limits to reduce regression testing costs
by: Bogren, Patrik, et al.
Published: (2021) -
Properties of Sequent-Calculus-Based Languages
by: Johnson-Freyd, Philip
Published: (2018) -
Properties of Sequent-Calculus-Based Languages
by: Johnson-Freyd, Philip Alden
Published: (2018) -
Sequent Calculus: A Logic and a Language for Computation and Duality
by: Downen, Paul
Published: (2017) -
Destackification and Motivic Classes of Stacks
by: Bergh, Daniel
Published: (2014)