Abstract: | We study a theory PTO(λη) of polynomial time computability on the type of binary strings (in the style of [6]), as embedded in full lambda calculus with total application and extensionality. We prove that the closed terms of (provable) type W → W are exactly the polynomial time operations. This answers a conjecture of Strahm [13]. |