Vendredi 6 Mars
Heure: 
11:00  12:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
The Plotkin's callbyvalue lambdacalculus from a linearlogical viewpoint 
Description: 
Giulio Guerrieri We translate the terms of ordinary lambdacalculus into proofnets accordingly the Girard's callbyvalue "boring'' encoding of intuitionistic implication A>B = !Ao!B. We show that (1) the Plotkin's callbyvalue betareduction is (bi)simulated in proofnets via cutelimination; (2) there is a sequentialization theorem that characterizes all and only the proofnets which are translations of some lambdaterm; (3) the equivalence relation on lambdaterms which identifies lambdaterms having the same translation in proofnets is the callbyvalue counterpart of Regnier's sigmaequivalence and is not included in Plotkin's callbyvalue betaequivalence. The semantics of lambdaterms is preserved by our callbyvalue sigmaequivalence. Adding an oriented version of the callbyvalue sigmarules to the callbyvalue betareduction (and keeping the same syntax of ordinary lambdacalculus) we preserve confluence and we get a callbyvalue operational characterization of solvable and potential valuable terms (this is not possible in original Plotkin's callbyvalue lambdacalculus). 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 resourcesensitive calculus in which the elements of the model are definable. 

