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