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 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.
