We study the relationship between the encodings of the λ-calculus into π-calculus, the Continuation Passing Style (CPS) transforms, and the compilation of the Higher-Order π-calculus (HOπ) into π-calculus. We factorise the π-calculus encodings of (untyped as well as simply-typed) call-by-name and call-by-value λ-calculus into three steps: a CPS transform, the inclusion of CPS terms into HOπ and the compilation from HOπ to π-calculus. The factorisations are used both to derive the encodings and to prove their correctness.

We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method for a large class of state based systems, including labelled transition systems but also stream systems and weighted automata. Our approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. All in all, this gives a powerful and modular framework for simplified coinductive proofs of equivalence.

The notion of semi-functor was introduced in Hayashi (1985) in order to make possible a category-theoretical characterization of models of the non-extensional typed lambda calculus. Motivated by the further use of semi-functors in Martini (1987), Jacobs (1991) and Hoofman (1992a), (1992b) and (1992c), we consider the general theory of semi-functors in this paper. It turns out that the notion of semi natural transformation plays an important part in this theory, and that various categorical notions involving semi-functors can be viewed as 2-categorical notions in the 2-category of categories, semi-functors and semi natural transformations. In particular, we find that the notion of normal semi-adjunction as defined in Hayashi (1985) is the canonical generalization of the notion of adjunction to the world of semi-functors. Further topics covered in this paper are the relation between semi-functors and splittings, the Karoubi envelope construction, semi-comonads, and a semi-adjoint functor theorem.

We establish Choquet–Kendall–Matheron theorems on non-Hausdorff topological spaces. This typical result of random set theory is profitably recast in purely topological terms using intuitions and tools from domain theory. We obtain three variants of the theorem, each one characterising distributions, in the form of continuous valuations, over relevant powerdomains of demonic, angelic and erratic non-determinism, respectively.

