In order to model the behaviour of open concurrent systems by means of Petri nets, we introduce open Petri nets, a generalisation of the ordinary model where some places, designated as open, represent an interface between the system and the environment. Besides generalising the token game to reflect this extension, we define a truly concurrent semantics for open nets by extending the Goltz–Reisig process semantics of Petri nets. We introduce a composition operation over open nets, characterised as a pushout in the corresponding category, suitable for modelling both interaction through open places and synchronisation of transitions. The deterministic process semantics is shown to be compositional with respect to such a composition operation. If a net $Z_3$ results as the composition of two nets $Z_1$ and $Z_2$, having a common subnet $Z_0$, then any two deterministic processes of $Z_1$ and $Z_2$ that ‘agree’ on the common part, can be ‘amalgamated’ to produce a deterministic process of $Z_3$. Conversely, any deterministic process of $Z_3$ can be decomposed into processes of the component nets. The amalgamation and decomposition operations are shown to be inverse to each other, leading to a bijective correspondence between the deterministic processes of $Z_3$ and the pair of deterministic processes of $Z_1$ and $Z_2$ that agree on the common subnet $Z_0$. Technically, our result is similar to the amalgamation theorem for data-types in the framework of algebraic specification. A possible application field of the proposed constructions and results is the modelling of interorganisational workflows, recently studied in the literature. This is illustrated by a running example.

This paper presents general syntactic conditions ensuring the strong normalisation and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. On the one hand, the Calculus of Constructions is a powerful type system in which one can formalise the propositions and natural deduction proofs of higher-order logic. On the other hand, rewriting is a simple and powerful computation paradigm. The combination of the two allows, among other things, the development of formal proofs with a reduced size and more automation compared with more traditional proof assistants. The main novelty is to consider a general form of rewriting at the predicate-level that generalises the strong elimination of the Calculus of Inductive Constructions.

We develop a coinductive calculus of streams based on the presence of a final coalgebra structure on the set of streams (infinite sequences of real numbers). The main ingredient is the notion of stream derivative, which can be used to formulate both coinductive proofs and definitions. In close analogy to classical analysis, the latter are presented as behavioural differential equations. A number of applications of the calculus are presented, including difference equations, analytical differential equations, continued fractions, and some problems from discrete mathematics and combinatorics.

We show how coalgebras can be presented by operations and equations. This is a special case of Linton's approach to algebras over a general base category ${\cal X}$, namely where ${\cal X}$ is taken as the dual of sets. Since the resulting equations generalise coalgebraic coequations to situations without cofree coalgebras, we call them coequations. We prove a general co-Birkhoff theorem describing covarieties of coalgebras by means of coequations. We argue that the resulting coequational logic generalises modal logic. This relies on the fact that coalgebraic operations respect an appropriate notion of bisimulation and can be considered as modal operators.

We define a constructive model for ${\Delta^0_2}$-maps, that is, maps recursively definable from a map deciding the halting problem. Our model refines an existing constructive interpretation for classical reasoning over one-quantifier formulas: it is compositional (Modus Ponens is interpreted as an application) and semantical (rather than translating classical proofs into intuitionistic ones, we define a mathematical structure intuitionistically validating excluded middle for one-quantifier formulas).