Publications and preprints
 The strength of non sizeincreasing computation
ps , pdf
Submitted.
 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.
 Realizability models for BLLlike languages ps, pdf.
with Phil Scott
Accepted for the LICS affiliated
workshop Implicit Computational Complexity
(ICC), Santa Barbara, 2829 June 2000.

We give a realizability model of GirardScedrovScott's
{\em Bounded Linear Logic} (BLL). This gives a new proof
that all numerical functions representable in that system are polytime.
Our analysis naturally justifies the design of the BLL syntax
and suggests further extensions.
 A new "feasible arithmetic" ps, pdf.
with Steve Bellantoni
To appear in JSL.

A classical quantified modal logic is used to define a ``feasible''
arithmetic whose provably total functions are exactly the
polynomialtime computable functions.
The crucial restrictions are (1) that induction is limited to
modalityfree formulas and (2) that an induction hypothesis may be
used at most once (in the sense of linear logic).
The logic is defined without any reference to bounding terms, and
admits induction over formulas having arbitrarily many alternations
of unbounded quantifiers.

Implementing a Program Logic of Objects in a HigherOrder Logic Theorem
Prover ps.gz ,
pdf .
with Francis Tang
Preprint.

We present an implementation of a program logic of objects,
extending that (AL) of Abadi and Leino. In particular, the
implementation uses higherorder abstract syntax (HOAS) and  unlike
previous approaches using HOAS  at the same time uses the builtin
higherorder logic of the theorem prover to formulate
specifications. We give examples of verifications, extending those
given in [Abadi, Leino 1997], that have been attempted with the
implementation. Due to the mixing of HOAS and builtin logic the
soundness of the encoding is nontrivial. In particular, unlike in
other HOAS encodings of program logics, it is not possible to
directly reduce normal proofs in the higherorder system to proofs
in the firstorder object logic.

Programming languages capturing complexity classes.
SIGACT News Logic Column 9

Survey article describing recent work by Bellantoni, Girard,
Goerdt, Leivant, Niggl, Schwichtenberg, the author, and others
on use of type systems to restrict programming languages
to certain complexity classes.

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.

Applications of a representation theorem to subsystems of arithmetic
with Thierry Coquand
to appear in MSCS special issue in honour of Roger Hindley's 60th
birthday.
 We use a syntactical notion of Kripke models to obtain interpretations of subsystems of
arithmetic in their intuitionistic counterparts. This yields in particular
a new proof of Buss' result that the Skolem functions of
Bounded Arithmetic are polynomial time computable.

Mediation is inherently parallel.
with
Martin Escardo and Thomas Streicher.
Draft presented at Workshop on Domains V, Darmstadt September 1999.

Let I be Scott's interval domain of closed subintervals of
[0,1] ordered by reverse inclusion. Let Sigma be the Sierpinskidomain
{__,T}. We show that if f:I x I > I is any continuous map such that on
total elements f agrees with mediation (average) then the parallel or
function on Sigma (given by wpor(x,y)=__ <=> x=y=__) can be defined
from f and a few undoubtedly sequential functions. We claim that this
shows that there can be no sequential implementation of a programming
language for exact real number computation based on Scott's interval
model.

Semantical analysis of higherorder abstract syntax
Proceedings of LICS '99

A functor category semantics for higherorder abstract syntax is
proposed with the following aims: relating higherorder and first
order syntax, justifying induction principles, suggesting new logical
principles to reason about higherorder syntax.

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 destructors.
With Benjamin
Pierce. Indiana University CSCI technical report #502. February 1998.
(A summary was presented at FOOL 4 in January, 1998.)


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.

Completeness of continuation models for lambdamucalculus.
Joint with Thomas Streicher.
To appear in Information and Computation

This is a journal version of "Continuation models are universal
..." described below. In addition to the material presented there it
contains an account of callbyvalue lambdamucalculus.

Semantics of
linear/modal lambda calculus .
Final version accepted for publication in JFP.

At CSL '97 (see below) I have introduced a lambda calculus SLR with
modal and linear types which serves as an extension of
BellantoniCook's function algebra BC to higher types. It is a step
towards a functional programming language in which all programs run in
polynomial time. While op. cit. was concerned with the
syntactic metatheory of SLR this paper develops a semantics of
SLR in terms of Chu spaces over a certain category of presheaves
from which it follows that all expressible functions are indeed
in PTIME. The alternative method of using BCK algebras of untyped
algorithms described in my habilitation thesis above is more powerful
than Chu spaces; however I hope that a compilation process based on
the Chu space interpretation would turn out to be more efficient than
one based on BCK algebras.

A mixed modal/linear lambda calculus with
applications to BellantoniCook safe recursion.
Presented at CSL '97, Aarhus, Denmark.


Continuation models are universal for lambdamucalculus
.
Joint with Thomas Streicher.
Proc. LICS '97, Warsaw, IEEE, pp. 387397.

We show that a certain simple callbyname continuation semantics of
Parigot's lambdamucalculus is complete. More precisely, for every
lambdamutheory we construct a cartesian closed category such that the
ensuing continuationstyle interpretation of lambdamu, which maps
terms to functions sending abstract continuations to responses, is
full and faithful.

An application of categorytheoretic semantics to the
characterisation of complexity classes using higherorder function
algebras
Bulletin of Symbolic Logic 3(4), Dec. 1997.

The category of presheaves over PTIMEfunctions is used in order
to show that Cook and Urquhart's higherorder function algebra
PVomega defines exactly the PTIMEfunctions. As a byproduct
a syntaxfree generalisation of PTIMEcomputability to
higher types is obtained. The technique is further applied to
intuitionistic predicate logic over PVomega and to a new
higherorder extension of BellantoniCook's system BC.

