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

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