We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: The Bang Calculus Revisited

Abstract: Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The paradigm was recently modelled by means of the Bang Calculus, a term language connecting CBPV and Linear Logic.
This paper presents a revisited version of the Bang Calculus, called $\lambda !$, enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to non-idempotent types. We provide a quantitative type system for our $\lambda !$-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form \emph{plus} the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from $\lambda$-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a \emph{tight} one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent \emph{exact} measures for them.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
DOI: 10.1007/978-3-030-59025-3\_2
Cite as: arXiv:2002.04011 [cs.LO]
  (or arXiv:2002.04011v2 [cs.LO] for this version)

Submission history

From: Andrés Ezequiel Viso [view email]
[v1] Mon, 10 Feb 2020 18:38:00 GMT (60kb)
[v2] Tue, 8 Sep 2020 13:02:32 GMT (63kb)

Link back to: arXiv, form interface, contact.