Syntax and Semantics of Dependent Types
In Semantics of Logics of
Computation, P. Dybjer and A. Pitts, eds., Cambridge University
Press. 1997.

Lecture Notes for a course held at a summerschool on Semantics and Logics of
Computation at the Newton Institute, Cambridge, September 1995.

Categorical reconstruction of a reductionfree normalisation proof
.
Joint
with
Thorsten Altenkirch
and Thomas Streicher.
Proc. CTCS '95. Cambridge, 1995. Springer
LNCS 953, pp 182199.

We define a cartesianclosed category which has the property that the
interpretation of simplytyped lambda calculus in it yields
Schwichtenberg and Berger's reductionfree
normalisation algorithm as
well as its correctness. The following two papers generalise this
approach to a combinatory version of system F and to full system F
with eta rules.

Reductionfree normalisation for a polymorphic system.
Joint
with Thorsten Altenkirch
and Thomas Streicher.
Proc. LICS '96. New Jersey, 1996. IEEE Press.


Reductionfree normalisation for system F.
Joint
with
Thorsten Altenkirch
and Thomas Streicher.
Manuscript.


Conservativity of equality reflection over
intensional type theory.
Preprint version of
Proc. BRA TYPES workshop, Torino, June 1995, Springer
LNCS 1158, pp 153  165.

It is shown that extensional MartinLöf type theory is a conservative
extension of intensional type theory augmented by two extensionality
axioms.

A simple model for quotient types .
Proc. TLCA '95, Edinburgh, April 1995, Springer Vol. 902, pp216234.

Contains an interpretation of the Calculus of Construction augmented
by quotient types in the pure Calculus of Constructions. Types are
interpreted as types together with a partial equivalence relation
("setoids"). The interpretation validates a choice principle for
quotient types which under certain syntactic restrictions allows one
to extract a representative from an equivalence class.

Positive subtyping
.
Joint with
Benjamin Pierce
Information and Computation (126)1, 1996, pp 186197.

We describe a variant of system F with records and subtyping which provides
polymorphic update functions. We give an equational axiomatisation of
these update functions and demonstrate how it can be applied to
specification and verification of Smalltalkstyle class hierarchies.

Inheritance of Proofs.
Joint with Wolfgang Naraschewski,
Martin Steffen,
and Terry Stroup.
To appear in the FOOL 3 special issue of Theory and Practice of
Software Systems (TAPOS).


A Unifying TypeTheoretic Framework for Objects.
With Benjamin
Pierce. JFP . January 1994. (Summary version appeared in
STACS '94.)


On
behavioural abstraction and behavioural satisfaction in higherorder
logic.
Joint with Don Sannella.
Presented at TAPSOFT '95, Aarhus.
Theoretical Computer Science 167 (1996), pp 345.


On the interpretation of type theory in locally
cartesian closed categories
.
Proc. CSL '94, Kazimierz, Poland. Jerzy Tiuryn and Leszek Pacholski,
eds. Springer LNCS, Vol. 933.

A problem with Seely's interpretation of dependent types in locally
cartesian closed categories is identified and solved using a general
construction due to Benabou.

Sound and complete axiomatisations of callbyvalue
control operators
.
Math. Struct. Comp. Sci. (1995), vol. 5, pp. 461482.

We formulate a typed version of callbyvalue lambdacalculus
containing variants of Felleisen's control operators A and
C which provide explicit access to continuations and logically
extend the propositionsastypes correspondence to classical
propositional logic. We give an equational theory for this calculus
which is shown to be sound and complete with respect to to a class of
categorical models based on continuationpassingstyle semantics.

A groupoid model refutes uniqueness of identity proofs
.
With Thomas Streicher.
Proceedings of the 9th Symposium on Logic in
Computer Science (LICS), Paris, 1994.

See below.

The groupoid interpretation of type theory.
With Thomas Streicher.
Preprint version of article appeared in
Proceedings of the meeting Twentyfive years of constructive type
theory, Venice, Oxford University Press, 1998.

An expanded version of the above. We describe an interpretation of
MartinLöf's type theory which interprets a type as a groupoid,
i.e. categories with isomorphisms only. This model shows that in
intensional MartinLöf type theory it is not provable that any two
elements of an identity type are equal. This entails that
patternmatching is not conservative over intensional type theory.
Furthermore, we exhibit an axiom which holds in the groupoid model yet
is inconsistent with pattern matching and with extensional type theory
or usual set theory. The axiom states that two sets are
propositionally equal iff there is a bijection between them.

Extensional concepts in intensional type theory .
PhD thesis. LFCS
Edinburgh, 1995.

Extensions of intensional MartinLöf type theory with "extensional
concepts" such as functional extensionality, quotient types, subset
types are studied.

Verifikation von MLProgrammen mit dem Beweisprüfer Lego.
Diploma thesis, Universität Erlangen, 1991.

The applicability of the proof checker Lego for structured
specification and verification of functional programs in the sense of Extended ML is explored.
In German. A revised
English version exists under the title "Formal Development of
Functional Programs in Type Theory  A Case Study" as LFCS Technical
Report No ECSLFCS92228.

Über die WeylAlgebra und das Theorem von Stafford.
Studienarbeit (term project). Universität Erlangen, 1987.

Contains an exposition of Stafford's result stating that every ideal
in the Weylalgebra (a certain algebra of linear differential
operators) can be generated by two elements. An attempt is made to
constructivise this result; in particular an example calculation is
carried out which yields two linear differential equations expressing
that a function in three variables is constant. In German.
Back to my homepage .