### 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 | 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

### Cite this

*13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015*(Vol. 38, pp. 211-225). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TLCA.2015.211

**Standardization of a call-by-value lambda-calculus.** / Guerrieri, Giulio; Paolini, Luca; Della Rocca, Simona Ronchi.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015.*vol. 38, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 211-225, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, Warsaw, Poland, 1/07/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.211

}

TY - GEN

T1 - Standardization of a call-by-value lambda-calculus

AU - Guerrieri, Giulio

AU - Paolini, Luca

AU - Della Rocca, Simona Ronchi

PY - 2015/7/1

Y1 - 2015/7/1

N2 - 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.

AB - 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.

KW - Call-by-value

KW - Head reduction

KW - Internal reduction

KW - Lambda-calculus

KW - Observational equivalence

KW - Parallel reduction

KW - Potential valuability

KW - Sequentialization

KW - Sigma-reduction

KW - Solvability

KW - Standardization

UR - http://www.scopus.com/inward/record.url?scp=84958690521&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.TLCA.2015.211

DO - 10.4230/LIPIcs.TLCA.2015.211

M3 - Conference contribution

VL - 38

SP - 211

EP - 225

BT - 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015

A2 - Altenkirch, Thorsten

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -