Bounded Linear Logic: A Modular Approach to Polynomial Time Computability
Jean-Yves Girard, Andre Scedrov, Philip James Scott · Birkhäuser Boston eBooks · 1990
Typing is a way of describing the interactive behavior of algorithms. Usual typing systems are mainly concerned with input-output specifications, e.g., given terms f : A ⇒ B and a : A, the computation of f ( a ) by normalization yields a result of type B. However, one can dream of more refined typings that would not only ensure ethereal termination, but would for instance yield feasible resource bounds. It seems that time complexity does not lend itself naturally to modular manipulation. We seek something more primitive.