Back to Search
Start Over
First Class Call Stacks: Exploring Head Reduction
- Source :
- Electronic Proceedings in Theoretical Computer Science, Vol 212, Iss Proc. WoC 2015, Pp 18-35 (2016)
- Publication Year :
- 2016
- Publisher :
- Open Publishing Association, 2016.
-
Abstract
- 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 operational semantics and a sequence of abstract machines for performing head reduction. Head reduction avoids the problems with weak-head reduction and extensionality, while our operational semantics and associated abstract machines show us how to retain weak-head reduction's ease of implementation.
- Subjects :
- Mathematics
QA1-939
Electronic computers. Computer science
QA75.5-76.95
Subjects
Details
- Language :
- English
- ISSN :
- 20752180
- Volume :
- 212
- Issue :
- Proc. WoC 2015
- Database :
- Directory of Open Access Journals
- Journal :
- Electronic Proceedings in Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- edsdoj.0b85ad98050f47fea9a4c606deefa12b
- Document Type :
- article
- Full Text :
- https://doi.org/10.4204/EPTCS.212.2