Abstract
We study an extension of Plotkin's call-by-value lambda-calculus by means of two commutation rules (sigma-reductions). Recently, it has been proved that this extended calculus provides elegant characterizations of many semantic properties, as for example solvability. We prove a standardization theorem for this calculus by generalizing Takahashi's approach of parallel reductions. The standardization property allows us to prove that our calculus is conservative with respect to the Plotkin's one. In particular, we show that the notion of solvability for this calculus coincides with that for Plotkin's call-by-value lambda-calculus.
| Original language | English |
|---|---|
| Title of host publication | 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 |
| Editors | Thorsten Altenkirch |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 211-225 |
| Number of pages | 15 |
| Volume | 38 |
| ISBN (Electronic) | 9783939897873 |
| DOIs | |
| Publication status | Published - 1 Jul 2015 |
| Event | 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 - Warsaw, Poland Duration: 1 Jul 2015 → 3 Jul 2015 |
Conference
| Conference | 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 |
|---|---|
| Country/Territory | Poland |
| City | Warsaw |
| Period | 1/07/15 → 3/07/15 |
Keywords
- Call-by-value
- Head reduction
- Internal reduction
- Lambda-calculus
- Observational equivalence
- Parallel reduction
- Potential valuability
- Sequentialization
- Sigma-reduction
- Solvability
- Standardization
ASJC Scopus subject areas
- Software