Some papers of Martin Hofmann on Resource Bounded Computation

• Static prediction of heap space usage for first-order functional programs
  joint work with Steffen Jost, accepted for POPL'03

• The strength of non size-increasing computation ps , pdf
  Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, 2002

  We study the expressive power non-size 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 well-known 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 Aehlig-Schwichtenberg and by the author in "Linear types and non size-increasing ...". 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 non-size 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 in-place 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 heap-allocated data structures in place. We present this both as a ``design pattern'' for writing C-code in a functional style and as a compilation process from linearly typed first-order 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 state-of-the-art 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 space-bounded 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 fully-fledged intuitionistic linear logic.

• Linear types and non-size-increasing 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 polynomial-time computation.
  Habilitation thesis. Darmstadt, 1999. Appeared as LFCS Technical Report ECS-LFCS-99-406. 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 higher-order primitive recursion over inductive datatypes which have the property that all definable number-theoretic functions are polynomial time computable. This is achieved by imposing type-theoretic 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 category-theoretic 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 meta-theoretic 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.