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

12 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