, If p ? ? ST, then it computes a second order function over words in MPT

S. Cook and A. Urquhart, Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic, vol.63, issue.2, pp.103-200, 1993.

M. Bruce, F. Kapron, and . Steinberg, Type-two polynomial-time and restricted lookahead, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pp.579-588, 2018.

J. Marion, A type system for complexity flow analysis, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp.123-132, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591853