The Bang Calculus and the Two Girard's Translations

Giulio Guerrieri
(Dipartimento di Informatica – Scienza e Ingegneria (DISI), Università di Bologna, Bologna, Italy)
Giulio Manzonetto
(LIPN, UMR 7030, Université Paris 13, Sorbonne Paris Cité, F-93430, Villetaneuse, France)

We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from a syntactic and a semantic viewpoint.

In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva and Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), Oxford, UK, 7-8 July 2018, Electronic Proceedings in Theoretical Computer Science 292, pp. 15–30.
Published: 15th April 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.292.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org