Head reduction and normalization in a call-by-value lambda-calculus

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

7 Citations (Scopus)

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 languageEnglish
Title of host publication2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015
EditorsSantiago Escobar, David Sabel, Yuki Chiba, Naoki Nishida, Manfred Schmidt-Schauss
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages3-17
Number of pages15
Volume46
ISBN (Electronic)9783939897941
DOIs
Publication statusPublished - 1 Jan 2015
Event2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 - Warsaw, Poland
Duration: 2 Jul 2015 → …

Conference

Conference2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015
CountryPoland
CityWarsaw
Period2/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

Cite this

Guerrieri, G. (2015). Head reduction and normalization in a call-by-value lambda-calculus. In S. Escobar, D. Sabel, Y. Chiba, N. Nishida, & M. Schmidt-Schauss (Eds.), 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 (Vol. 46, pp. 3-17). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/OASIcs.WPTE.2015.3