We present QBAL, an extension of Girard, Scedrov and Scott's bounded linearlogic. The main novelty of the system is the possibility of quantifying overresource variables. This generalization makes bounded linear logic considerablymore flexible, while preserving soundness and completeness for polynomial time.In particular, we provide compositional embeddings of Leivant's RRW andHofmann's LFPL into QBAL.
展开▼
