FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
The Bang Calculus and the Two Girard's Translations

Authors: Giulio Manzonetto and Giulio Guerrieri

Paper Information

Title:The Bang Calculus and the Two Girard's Translations
Authors:Giulio Manzonetto and Giulio Guerrieri
Proceedings:Linearity/TLLA Pre-proceedings
Editors: Maribel Fernandez, Valeria de Paiva, Thomas Ehrhard and Lorenzo Tortora De Falco
Keywords:lambda calculus, call-by-push value, operational semantics, denotational semantics, linear logic, Girard's translations, call-by-value, call-by-name
Abstract:

ABSTRACT. 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 the 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 both a syntactic and a semantic point of view.

Pages:12
Talk:Jul 07 09:55 (Session 23I)
Paper: