In object-oriented programming, there are many notions of ‘collection with members in X’. This paper offers an axiomatic theory of collections based on monads in the category of sets and total functions. Heuristically, the axioms defining a collection monad state that each collection has a finite set of members of X, that pure 1-element collections exist and that a collection of collections flattens to a single collection whose members are the union of the members of the constituent collections. The relationship between monads and universal algebra leads to a formal definition of collection implementation in terms of tree-processing. Ideas from elementary category theory underly the classification of collections. For example, collections can be zipped if and only if the monad's endofunctor preserves pullbacks. Or, a collection can be uniquely specified by its shape and list of data if the morphisms of the Kleisli category of the monad are all deterministic, and the converse holds for commutative monads. Again, a collection monad is ordered if the monad's functor preserves equalizers of monomorphisms (so, in particular, if collections can be zipped the monad is ordered). Every implementable monad is ordered. It is shown using the well-ordering principle that a collection monad is ordered if and only if its functor admits an appropriated list-valued natural transformation that lists the members of each collection.

A framework is defined within which reactive systems can be studied formally. The framework is based on s-categories, which are a new variety of categories within which reactive systems can be set up in such a way that labelled transition systems can be uniformly extracted. These lead in turn to behavioural preorders and equivalences, such as the failures preorder (treated elsewhere) and bisimilarity, which are guaranteed to be congruential. The theory rests on the notion of relative pushout, which was previously introduced by the authors.

The framework is applied to a particular graphical model, known as link graphs, which encompasses a variety of calculi for mobile distributed processes. The specific theory of link graphs is developed. It is then applied to an established calculus, namely condition-event Petri nets.

In particular, a labelled transition system is derived for condition-event nets, corresponding to a natural notion of observable actions in Petri-net theory. The transition system yields a congruential bisimilarity coinciding with one derived directly from the observable actions. This yields a calibration of the general theory of reactive systems and link graphs against known specific theories.

We add extensional equalities for the functional and product types to the typed λ-calculus with, in addition to products and terminal object, sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus that stays confluent when allowing unbounded recursion. To do this, we turn the extensional equalities into expansion rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual λ-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non-extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly form our simulation technique without using the weak confluence property.

The analysis of the dynamics of Biological Regulatory Networks (BRNs) requires innovative methods to cope with the state-space explosion. This paper settles an original approach for deciding reachability properties based on Process Hitting, which is a framework suitable for modelling dynamical complex systems. In particular, Process Hitting has been shown to be of interest in providing compact models of the dynamics of BRNs with discrete values. Process Hitting splits a finite number of processes into so-called sorts and describes the way each process is able to act upon (that is, to ‘hit’) another one (or itself) in order to ‘bounce’ it as another process of the same sort with further actions.

By using complementary abstract interpretations of the succession of actions in Process Hitting, we build a very efficient static analysis to over- and under-approximate reachability properties, which avoids the need to build the underlying states graph. The analysis is proved to have a low theoretical complexity, in particular when the number of processes per sorts is limited, while a very large number of sorts can be managed.

This makes such an approach very promising for the scalable analysis of abstract complex systems. We illustrate this through the analysis of a large BRN of 94 components. Our method replies quasi-instantaneously to reachability questions, while standard model-checking techniques regularly fail because of the combinatoric explosion of behaviours.

Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle than might appear at first glance: final coalgebras can form monads just as easily as comonads, and, dually, initial algebras form both monads and comonads.

In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by first defining a notion of cosignature and coequation and then proving that the models of such coalgebraic presentations are precisely the coalgebras of the representing comonad.

In this paper we address the extension problem for quantal measures of path-integral type, concentrating on two cases: sequential growth of causal sets and a particle moving on the finite lattice ℤn. In both cases, the dynamics can be coded into a vector-valued measure μ on Ω, the space of all histories. Initially, μ is just defined on special subsets of Ω called cylinder events, and we would like to extend it to a larger family of subsets (events) in analogy to the way this is done in the classical theory of stochastic processes. Since quantally μ is generally not of bounded variation, a new method is required. We propose a method that defines the measure of an event by means of a sequence of simpler events that in a suitable sense converges to the event whose measure we are seeking to define. To this end, we introduce canonical sequences approximating certain events, and we propose a measure-based criterion for the convergence of such sequences. Applying the method, we encounter a simple event whose measure is zero classically but non-zero quantally.

In a controversial paper (De Millo et al. 1979) at the end of the 1970's, R. A. De Millo, R. J. Lipton and A. J. Perlis argued against formal verifications of programs, mostly motivating their position by an analogy with proofs in mathematics, and, in particular, with the impracticality of a strictly formalist approach to this discipline. The recent, impressive achievements in the field of interactive theorem proving provide an interesting ground for a critical revisiting of their theses. We believe that the social nature of proof and program development is uncontroversial and ineluctable, but formal verification is not antithetical to it. Formal verification should strive not only to cope with, but to ease and enhance the collaborative, organic nature of this process, eventually helping us to master the growing complexity of scientific knowledge.

