### A completeness theorem in the modal logic of programs

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

We introduce adhesive categories, which are categories with structure ensuring that pushouts along monomorphisms are well-behaved, as well as quasiadhesive categories which restrict attention to regular monomorphisms. Many examples of graphical structures used in computer science are shown to be examples of adhesive and quasiadhesive categories. Double-pushout graph rewriting generalizes well to rewriting on arbitrary adhesive and quasiadhesive categories.

Coalgebras for endofunctors $\mathcal{C}\to \mathcal{C}$ can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors ${\mathcal{C}}^{op}\times \mathcal{C}\to \mathcal{C}$. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard...

Coalgebras for endofunctors $\mathcal{C}\to \mathcal{C}$ can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors${\mathcal{C}}^{op}\times \mathcal{C}\to \mathcal{C}$. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many...

The abstract model-theoretic concepts of compactness and Löwenheim-Skolem properties are investigated in the "softer" framework of pre-institutions [18]. Two compactness results are presented in this paper: a more informative reformulation of the compactness theorem for pre-institution transformations, and a theorem on natural equivalences with an abstract form of the first-order pre-institution. These results rely on notions of compact transformation, which are introduced as arrow-oriented generalizations...

A new implementation concept for parameterized specifications based on constructors and abstractors was recently introduced by Orejas, Navarro and Sánchez which includes most of the implementation concepts in the literature for initial as well as loose semantics. In this paper we redefine vertical and different kinds of horizontal compositions using the new concept of semi-pushout defined for a mixture of signature and specification morphisms. The main results concerning correctness of horizontal...

The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. In this paper we enrich this calculus with a type discipline which preserves some biological properties depending on the minimum and the maximum number of elements of some type requested by the present elements. The type system enforces these properties and typed reductions guarantee that evolution preserves them. As an example, we model the hemoglobin structure and...