An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value
Giulio Guerrieri
I2M, Aix-Marseille Université
https://www.irif.fr/~giuliog/
Date(s) : 26/05/2016 iCal
11h00 - 12h00
We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of Call-By-Push-Value, subsumes both Call-By-Name and Call-By-Value lambda-calculi, factorizing the Girard’s translations of these calculi in Linear Logic. We build a denotational model of the Bang Calculus based on the relational interpretation of Linear Logic and prove an adequacy theorem by means of a resource Bang Calculus whose design is based on Differential Linear Logic.
Catégories
