by R.A.G. Seely
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.