Bounded Linear Logic, Revisited

Abstract

We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.

Cited by in corpus (7)

• Characterizing co-NL by a group action
• Church => Scott = Ptime: an application of resource sensitive realizability
• Unification and Logarithmic Space
• From bounded affine types to automatic timing analysis
• Polynomial Time and Dependent Types
• A graded dependent type system with a usage-aware semantics (extended version)
• Quantitative classical realizability