Speaker:  Thomas Ehrhard CNRS, PPS  Universite' Paris Diderot  Paris 7


Quando:  16/10/2015  11:00


Dove:  Dipartimento di Matematica e Fisica, Univ. Roma Tre,
Largo San Leonardo Murialdo, 1
edificio C, terzo piano, aula 311


Abstract
There are two well known translations of the lambdacalculus into the multiplicativeexponential fragment of linear logic: the callbyname and the callbyvalue translations. The former is the standard "Girard's translation" and the latter was called "boring" by Girard in his seminal LL paper. We shall see how one can extend the lambdacalculus with simple constructions inspired by linear logic in order to factorize these translation through a single functional language admittedly much simpler than proof nets, and where weakening and contraction remain implicit. This calculus bears some similarities with Paul Levy's "callbypushvalue" and, just as the LL translation of classical systems, gives an essential role to the category of coalgebras of the exponential "!". It corresponds to a kind of halfpolarized version of linear logic. 