Bounded Linear Logic, Revisited

TL;DR

This paper introduces QBAL, an extended bounded linear logic that allows quantification over resource variables, enhancing flexibility while maintaining polynomial time soundness and completeness.

Contribution

QBAL extends bounded linear logic with resource variable quantification, enabling embeddings of other polynomial time systems and increasing expressiveness.

Findings

QBAL preserves soundness and completeness for polynomial time.

It allows embeddings of Leivant's RRW and Hofmann's LFPL.

The system enhances flexibility of bounded linear logic.

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.