### 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 Sep 2016 |

Event | 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 - Edinburgh, UK United Kingdom Duration: 5 Sep 2016 → 7 Sep 2016 |

### Conference

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

Country | UK United Kingdom |

City | Edinburgh |

Period | 5/09/16 → 7/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

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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 -