eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-06-17
3
17
10.4230/OASIcs.WPTE.2015.3
article
Head reduction and normalization in a call-by-value lambda-calculus
Guerrieri, Giulio
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.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol046_wpte2015/OASIcs.WPTE.2015.3/OASIcs.WPTE.2015.3.pdf
sequentialization
lambda-calculus
sigma-reduction
call-by-value
head reduction
internal reduction
(strong) normalization
evaluation
confluence