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

8 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