The bang calculus

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

Thomas Ehrhard, Giulio Guerrieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)

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 languageEnglish
Title of host publicationProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
PublisherAssociation for Computing Machinery
Pages174-187
Number of pages14
ISBN (Electronic)9781450341486
DOIs
Publication statusPublished - 5 Sep 2016
Event18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 - Edinburgh, UK United Kingdom
Duration: 5 Sep 20167 Sep 2016

Conference

Conference18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
CountryUK United Kingdom
CityEdinburgh
Period5/09/167/09/16

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

Cite this

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 (pp. 174-187). Association for Computing Machinery. https://doi.org/10.1145/2967973.2968608

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 in Book/Report/Conference proceedingConference contribution

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
Ehrhard T, Guerrieri G. 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. 2016. p. 174-187 https://doi.org/10.1145/2967973.2968608
Ehrhard, Thomas ; Guerrieri, Giulio. / The bang calculus : An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value. Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016. Association for Computing Machinery, 2016. pp. 174-187
@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 = "9",
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",

}

TY - GEN

T1 - The bang calculus

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

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 - http://www.scopus.com/inward/record.url?scp=84991052032&partnerID=8YFLogxK

U2 - 10.1145/2967973.2968608

DO - 10.1145/2967973.2968608

M3 - Conference contribution

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

ER -