Cari tutti,
il prossimo seminario del gruppo di ricerca in “Logica e Geometria della Cognizione” avrà luogo questo venerdì presso il dipartimento di Matematica e Fisica, l.go S.Leonardo Murialdo 1, alle ore 11 in aula 311 (edificio C, terzo piano).

Thomas Ehrhard (CNRS, PPS - Universite' Paris Diderot - Paris 7)
Linear logic, polarization and evaluation strategies

Abstract:
There are two well known translations of the lambda-calculus into the multiplicative-exponential fragment of linear logic: the call-by-name and the call-by-value 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 lambda-calculus 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 "call-by-push-value" 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 half-polarized version of linear logic.