by R.A.G. Seely
Abstract:
We present a logical calculus which imposes a grading on a sequent-style
calculus to account for the runtime of the programmes represented by the
sequents. This system is sound for a notion of polynomial-time
realizability. An extension of the grading is also considered, giving
a notion of ``dependant grades'', which is also sound. Furthermore, we
define a notion of closed graded multicategory, and show how the structure of
polynomial-time realizers has that structure.
This appeared in Springer Lecture Notes in Computer Science 389, pp 182 - 197.