Some papers of Martin Hofmann on Resource Bounded
Computation

Static prediction of heap space usage for firstorder functional programs
joint work with Steffen Jost,
accepted for POPL'03
 The strength of non sizeincreasing computation
ps , pdf
Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, 2002
 We study the expressive power nonsize increasing recursive
definitions over lists. This notion of computation is such that the
size of all intermediate results will automatically be bounded by the
size of the input so that the interpretation in a finite model is
sound with respect to the standard semantics. Many wellknown
algorithms with this property such as the usual sorting algorithms
are definable in the system in the natural way. The main result is
that a characteristic function is definable if and only if it is
computable in time O(2^{p(n)}) for some polynomial p.
The method used to establish the lower bound on the expressive power
also shows that the complexity becomes polynomial time if we allow
primitive recursion only. This settles an open question posed by
AehligSchwichtenberg and by the author in "Linear types and non
sizeincreasing ...".
The key tool for establishing upper bounds on the complexity of
derivable functions is an interpretation in a finite relational model
whose correctness with respect to the standard interpretation is
shown using a semantic technique.

Linear types and nonsize increasing polynomial
time computation.
Expanded journal version of the LICS'99 paper described
below. To appear in Theoretical Computer Science.

A type system for bounded space and functional
inplace update or "how to compile functional
programs into malloc()free C"
To appear in the Nordic Journal of Computing.
A previous version was presented at ESOP '00.

We show how linear typing can be used to obtain functional programs
which modify heapallocated data structures in place.
We present this both as a ``design pattern'' for writing Ccode in a
functional style and as a compilation process from linearly typed
firstorder functional programs into malloc()free C code.
The main technical result is the correctness of this compilation.
The crucial innovation over previous linear typing schemes consists of
the introduction of a resource type <> which controls the
number of constructor symbols such as "cons" in recursive definitions
and ensures linear space while restricting expressive power
surprisingly little.
While the space efficiency brought about by the new typing scheme and
the compilation into C can also be realised by with stateoftheart
optimising compilers for functional languages such as Ocaml the
present method provides guaranteed bounds on heap space which will be
of use for applications such as languages for embedded systems or
automatic certification of resource bounds.
We show that the functions expressible in the system are precisely
those computable on a linearly spacebounded Turing machine with an
unbounded stack. By a result of Cook this equals the complexity class
'exponential time'. A tail recursive fragment of the language captures
the complexity class 'linear space'.
We discuss various extensions, in particular an extension with
FIFO queues admitting constant time catenation and enqueuing, and an
extension of the type system to fullyfledged intuitionistic linear
logic.

Linear types and nonsizeincreasing polynomial time computation.
Proceedings of LICS '99

We propose a linear type system with recursion operators for inductive
datatypes which ensures that all definable functions are polynomial
time computable. The system improves upon previous such systems in
that recursive definitions can be arbitrarily nested, in particular no
predicativity or modality restrictions are made.

Type systems for polynomialtime computation.
Habilitation thesis. Darmstadt, 1999. Appeared as LFCS Technical
Report ECSLFCS99406. An abridged and updated
version will appear
under the title Safe recursion with higher types and BCK algebra in
Annals of Pure and Applied Logic.

This thesis introduces and studies a typed lambda calculus with
higherorder primitive recursion over inductive datatypes
which have the property
that all definable numbertheoretic functions are polynomial time
computable. This is achieved by imposing typetheoretic restrictions
on the way results of recursive calls can be used.
The main technical result is the proof of the characteristic property
of this system. It proceeds by exhibiting a categorytheoretic model
in which all morphisms are polynomial time computable by construction.
The second more subtle goal of the thesis is to illustrate the
usefulness of this semantic technique as a means for guiding the
development of syntactic systems, in particular typed lambda calculi,
and to study their metatheoretic properties.
Minor results are a type checking algorithm for the lambda calculus
and the construction of combinatory algebras consisting of polynomial
time algorithms in the style of the first Kleene algebra.
Back to the main project page.
Page created by copying and pasting from
Martin Hofmann's Publications and Preprints page
by Michal Konecny
Last modified: Fri Jan 31 19:09:09 GMT 2003