The bang calculus revisited.

Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a term language connecting CBPV and Linear Logic. This paper presents a revisited version of the Bang Calculus, called λ !, enjoying some important properties missing in the original formulation. Indeed, the new calculus integrates permutative conversions to unblock value redexes while preserving confluence. A second contribution is related to non-idempotent types. We provide a quantitative type system for our λ !-calculus, giving upper bounds to the length of the reduction to normal form plus its size. We also explore the properties of this type system with respect to CBN/CBV translations. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound into two independent exact measures for the reduction length and the normal form size respectively. [ABSTRACT FROM AUTHOR]