We present a forward sequent calculus for intuitionistic propositional linear logic (⊗, 1, &, T, ¯°, ⊕, 0, !) and a corresponding inverse-method search strategy. Our approach centres around resource management, inspired by similar approaches for backward-directed calculi such as top-down linear logic programming. Surprisingly, the resource management problems for the forward direction turn out to have a different character to those of the backward direction, arising for different connectives. Our approach identifies conditions for which we may relax linearity to allowing (implicit) weakening. We characterize two such classes of affine behaviour as a form of weak sequent designed to handle T-weakening lazily, and as affine contexts to control the multiplicative unit 1 using a general matching framework.

26 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu