Publications and preprints

• The strength of non size-increasing computation ps , pdf
  Submitted.

  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.

• Realizability models for BLL-like languages ps, pdf.
  with Phil Scott
  Accepted for the LICS affiliated workshop Implicit Computational Complexity (ICC), Santa Barbara, 28-29 June 2000.

  We give a realizability model of Girard-Scedrov-Scott'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 polynomial-time computable functions. The crucial restrictions are (1) that induction is limited to modality-free 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 Higher-Order 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 higher-order abstract syntax (HOAS) and - unlike previous approaches using HOAS - at the same time uses the built-in higher-order 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 built-in 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 higher-order system to proofs in the first-order 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 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.

• 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 Sierpinski-domain {_|_,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 higher-order abstract syntax
  Proceedings of LICS '99

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

• 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 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 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.

• Completeness of continuation models for lambda-mu-calculus.
  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 call-by-value lambda-mu-calculus.

• 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 Bellantoni-Cook'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 Bellantoni-Cook safe recursion.
  Presented at CSL '97, Aarhus, Denmark.

• Continuation models are universal for lambda-mu-calculus .
  Joint with Thomas Streicher.
  Proc. LICS '97, Warsaw, IEEE, pp. 387-397.

  We show that a certain simple call-by-name continuation semantics of Parigot's lambda-mu-calculus is complete. More precisely, for every lambda-mu-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of lambda-mu, which maps terms to functions sending abstract continuations to responses, is full and faithful.

• An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras
  Bulletin of Symbolic Logic 3(4), Dec. 1997.

  The category of presheaves over PTIME-functions is used in order to show that Cook and Urquhart's higher-order function algebra PV-omega defines exactly the PTIME-functions. As a byproduct a syntax-free generalisation of PTIME-computability to higher types is obtained. The technique is further applied to intuitionistic predicate logic over PV-omega and to a new higher-order extension of Bellantoni-Cook'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 reduction-free normalisation proof .
  Joint with Thorsten Altenkirch and Thomas Streicher.
  Proc. CTCS '95. Cambridge, 1995. Springer LNCS 953, pp 182-199.

  We define a cartesian-closed category which has the property that the interpretation of simply-typed lambda calculus in it yields Schwichtenberg and Berger's reduction-free 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.

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

• Reduction-free 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 Martin-Lö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, pp216-234.

  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 186-197.

  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 Smalltalk-style 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 Type-Theoretic Framework for Objects.
  With Benjamin Pierce. JFP . January 1994. (Summary version appeared in STACS '94.)

• On behavioural abstraction and behavioural satisfaction in higher-order logic.
  Joint with Don Sannella.
  Presented at TAPSOFT '95, Aarhus. Theoretical Computer Science 167 (1996), pp 3-45.

• 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 call-by-value control operators .
  Math. Struct. Comp. Sci. (1995), vol. 5, pp. 461-482.

  We formulate a typed version of call-by-value lambda-calculus containing variants of Felleisen's control operators A and C which provide explicit access to continuations and logically extend the propositions-as-types 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 continuation-passing-style 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 Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998.

  An expanded version of the above. We describe an interpretation of Martin-Löf's type theory which interprets a type as a groupoid, i.e. categories with isomorphisms only. This model shows that in intensional Martin-Löf type theory it is not provable that any two elements of an identity type are equal. This entails that pattern-matching 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 Martin-Löf type theory with "extensional concepts" such as functional extensionality, quotient types, subset types are studied.

• Verifikation von ML-Programmen 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 ECS-LFCS-92-228.

• Über die Weyl-Algebra 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 Weyl-algebra (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.