Paper: Polynomially graded logic I. A graded version of system T (at LICS 1989)

Authors: Anil Nerode Jeffrey B. Remmel Andre Scedrov

Abstract

An investigation is made of a logical framework for programming languages which treats requirements on computation resources as part of the formal program specification. Resource bounds are explicit in the syntax of all programs. In a programming language based on this approach, compliance of a program with imposed resource bounds would be assured by verifying the syntactic correctness using a compiler with a static type checking feature. The principal innovation is the introduction of systems of logical inference, called polynomially graded logics. These logics make resource bounds part of every proposition and every deduction. The sample calculus presented is a restriction of Godel's system T to polynomial time resources. It is proved that the numerical functions representable in this calculus are exactly the PTIME functions

BibTeX

  @InProceedings{NerodeRemmelScedrov-Polynomiallygradedl,
    author = 	 {Anil Nerode and Jeffrey B. Remmel and Andre Scedrov},
    title = 	 {Polynomially graded logic I. A graded version of system T},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {375--385},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }