May 1st, 2011

Book

Pola: a language for PTIME programming

http://projects.wizardlike.ca/projects/pola/documents

This paper describes the type system of a functional style
programming language called Pola which is complete with respect to
polynomial time programming. This means, both that every well-typed
Pola program is guaranteed to halt in time polynomial with respect to
the size of its input, and that all such polynomial time functions can be
written in Pola.

UPDATE: Но и это ещё не всё - ...there is a full type inference algorithm
for Pola programs! И они были далеко не первыми - читайте их библиографию