An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value

Giulio Guerrieri
I2M, Aix-Marseille Université

Date(s) : 26/05/2016   iCal
11 h 00 min - 12 h 00 min

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.


Retour en haut 

Secured By miniOrange