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.
linear types type system complexity theory higher-order function resources