  The field of implicit complexity has recently produced several
bounded-complexity programming languages. This kind of language allows to
implement exactly the functions belonging to a certain complexity class. We
here present a realizability semantics for a higher-order functional language
based on a fragment of linear logic called LAL which characterizes the
complexity class PTIME. This language features recursive types and higher-order
store. Our realizability is based on biorthogonality, step-indexing and is
moreover quantitative. This last feature enables us not only to derive a
semantical proof of termination, but also to give bounds on the number of
computational steps needed by typed programs to terminate.
