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.
Bounded Linear Logic, Revisited / U. Dal Lago; M. Hofmann. - STAMPA. - 5608:(2009), pp. 80-94. (Intervento presentato al convegno Typed Lambda Calculi and Applications, 9th International Conference tenutosi a Brasilia, Brasil nel July 1-3 2009).
Bounded Linear Logic, Revisited
DAL LAGO, UGO;
2009
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
