A Polytime-Complete Functional Language based on Light Logic

Luke Ong

After a brief survey of recent characterizations of polytime-bounded
computation, we introduce a polymorphic functional language, based on
Girard's Light Linear Logic, that is sound and complete for polytime
(numeric) functions. We give examples to show that the language
expresses many polytime algorithms and is useful as a unifying setting
in which to relate different resource-free characterizations of
polytime computable functions.