The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value

Thomas Ehrhard; Giulio Guerrieri

doi:10.1145/2967973.2968608

The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value

Thomas Ehrhard, Giulio Guerrieri

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

42 Citations (SciVal)

Abstract

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.

Original language	English
Title of host publication	Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
Publisher	Association for Computing Machinery
Pages	174-187
Number of pages	14
ISBN (Electronic)	9781450341486
DOIs	https://doi.org/10.1145/2967973.2968608
Publication status	Published - 5 Sept 2016
Event	18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 - Edinburgh, UK United Kingdom Duration: 5 Sept 2016 → 7 Sept 2016

Conference

Conference	18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
Country/Territory	UK United Kingdom
City	Edinburgh
Period	5/09/16 → 7/09/16

Funding

This work has been partially supported by the French-Chinese project ANR-11-IS02-0002 and NSFC 61161130530 Locali, and by the A?MIDEX project ANR-11-IDEX-0001-02 funded by the "Investissements d'Avenir" French Government program, managed by the French National Research Agency (ANR).

Keywords

Box
Call-by-name
Call-by-push-value
Call-by-value
Clash
Denotational semantics
Girard's translations
Lambda-calculus
Linear logic
Relational model
Sigma-reduction
Taylor expansion

ASJC Scopus subject areas

Software
Computational Theory and Mathematics
Computer Science Applications

Access to Document

10.1145/2967973.2968608

Cite this

The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value. / Ehrhard, Thomas; Guerrieri, Giulio.
Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016. Association for Computing Machinery, 2016. p. 174-187.

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Ehrhard, T & Guerrieri, G 2016, The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value. in Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016. Association for Computing Machinery, pp. 174-187, 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016, Edinburgh, UK United Kingdom, 5/09/16. https://doi.org/10.1145/2967973.2968608

@inproceedings{1a91b5175ef049a5a5e6c44c10559f5f,

title = "The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value",

abstract = "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.",

keywords = "Box, Call-by-name, Call-by-push-value, Call-by-value, Clash, Denotational semantics, Girard's translations, Lambda-calculus, Linear logic, Relational model, Sigma-reduction, Taylor expansion",

author = "Thomas Ehrhard and Giulio Guerrieri",

year = "2016",

month = sep,

day = "5",

doi = "10.1145/2967973.2968608",

language = "English",

pages = "174--187",

booktitle = "Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016",

publisher = "Association for Computing Machinery",

address = "USA United States",

note = "18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 ; Conference date: 05-09-2016 Through 07-09-2016",

}

TY - GEN

T1 - The bang calculus

T2 - 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016

AU - Ehrhard, Thomas

AU - Guerrieri, Giulio

PY - 2016/9/5

Y1 - 2016/9/5

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

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

KW - Box

KW - Call-by-name

KW - Call-by-push-value

KW - Call-by-value

KW - Clash

KW - Denotational semantics

KW - Girard's translations

KW - Lambda-calculus

KW - Linear logic

KW - Relational model

KW - Sigma-reduction

KW - Taylor expansion

UR - https://www.scopus.com/pages/publications/84991052032

U2 - 10.1145/2967973.2968608

DO - 10.1145/2967973.2968608

M3 - Chapter in a published conference proceeding

AN - SCOPUS:84991052032

SP - 174

EP - 187

BT - Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016

PB - Association for Computing Machinery

Y2 - 5 September 2016 through 7 September 2016

ER -

The bang calculus: An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value

Abstract

Conference

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this