Linear types and non-size-increasing polynomial time computation

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.

Authors

• Martin Hofmann

Keywords

• Complexity theory
• Type system
• Linear types
• Higher-order function
• Resources