Characterising Polytime through higher type Recursion
Résumé
It is shown how to restrict recursion on notation in all finite types so as to characterise the polynomial time computable functions. The restrictions are obtained by enriching the type structure with the formation of types $!\sigma$, and by adding linear concepts to the lambda calculus.