Abstract
Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
| Original language | English |
|---|---|
| Title of host publication | 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 |
| Editors | Santiago Escobar, David Sabel, Yuki Chiba, Naoki Nishida, Manfred Schmidt-Schauss |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 3-17 |
| Number of pages | 15 |
| Volume | 46 |
| ISBN (Electronic) | 9783939897941 |
| DOIs | |
| Publication status | Published - 1 Jan 2015 |
| Event | 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 - Warsaw, Poland Duration: 2 Jul 2015 → … |
Conference
| Conference | 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 |
|---|---|
| Country/Territory | Poland |
| City | Warsaw |
| Period | 2/07/15 → … |
Keywords
- (strong) normalization
- Call-by-value
- Confluence
- Evaluation
- Head reduction
- Internal reduction
- Lambda-calculus
- Reduction strategy
- Sequentialization
- Sigma-reduction
ASJC Scopus subject areas
- Geography, Planning and Development
- Modelling and Simulation