Abstract
Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular it allows for reasoning about confinement in object-oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

Abstract
Invariants, bisimulations and assertions are the main ingredients of coalgebra theory applied to software systems. In this paper we reduce the first to a particular case of the second and show how both together pave the way to a theory of coalgebras which regards invariant predicates as types. An outcome of such a theory is a calculus of invariants' proof obligation discharge, a fragment of which is presented in the paper. The approach has two main ingredients: one is that of adopting relations as "first class citizens" in a pointfree reasoning style; the other lies on a synergy found between a relational construct, Reynolds' relation on functions involved in the abstraction theorem on parametric polymorphism and the coalgebraic account of bisimulations and invariants. This leads to an elegant proof of the equivalence between two different definitions of bisimulation found in coalgebra literature (due to B. Jacobs and Aczel & Mendler, respectively) and to their instantiation to the classical Park-Milner definition popular in process algebra.

Abstract
Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Calculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed. Copyright © 2008 ACM.

Abstract
This paper addresses the foundations of data-model trans formation. A catalog of data mappings is presented which includes abstraction and representation relations and associated constraints. These are justified in an algebraic style via the pointfree-transform, a technique whereby predicates are lifted to binary relation terms (of the algebra of programming) in a two-level style encompassing both data and operations. This approach to data calculation, which also includes transformation of recursive data models into "flat" database schemes, is offered as alternative to standard database design from abstract models. The calculus is also used to establish a link between the proposed transformational style and bidirectional tenses developed in the context of the classical view-update problem.

Abstract

Abstract