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

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

8 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

Fingerprint Dive into the research topics of 'Head reduction and normalization in a call-by-value lambda-calculus'. Together they form a unique fingerprint.

Cite this