Vendredi 6 Mars

Retour à la vue des calendrier
Vendredi 6 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: The Plotkin's call-by-value lambda-calculus from a linear-logical viewpoint
Description: Giulio Guerrieri We translate the terms of ordinary lambda-calculus into proof-nets
accordingly the Girard's call-by-value "boring'' encoding of intuitionistic
implication A->B = !A-o!B. We show that (1) the Plotkin's call-by-value
beta-reduction is (bi)simulated in proof-nets via cut-elimination; (2)
there is a sequentialization theorem that characterizes all and only the
proof-nets which are translations of some lambda-term; (3) the equivalence
relation on lambda-terms which identifies lambda-terms having the same
translation in proof-nets is the call-by-value counterpart of Regnier's
sigma-equivalence and is not included in Plotkin's call-by-value
beta-equivalence. The semantics of lambda-terms is preserved by our
call-by-value sigma-equivalence.
Adding an oriented version of the call-by-value sigma-rules to the
call-by-value beta-reduction (and keeping the same syntax of ordinary
lambda-calculus) we preserve confluence and we get a call-by-value
operational characterization of solvable and potential valuable terms (this
is not possible in original Plotkin's call-by-value lambda-calculus).
Moreover, we give a semantic characterization of solvable and potential
valuable terms in a relational model, based on Linear Logic, satisfying the
Taylor expansion formula. As a technical tool, we also use a
resource-sensitive calculus in which the elements of the model are