Bernhard Reus

I&C Journal 2013 Journal Article

Specification patterns for reasoning about recursion through the store

• Nathaniel Charlton
• Bernhard Reus

Higher-order store means that code can be stored on the mutable heap that programs manipulate, and is the basis of flexible software that can be changed or reconfigured at runtime. Specifying such programs is challenging because higher-order store allows recursion through the store, where new (mutual) recursions between code are set up on the fly. This paper presents a series of formal specification patterns that capture increasingly complex uses of recursion through the store. To express the necessary specifications we extend the separation logic for higher-order store given by Schwinghammer et al. (CSL, 2009), adding parameter passing, and certain recursively defined families of assertions. We give proof rules for our extended logic and show their soundness. Finally, we apply our specification patterns and rules to an example program that exploits many of the possibilities offered by higher-order store; this is the first larger case study conducted with logical techniques based on work by Schwinghammer et al. (CSL, 2009), and shows that they are practical.

CSL Conference 2011 Conference Paper

Relative Completeness for Logics of Functional Programs

• Bernhard Reus
• Thomas Streicher

We prove a relative completeness result for a logic of functional programs extending D. Scott's LCF. For such a logic, contrary to results for Hoare logic, it does not make sense to ask whether it is complete relative to the full theory of its first-order part, since the first order part does not determine uniquely the model at higher-order types. Therefore, one has to fix a model and choose an appropriate data theory w. r. t. which the logic is relatively complete. We establish relative completeness for two models: for the Scott model we use the theory of Baire Space as data theory, and for the effective Scott model we take first-order arithmetic. In both cases we need to extend traditional LCF in order to capture a sufficient amount of domain theory.

CSL Conference 2009 Conference Paper

Nested Hoare Triples and Frame Rules for Higher-Order Store

• Jan Schwinghammer
• Lars Birkedal
• Bernhard Reus
• Hongseok Yang

Abstract Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several variations of higher-order frame rules. The interaction of nested triples and frame rules can be subtle, and the inclusion of certain frame rules is in fact unsound. A particular combination of rules can be shown consistent by means of a Kripke model where worlds live in a recursively defined ultrametric space. The resulting logic allows us to elegantly prove programs involving stored code. In particular, it leads to natural specifications and proofs of invariants required for dealing with recursion through the store.

CSL Conference 2006 Conference Paper

Separation Logic for Higher-Order Store

• Bernhard Reus
• Jan Schwinghammer

Abstract Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. In past work, separation logic has been developed for heaps containing records of basic data types. Languages like C or ML, however, also permit the use of code pointers. The corresponding heap model is commonly referred to as “higher-order store” since heaps may contain commands which in turn are interpreted as partial functions between heaps. In this paper we make Separation Logic and the benefits of local reasoning available to languages with higher-order store. In particular, we introduce an extension of the logic and prove it sound, including the Frame Rule that enables specifications of code to be extended by invariants on parts of the heap that are not accessed.

TCS Journal 2004 Journal Article

Semantics and logic of object calculi

• Bernhard Reus
• Thomas Streicher

The main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. Existence is not guaranteed but can be shown employing Pitts’ results on relational properties of domains. The semantics can be used to analyse and verify Abadi and Leino's object logic but it also suggests extensions. For example, specifications of methods may not only refer to fields but also to methods of objects in the store. This can be achieved without compromising the existence theorem. An informal logic of predomains is in use intentionally in order to avoid any commitment to a particular syntax of specification logic.

CSL Conference 2003 Conference Paper

Modular Semantics and Logics of Classes

• Bernhard Reus

Abstract The semantics of class-based languages can be defined in terms of objects only [1, 7, 8] if classes are viewed as objects with a constructor method. One obtains a store in which method closures are held together with field values. Such a store is also called “higher-order” and does not come for free [13]. It is much harder to prove properties of such stores and as a consequence (soundness of) programming logics can become rather contrived (see [2]). A simpler semantics separates methods from the object store [4, 12]. But again, there is a drawback. Once the semantics of a package of classes is computed it is impossible to add other classes in a compositional way. Modular reasoning principles are therefore not obtainable either. In this paper we improve a simple class-based semantics to deal with extensions compositionally and derive modular reasoning principles for a logic of classes. The domain theoretic reasoning principle behind this is fixpoint induction. Modularity is obtained by endowing the denotations of classes with an additional parameter that accounts for those classes added “later at linkage time. ” Local class definitions (inner classes) are possible but for dynamic class-loading one cannot do without higher-order store.

TCS Journal 2001 Journal Article

Preface

• Ulrich Berger
• Karl-Heinz Niggl
• Bernhard Reus

CSL Conference 1999 Conference Paper

Monadic Presentations of Lambda Terms Using Generalized Inductive Types

• Thorsten Altenkirch
• Bernhard Reus

Abstract We present a definition of untyped λ-terms using a heterogeneous datatype, i. e. an inductively defined operator. This operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for λ-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed λ-calculus using dependent types, and show that this is an instance of a generalization of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.

MFCS Conference 1993 Conference Paper

Verifying Properties of Module Construction in Type Theory

• Bernhard Reus
• Thomas Streicher

Abstract This paper presents a comparison between algebraic specifications-in-the-large and a type theoretical formulation of modular specifications, called deliverables. It is shown that the laws of module algebra can be translated to laws about deliverables which can be proved correct in type theory. The adequacy of the Extended Calculus of Constructions as a possible implementation of type theory is discussed and it is explained how the reformulation of the laws is influenced by this choice.