Startseite > Mitarbeiter > Martin Hofmann > Research

Research

  PUBLICATIONS and PREPRINTS

 


    THIS LIST IS INCOMPLETE AND WILL BE SUCCESSIVELY BROUGHT UP TO DATE. FOR THE TIME BEING CONSULT DBLP OR SIMILAR.
    Please ask me for preprints or PDFs of those articles that are not linked here. I will reply as soon as I can.

     

  • A Semantic Proof of Polytime Soundness of Light Affine Logic .pdf
    with Ugo Dal Lago Lecture Notes, May 2008
    We define a denotational semantics for Light Affine Logic (LAL) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL which is considerably simpler than the standard proof based on proof nets and also is entirely semantical in nature. The model construction uses a new instance of a resource monoid; a general method for interpreting variations of linear logic with complexity restrictions introduced earlier by the authors.
  • Pure Pointer Programms with Iteration .pdf
    with Ulrich Schoepp Lecture Notes, , CSL 2008, September 2008
    Many LOGSPACE algorithms are naturally described as programs that operate on a structured input (e.g. a graph), that store in memory only a constant number of pointers (e.g. to graph nodes) and that do not use pointer arithmetic. Such  pure pointer algorithms thus are a useful abstraction for studying the nature of LOGSPACE-computation. In this paper we introduce a formal class PURPLE of pure pointer programs and study them on locally ordered graphs. Existing classes of pointer algorithms, such as Jumping Automata on Graphs (JAGs) or Deterministic Transitive Closure (DTC) logic, often exclude simple programs. PURPLE subsumes these classes and allows for a natural representation of many graph algorithms that access the input graph by a constant number of pure pointers. It does so by providing a primitive for iterating an algorithm over all nodes of the input graph in an unspecified order. Since pointers are given as an abstract data type rather than as binary digits we expect that logarithmic-size worktapes cannot be encoded using pointers as is done, e.g. in totally-ordered DTC logic. We show that this is indeed the case by proving that the property  the number of nodes is a power of two, which is in LOGSPACE, is not representable in PURPLE.
  • Elimination of ghost variables in program logics .pdf
    with Mariela Pavlova
    Ghost variables are assignable variables that appear in program annotations but do not correspond to physical entities. They are used to facilitate specification and verification, e.g., by using a ghost variable to count the number of iterations of a loop, and also to express extra-functional behaviours. In this paper we give a formal model of ghost variables and show how they can be eliminated from specifications and proofs in a compositional and automatic way. Thus, with the results of this paper ghost variables can be seen as a specification pattern rather than a primitive notion.
  • Nominal Renaming Sets .pdf
    with MurdochJ. Gabbay LPAR 2008, November 2008
    Nominal techniques are based on the idea of sets with a finitely- supported atoms-permutation action. We consider the idea of nominal renaming sets, which are sets with a finitely-supported atoms-renaming action; renamings can identify atoms, permutations cannot. We show that nominal renaming sets exhibit many of the useful qualities found in (permutative) nominal sets; an elementary sets-based presentation, inductive datatypes of syntax up to binding, cartesian closure, and being a topos. Unlike is the case for nominal sets, the notion of names-abstraction coincides with functional abstraction. Thus we obtain a concrete presentation of sheaves on the category of finite sets in the form of a category of sets with structure.
  • Correctness of effect-based program transformations
    Proceedings of the Marktoberdorf summer school 2007 .pdf
  • Proof-theoretic approach to description logic
    Presented at Symp. Logic in Computer Science (LICS 2005) .pdf
    In recent work Baader has shown that a certain description logic with conjunction, existential quantification and with circular definitions has a polynomial time subsumption problem both under an interpretation of circular definitions as greatest fixpoints and under an interpretation as arbitrary fixpoints (introduced by Nebel). This was shown by translating definitions in the description logic (``TBoxes'') into a labelled transition system and by reducing subsumption to a question of the existence of certain simulations. In the case of subsumption under the descriptive semantics a new kind of simulation, called synchronised simulation, had to be introduced. In this paper, we also give polynomial-time decision procedures for these logics; this time by devising sound and complete proof systems for them and demonstrating that proof search is polynomial for these systems. We then use the proof-theoretic method to study the hitherto unknown complexity of description logic with universal quantification, conjunction, and GCI axioms. Finally, we extend the proof-theoretic method to negation and thus obtain a decision procedure for the description logic ALC with fixpoints. This last section is only sketched.
  • Static prediction of heap space usage for first-order functional programs
    Presented at Symposium on Principles of Programming Languages (POPL),
    In Proceedings of the 30th ACM SIGPLAN-SIGACT 2003, 185-197
  • The strength of non size-increasing computation .ps, .pdf
    Presented at POPL'02. Hereare the slides from 3 lectures at the 2002 Oberwolfach meeting on Mathematical Logic. .ps, .pdf
    ACM SIGPLAN Notices 37(1), 260 - 269
    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
    To appear in Theoretical Computer Science.
    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
    Appeared in Journal of Symbolic Logic 67(1), 104-116, March 2002
    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 .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
    ACM SIGACT News 31(1), 31-42, March 2000
    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 .pdf
    Expanded journal version of the LICS'99 paper described below. Appeared in Information and Computation 183(1), 57-85, 2003
  • A type system for bounded space and functional in-place update or "how to compile functional programs into malloc()-free C" .pdf
    Appeared in the Nordic Journal of Computing 7(4), 258-289, 2000. 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
    Appeared 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.
    Appeared in Math. Struct. Computer Science, 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 .pdf
    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 .pdf
    Proceedings of LICS '99
    Appeared in Information and Computation 183(1), 57 - 85, 2003
    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 .pdf
    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 .pdf
    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 .pdf
    Joint with Thomas Streicher.
    Appeared in Information and Computation 179(2), 332 - 355, 2002
    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 .pdf
    Appeared in Journal of Functional Programming 9(3), 247-277, May 1999.
    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 .pdf
    Presented at CSL '97, Aarhus, Denmark.
  • Continuation models are universal for lambda-mu-calculus .pdf
    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 .pdf
    Bulletin of Symbolic Logic 3(4), 469-486, 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 .pdf
    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 .pdf
    Joint with Thorsten Altenkirchand 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 .pdf
    Joint with Thorsten Altenkirchand Thomas Streicher.
    Proc. LICS '96. New Jersey, 1996. IEEE Press.
  • Reduction-free normalisation for system F .pdf
    Joint with Thorsten Altenkirchand 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 .pdf
    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 .pdf
    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. .pdf
    Joint with Wolfgang Naraschewski, Martin Steffen, and Terry Stroup.
    Appeared in the FOOL 3 special issue of Theory and Practice of Software Systems (TAPOS).
  • A Unifying Type-Theoretic Framework for Objects .pdf
    With Benjamin Pierce. JFP . January 1994. (Summary version 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 .pdf
    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 .pdf
    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 .pdf
    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 .pdf
    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.

 

 

Versenden Drucken
nach oben
Impressum - Datenschutz - Kontakt