Martin Hofmann

TCS Journal 2018 Journal Article

Foreword

• Martin Hofmann
• David Aspinall
• Brian Campbell
• Ian Stark
• Perdita Stevens

TCS Journal 2014 Journal Article

Revisiting the categorical interpretation of dependent type theory

• Pierre-Louis Curien
• Richard Garner
• Martin Hofmann

We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

GandALF Workshop 2012 Workshop Paper

Learn with SAT to Minimize Büchi Automata

• Stephan Barth
• Martin Hofmann

We describe a minimization procedure for nondeterministic Büchi automata (NBA). For an automaton A another automaton A_min with the minimal number of states is learned with the help of a SAT-solver. This is done by successively computing automata A' that approximate A in the sense that they accept a given finite set of positive examples and reject a given finite set of negative examples. In the course of the procedure these example sets are successively increased. Thus, our method can be seen as an instance of a generic learning algorithm based on a "minimally adequate teacher'' in the sense of Angluin. We use a SAT solver to find an NBA for given sets of positive and negative examples. We use complementation via construction of deterministic parity automata to check candidates computed in this manner for equivalence with A. Failure of equivalence yields new positive or negative examples. Our method proved successful on complete samplings of small automata and of quite some examples of bigger automata. We successfully ran the minimization on over ten thousand automata with mostly up to ten states, including the complements of all possible automata with two states and alphabet size three and discuss results and runtimes; single examples had over 100 states.

TCS Journal 2011 Journal Article

Realizability models and implicit complexity

• Ugo Dal Lago
• Martin Hofmann

New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs).

TCS Journal 2007 Journal Article

A program logic for resources

• David Aspinall
• Lennart Beringer
• Martin Hofmann
• Hans-Wolfgang Loidl
• Alberto Momigliano

We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have predictable resource behaviour. This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination; it too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics. The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs.

TCS Journal 2006 Journal Article

Preface

• Martin Hofmann
• Hans-Wolfgang Loidl

TCS Journal 2004 Journal Article

An arithmetic for non-size-increasing polynomial-time computation

• Klaus Aehlig
• Ulrich Berger
• Martin Hofmann
• Helmut Schwichtenberg

An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Gödel's T and therefore defines a non-size-increasing polynomial time computable function.

I&C Journal 2003 Journal Article

Linear types and non-size-increasing polynomial time computation

• Martin Hofmann

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.

TCS Journal 2003 Journal Article

Preface

• Jiřı́ Adámek
• Martı́n Escardó
• Martin Hofmann

I&C Journal 2002 Journal Article

Completeness of Continuation Models for λμ-Calculus

• Martin Hofmann
• Thomas Streicher

We show that a certain simple call-by-name continuation semantics of Parigot's λμ-calculus is complete. More precisely, for every λμ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λμ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λμ-category in the sense of L. Ong (1996, in “Proceedings of LICS '96, ” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation, ” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λμ developed by C. -H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997, ” Assoc. Comput. Mach. Press, New York).

I&C Journal 2002 Journal Article

Type Destructors

• Martin Hofmann
• Benjamin C. Pierce

We study a variant of System F ≤ that integrates and generalizes several existing proposals for calculi with “structural typing rules. ” To the usual type constructors (→, ×, All, Some, Rec) we add a number of type destructors, each internalizing a useful fact about the subtyping relation. For example, in F ≤ with products every closed subtype of a product S×T must itself be a product S′×T′ with S′<: S and T′<: T. We internalise this observation by introducing type destructors. 1 and. 2 and postulating an equivalence T=ηT. 1×T. 2 whenever T<: U×V (including, for example, when T is a variable). In other words, every subtype of a product type literally is a product type, modulo η-conversion. Adding type destructors provides a clean solution to the problem of polymorphic update without introducing new term formers, new forms of polymorphism, or quantification over type operators. We illustrate this by giving elementary presentations of two well-known encodings of objects, one based on recursive record types and the other based on existential packages. The formulation of type destructors poses some tricky meta-theoretic problems. We discuss two different variants: an “ideal” system where both constructors and destructors appear in general forms, and a more modest system, F ≤ TD, which imposes some restrictions in order to achieve a tractable metatheory. The properties of the latter system are developed in detail.

TCS Journal 1996 Journal Article

On behavioural abstraction and behavioural satisfaction in higher-order logic

• Martin Hofmann
• Donald Sannella

The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al. , is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.

I&C Journal 1996 Journal Article

Positive Subtyping

• Martin Hofmann
• Benjamin C. Pierce

The statementS⩽Tin aλ-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[lsqb; T]] that extracts the “Tpart” of an element ofS. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to include both the implicit coercion and an overwriting functionput[S, T]∈[[S]]→[[T]]→[[S]] that updates theTpart of an element ofS. We give a realizability model and a sound equational theory for a second-order calculus of positive subtyping. Though weaker than familiar calculi of bounded quantification, positive subtyping retains 1? sufficient power to model objects, encapsulation, and message passing, and inheritance. The equational laws relating the behavior of coercions andputfunctions can be used to prove simple properties of the resulting? classes in such a way that proofs for superclasses are “inherited” by subclasses.