The Rewriting Calculus (ρ-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories.

In this paper we propose an extension of the ρ-calculus, called ρg-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard ρ-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the ρ-calculus, the transformations are performed by explicit application of rewrite rules as first-class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.

We show that the ρg-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that ρg-calculus-terms are considered modulo an equational theory. We also show that the ρg-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and α-calculus with explicit recursion (modelled using a letrec-like construct).

This paper considers two main aspects of the lower power locale PL(X): first, its relation to the symmetric topos construction of Bunge and Carboni; and second, its points, which, it is shown, are equivalent to the weakly closed sublocales of X with open domain. This is done as part of a more general discussion of arbitrary weakly closed sublocales, including a new characterization using suplattice homomorphisms from o(X) to Sub(1), and a new proof of a theorem of Jibladze relating them to Ω-nuclei.

This paper studies the properties of the subnets of a proof-net for first-order Multiplicative Linear Logic without propositional constants (MLL−), extended with the rule of Mix: from [vdash ]Γ and [vdash ]Δ infer [vdash ]Γ, Δ. Asperti's correctness criterion and its interpretation in terms of concurrent processes are extended to the first-order case. The notions of kingdom and empire of a formula are extended from MLL− to MLL−+MIX. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland's Full Intuitionistic Linear Logic with Mix; this result gives a general method for translating Abramsky-style term assignments into proof-nets, and vice versa.

Finitary $\mathcal{M}$-adhesive categories are $\mathcal{M}$-adhesive categories with finite objects only, where $\mathcal{M}$-adhesive categories are a slight generalisation of weak adhesive high-level replacement (HLR) categories. We say an object is finite if it has a finite number of $\mathcal{M}$-subobjects. In this paper, we show that in finitary $\mathcal{M}$-adhesive categories we not only have all the well-known HLR properties of weak adhesive HLR categories, which are already valid for $\mathcal{M}$-adhesive categories, but also all the additional HLR requirements needed to prove classical results including the Local Church-Rosser, Parallelism, Concurrency, Embedding, Extension and Local Confluence Theorems, where the last of these is based on critical pairs. More precisely, we are able to show that finitary $\mathcal{M}$-adhesive categories have a unique $\mathcal{E}$-$\mathcal{M}$ factorisation and initial pushouts, and the existence of an $\mathcal{M}$-initial object implies we also have finite coproducts and a unique $\mathcal{E}$′-$\mathcal{M}$ pair factorisation. Moreover, we can show that the finitary restriction of each $\mathcal{M}$-adhesive category is a finitary $\mathcal{M}$-adhesive category, and finitarity is preserved under functor and comma category constructions based on $\mathcal{M}$-adhesive categories. This means that all the classical results are also valid for corresponding finitary $\mathcal{M}$-adhesive transformation systems including several kinds of finitary graph and Petri net transformation systems. Finally, we discuss how some of the results can be extended to non-$\mathcal{M}$-adhesive categories.

We present a simple stochastic rule-based approach to multi-level modelling for computational systems biology. Populations are modelled using multi-level multisets; these contain both species and agents, with the latter possibly containing further such multisets. Rules are pairs of such multisets, but they may now also include variables (as well as species and agents), together with an associated stochastic rate.

We give two illustrative examples. The first is an extracellular model of virus infection, coupled with an intracellular model of viral reproduction; this model can demonstrate successive waves of infection. The second is a model of cell division in which a repressor protein is diluted in successive generations, so eventually repression no longer occurs. The multi-level multiset approach can also be seen in terms of stochastic term rewriting for the theory of a commutative monoid equipped with extra constants (for the species) and unary operations (for the agents). We further discuss the relationship of this approach with two others: Krivine et al.'s stochastic bigraphs, restricted to Milner's place graphs, and Coppo et al.'s Stochastic Calculus of Wrapped Compartments. These various relationships provide evidence for the fundamental nature of the approach.

The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally polymorphic types, such as polymorphic object and variant types, which have the extra specificity of allowing recursion. We implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of evaluation, soundness and principality of type inference, and correctness of a stack-based interpreter, are also proved.†

A set X ⊆ Σ** of pictures is a code if every picture over Σ is tilable in at most one way with pictures in X. The definition of strong prefix code is introduced. The family of finite strong prefix codes is decidable and it has a polynomial time decoding algorithm. Maximality for finite strong prefix codes is also studied and related to the notion of completeness. We prove that any finite strong prefix code can be embedded in a unique maximal strong prefix code that has minimal size and cardinality. A complete characterization of the structure of maximal finite strong prefix codes completes the paper.

Using the well-known categorical notion of ‘functor’, one may define the concept of datatype (algebra) without being forced to introduce a signature (that is, names and typings for the individual sorts (types) and operations involved). This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra.

The categorical notion of ‘transformer’ developed in this paper allows the same approach to laws: without using signatures one can define the concept of law for datatypes (lawful algebras), and investigate the equational specification of datatypes in a syntax-free manner. A transformer is a special kind of functor and also a natural transformation on the level of dialgebras. Transformers are quite expressive, satisfy several closure properties, and are related to naturality and Wadler'' Theorems For Free Theorem. In fact, any colimit is an initial lawful algebra.

This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =).

We present two satisfiability-preserving (in a broad sense) translations Φ ↦ $\dot{\Phi}$ and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{\Phi}$ is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic.

It turns out that |$\dot{\Phi}$| = $\mathcal{O}$(|Φ|) and |Φσ| = $\mathcal{O}$(|Φ|2).

Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.

In this paper, we introduce the formalism of deduction graphs as a generalisation of both Gentzen–Prawitz style natural deduction and Fitch style flag deduction. The advantage of this formalism is that, as with flag deductions (but not natural deduction), subproofs can be shared, but the linearisation used in flag deductions is avoided. Our deduction graphs have both nodes and boxes, which are collections of nodes that also form a node themselves. This is reminiscent of the bigraphs of Milner, where the link graph describes the nodes and edges and the place graph describes the nesting of nodes. We give a precise definition of deduction graphs, together with some illustrative examples. Furthermore, we analyse their computational behaviour by studying the process of cut-elimination and by defining translations from deduction graphs to simply typed lambda terms. From a slight variation of this translation, we conclude that the process of cut-elimination is strongly normalising. The translation to simple type theory removes quite a lot of structure, so we also propose a translation to a context calculus with lets that faithfully captures the structure of deduction graphs. The proof nets of linear logic also offer a graph-like presentation of natural deduction, and we point out some similarities between the two formalisms.