We refine the simulation technique introduced in Di Cosmo and Kesner (1997) to show strong normalisation of $\l$-calculi with explicit substitutions via termination of cut elimination in proof nets (Girard 1987). We first propose a notion of equivalence relation for proof nets that extends the one in Di Cosmo and Guerrini (1999), and show that cut elimination modulo this equivalence relation is terminating. We then show strong normalisation of the typed version of the $\ll$-calculus with de Bruijn indices (a calculus with full composition defined in David and Guillaume (1999)) using a translation from typed $\ll$ to proof nets. Finally, we propose a version of typed $\ll$ with named variables, which helps to give a better understanding of the complex mechanism of the explicit weakening notation introduced in the $\ll$-calculus with de Bruijn indices (David and Guillaume 1999).

We present strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and programming tasks associated with the modelling of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, and describe its implementation: the graph transformation and visualisation tool Porgy.

It has recently become evident that categories of representations of Hopf algebras provide fundamental examples of monoidal categories. In this expository paper, we examine such categories as models of (multiplicative) linear logic. By varying the Hopf algebra, it is possible to model several variants of linear logic. We present models of the original commutative logic, the noncommutative logic of Lambek and Abrusci, the braided variant due to the author, and the cyclic logic of Yetter. Hopf algebras provide a unifying framework for the analysis of these variants. While these categories are monoidal closed, they lack sufficient structure to model the involutive negation of classical linear logic. We recall work of Lefschetz and Barr in which vector spaces are endowed with an additional topological structure, called linear topology. The resulting category has a large class of reflexive objects, which form a *-autonomous category, and so model the involutive negation. We show that the monoidal closed structure of the category of representations of a Hopf algebra can be extended to this topological category in a natural and simple manner. The models we obtain have the advantage of being nondegenerate in the sense that the two multiplicative connectives, tensor and par, are not equated. It has been recently shown by Barr that this category of topological vector spaces can be viewed as a subcategory of a certain Chu category. In an Appendix, Barr uses this equivalence to analyze the structure of its tensor product.

Relational structures offer a common framework for handling graphs and hypergraphs of various kinds. Operations like disjoint union, the creation of new relations by means of quantifier-free formulas, and relabellings of relations make it possible to denote them using algebraic expressions. It is known that every monadic second-order property of a structure is verifiable in time proportional to the size of such an algebraic expression defining it. We prove here that this result remains true if we also use in these algebraic expressions a fusion operation that fuses all elements of the domain satisfying some unary predicate. The value mapping from these algebraic expressions to the structures they denote is a monadic second-order definable transduction, which means that the structure is definable inside the tree representing the algebraic expression by monadic second-order formulas. It follows (by using results of other articles) that, with this fusion operation, we cannot generate more graph families, but we can generate them with less unary auxiliary predicates. We also obtain clear-cut characterizations of Vertex Replacement and Hyperedge Replacement context-free graph grammars in terms of four types of operations, amongst which is the fusion of vertices satisfying a specified predicate.

Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

We formulate a typed version of call-by-value λ-calculus containing variants of Felleisen's control operators A and C that provide explicit access to continuations and logically extend the propositions-as-types correspondence to classical propositional logic. We give an equational theory for this calculus, which is shown to be sound and complete with respect to a class of categorical models based on continuation-passing-style semantics.

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).

Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

Full abstraction, i.e. that a function preserves equivalence from a source to a target, has been used extensively as a correctness criterion for mappings between models of computation. I here show that with fixed equivalences, fully abstract functions almost always exist. Also, with the function and one of the equivalences fixed the other equivalence can almost always be found.

Tries, a form of string-indexed look-up structure, are generalized, in a manner first discovered by Wadsworth, to permit indexing by terms built according to an arbitrary signature. The construction is parametric with respect to the type of data to be stored as values; this is essential, because the recursion that defines tries appeals from one value type to others. ‘Trie’ (for any fixed signature) is then a functor, and the corresponding look-up function is a natural isomorphism.

The trie functor is in principle definable by the ‘initial fixed point’ semantics of Smyth and Plotkin. We simplify the construction, however, by introducing the ‘category-cpo’, a class of category within which calculations can retain some domain-theoretic flavor. Our construction of tries extends easily to many-sorted signatures.

This paper is an introduction to the RealLib package for exact real number computations. The library provides certified accuracy, but tries to achieve this at performance close to the performance of hardware floating point for problems that do not require higher precision. The paper gives the motivation and features of the design of the library and compares it with other packages for exact real arithmetic.

The spi calculus is an extension of the pi calculus with cryptographic primitives, which was designed for the verification of cryptographic protocols. Because of this extension, the naive adaptation of labelled bisimulations from the pi calculus is too strong to be useful for the purposes of verification. Instead, as a viable alternative, several ‘environment-sensitive’ bisimulations have been proposed. In this paper, we present a formal study of the differences between these bisimulations.

This paper presents a simple implementation of the λ-calculus in the interaction net paradigm. It is based on a two-fold translation. λ-terms are coded (for duplication) or decoded (for execution), and reduction is achieved by switching between these two states: decoding corresponds to head reduction and encoding to left reduction.