• DocumentCode
    342866
  • Title

    Linear types and non-size-increasing polynomial time computation

  • Author

    Hofmann, Martin

  • Author_Institution
    Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
  • fYear
    1999
  • fDate
    1999
  • Firstpage
    464
  • Lastpage
    473
  • Abstract
    We propose a linear type system with recursion operators for inductive datatypes which ensures that all definable functions are polynomial time computable. The system improves upon previous such systems in that recursive definitions can be arbitrarily nested, in particular no predicativity or modality restrictions are made
  • Keywords
    recursive functions; type theory; definable functions; inductive datatypes; linear type system; polynomial time computable; polynomial time computation; recursion operators; recursive definitions; Data structures; Electrical capacitance tomography; Law; Legal factors; Logic; Polynomials; Runtime;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1999. Proceedings. 14th Symposium on
  • Conference_Location
    Trento
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-0158-3
  • Type

    conf

  • DOI
    10.1109/LICS.1999.782641
  • Filename
    782641