Title:Efficient first order functional program
      interpreter with time bound certifications.
Authors:J.-Y. Marion, J.-Y. Moyen

Abstract:

We demonstrate that the class of  first order functional programs over
lists
which terminate by multiset path ordering and admit a polynomial
quasi-interpretation, is exactly the class of function computable in
polynomial time.
The interest of this result lies
(i) on the simplicity
of the conditions on programs to certify their complexity,
(ii) on the fact that an important class of natural programs is
captured,
(iii) and on  potential applications on program optimizations.