a) completeness of continuation semantics for the lambda-mu-calculus (a proof term assignment for classical logic)
in a LiCS'97 paper by Hofmann and Streicher it has been shown that the call-by-name lambda-mu-calculus (of Parigot, Ong et. al.) is complete w.r.t. a simple continuation semantics; the key idea of the proof is to show that the term model is isomorphic to a continuation model over an appropriate syntactically defined category of continuations; from a more practical point of view this means that a certain simple CPS-translation to a fragment of ordinary simply typed lambda calculus provides a viable alternative to reasoning in the somewhat unorthodox formal systems of Parigot and Ong; an analogous treatment of a call-by-value variant of lambda-mu-calculus (by Ong and Stewart) is under preparation.
b) conservativity results for higher order extensions of first order theories of feasible computation.
Hofmann has worked on a research programme aimed at extending Bellantoni-Cook's recursion-theoretic characterisations for polynomial time to a fully-fledged higher-order typed functional programming language. He has designed a modal/linear lambda calculus which provides an extension of the Bellantoni-Cook framework to higher types. The purpose of modality is to provide a higher-order analogue for the safe and normal values crucial to the Bellantoni-Cook framework. The purpose of the linear types is to provide a tame version of primitive recursion with functional result type which does not lead beyond PTIME. Using this recursion patterns many algorithms admit a more natural formulation.
At CSL '97 [H1] Hofmann has presented the calculus and its syntactic metatheory such as existence of minimal types and decidability of typechecking. In [H2] he has presented a category-theoretic semantics which interprets the modal fragment of this calculus and shows that all definable functions are in PTIME. An extension of this semantics to the full calculus including linear types is in preparation.
c) The joint work with Naraschewski et al. on verification of object-oriented programs in type theory has been successfully completed and led to the publication [NH+].
[H1] Martin Hofmann. A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. Presented at Computer Science Logic '97, Aarhus, Denmark. To appear in the refereed proceedings. 1997.
[H2] Martin Hofmann. An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. To appear in Bulletin of Symbolic Logic. 1998.
[NH+] M. Hofmann and W. Naraschewski and M. Steffen and T. Stroup. Inheritance of Proofs. To appear in Theory and Pratice of Object-Oriented Systems.