In this paper we characterise the categories of Lawvere theories and equational theories that correspond to the categories of analytic and polynomial monads on Set, and hence also to the categories of the symmetric and rigid operads in Set. We show that the category of analytic monads is equivalent to the category of regular-linear theories. The category of polynomial monads is equivalent to the category of rigid theories, that is, regular-linear theories satisfying an additional global condition. This solves a problem posed by A. Carboni and P. T. Johnstone. The Lawvere theories corresponding to these monads are identified via some factorisation systems. We also show that the categories of analytic monads and finitary endofunctors on Set are monadic over the category of analytic functors. The corresponding monad for analytic monads distributes over the monad for finitary endofunctors and hence the category of (finitary) monads on Set is monadic over the category of analytic functors. This extends a result of M. Barr.

This paper presents a new and self-contained proof of a result characterizing objects isomorphic in the free symmetric monoidal closed category, i.e., objects isomorphic in every symmetric monoidal closed category. This characterization is given by a finitely axiomatizable and decidable equational calculus, which differs from the calculus that axiomatizes all arithmetical equalities in the language with 1, product and exponentiation by lacking 1c=1 and (a · b)c=ac · bc (the latter calculus characterizes objects isomorphic in the free cartesian closed category). Nevertheless, this calculus is complete for a certain arithmetical interpretation, and its arithmetical completeness plays an essential role in the proof given here of its completeness with respect to symmetric monoidal closed isomorphisms.

In this paper we introduce the concept of Kleisli strength for monads in an arbitrary symmetric monoidal category. This generalises the notion of commutative monad and gives us new examples, even in the cartesian-closed category of sets. We exploit the presence of Kleisli strength to derive methods for generating distributive laws. We also introduce linear equations to extend the results to certain quotient monads. Mechanisms are described for finding strengths that produce a large collection of new distributive laws, and consequently monad compositions, including the composition of monadic data types such as lists, trees, exceptions and state.

We study perpetuality in the calculus of explicit substitutions λx. A reduction is called perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at applications of this study: an inductive characterization of the λx-strongly normalizing terms, two perpetual reduction strategies for λx and finally a proof of strong normalization of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of Fes, the property of subject reduction is shown to hold by extending type assignments of the typing rules to allow non-pure types (types with possible occurrences of the type substitution operator).

A categorical framework for equational logics is presented, together with axiomatizability results in the style of Birkhoff. The distinctive categorical structures used are inclusion systems, which are an alternative to factorization systems in which factorization is required to be unique rather than unique ‘up to an isomorphism’. In this framework, models are any objects, and equations are special epimorphisms in [Cfr ], while satisfaction is injectivity. A first result says that equations-as-epimorphisms define exactly the quasi-varieties, suggesting that epimorphisms actually represent conditional equations. In fact, it is shown that the projectivity/freeness of the domain of epimorphisms is what makes the difference between unconditional and conditional equations, the first defining the varieties, as expected. An abstract version of the axiom of choice seems to be sufficient for free objects to be projective, in which case the definitional power of equations of projective and free domain, respectively, is the same. Connections with other abstract formulations of equational logics are investigated, together with an organization of our logic as an institution.

This paper describes the design and semantics of METAKLAIM, which is a higher order distributed process calculus equipped with staging mechanisms. METAKLAIM integrates METAML (an extension of SML for multi-stage programming) and KLAIM (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (such as assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ‘traditional’ computational activities on a wide area network (such as remote communication and code mobility). METAKLAIM exploits a powerful type system (including polymorphic types á la system F) to deal with highly parameterised mobile components and to enforce security policies dynamically: types are metadata that are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide area network applications are maintained whenever computations interoperate with potentially untrusted components.