Standardization of a call-by-value lambda-calculus

Giulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

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 languageEnglish
Title of host publication13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015
EditorsThorsten Altenkirch
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages211-225
Number of pages15
Volume38
ISBN (Electronic)9783939897873
DOIs
Publication statusPublished - 1 Jul 2015
Event13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 - Warsaw, Poland
Duration: 1 Jul 20153 Jul 2015

Conference

Conference13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015
CountryPoland
CityWarsaw
Period1/07/153/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

Guerrieri, G., Paolini, L., & Della Rocca, S. R. (2015). Standardization of a call-by-value lambda-calculus. In T. Altenkirch (Ed.), 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.

13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. ed. / Thorsten Altenkirch. Vol. 38 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. p. 211-225.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Guerrieri, G, Paolini, L & Della Rocca, SR 2015, Standardization of a call-by-value lambda-calculus. in T Altenkirch (ed.), 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
Guerrieri G, Paolini L, Della Rocca SR. Standardization of a call-by-value lambda-calculus. In Altenkirch T, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. Vol. 38. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2015. p. 211-225 https://doi.org/10.4230/LIPIcs.TLCA.2015.211
Guerrieri, Giulio ; Paolini, Luca ; Della Rocca, Simona Ronchi. / Standardization of a call-by-value lambda-calculus. 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. editor / Thorsten Altenkirch. Vol. 38 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. pp. 211-225
@inproceedings{9b14afff29694084bc55148b48541fa2,
title = "Standardization of a call-by-value lambda-calculus",
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.",
keywords = "Call-by-value, Head reduction, Internal reduction, Lambda-calculus, Observational equivalence, Parallel reduction, Potential valuability, Sequentialization, Sigma-reduction, Solvability, Standardization",
author = "Giulio Guerrieri and Luca Paolini and {Della Rocca}, {Simona Ronchi}",
year = "2015",
month = "7",
day = "1",
doi = "10.4230/LIPIcs.TLCA.2015.211",
language = "English",
volume = "38",
pages = "211--225",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
address = "Germany",

}

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 -