This article surveys a variety of approaches to integration theory that have arisen in the context of continuous domain theory. The presentation is set in a broader context of ‘positive’ analysis, analysis where order-theoretic notions and notions of positivity play a key role.

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.

This paper introduces the following new constructions on stable domains and event structures: the tensor product; the linear function space; and the exponential. These give rise to a monoidal closed category of dI-domains and to stable event structures, which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the category of stable event structures for modeling concurrency and its relation to other models are discussed.

Abstract Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the traditional and all other contemporary approaches, which rely on a prior notion of discrete set, type or object of a topos.

ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory and formal topology, it is founded on the algebra of open subspaces.

ASD is presented as a lambda calculus, of which we provide a self-contained summary, as the foundational background has been investigated in earlier work.

The core of the paper constructs the real line using two-sided Dedekind cuts. We show that the closed interval is compact and overt, where these concepts are defined using quantifiers. Further topics, such as the Intermediate Value Theorem, are presented in a separate paper that builds on this one.

The interval domain plays an important foundational role. However, we see intervals as generalised Dedekind cuts, which underly the construction of the real line, not as sets or pairs of real numbers.

We make a thorough study of arithmetic, in which our operations are more complicated than Moore's, because we work constructively, and we also consider back-to-front (Kaucher) intervals.

Finally, we compare ASD with other systems of constructive and computable topology and analysis.

Homotopy type theory may be seen as an internal language for the ∞-category of weak ∞-groupoids. Moreover, weak ∞-groupoids model the univalence axiom. Voevodsky proposes this (language for) weak ∞-groupoids as a new foundation for Mathematics called the univalent foundations. It includes the sets as weak ∞-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those ‘discrete’ groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of ‘elementary’ of ∞-toposes. We prove that sets in homotopy type theory form a ΠW-pretopos. This is similar to the fact that the 0-truncation of an ∞-topos is a topos. We show that both a subobject classifier and a 0-object classifier are available for the type theoretical universe of sets. However, both of these are large and moreover the 0-object classifier for sets is a function between 1-types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.

This paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction steps. The presentation of this procedure is preceded by an analysis of Gentzen's mix-elimination procedure, made in the perspective of permuting cut with contraction. We also show that in the absence of implication, pushing cut above contraction does not pose problems for directly eliminating cut.

We introduce a method to associate calculi of proof terms and rewrite rules with cut elimination procedures for logical deduction systems (i.e., Gentzen-style sequent calculi) in the case of intuitionistic logic. We illustrate this method using two different versions of the cut rule for a variant of the intuitionistic fragment of Kleene's logical deduction system G3.

Our systems are in fact calculi of explicit substitution, where the cut rule introduces an explicit substitution and the left-→ rule introduces a binding of the result of a function application. Cut propagation steps of cut elimination correspond to propagation of explicit substitutions, and propagation of weakening (to eliminate it) corresponds to propagation of index-updating operations. We prove various subject reduction, termination, and confluence properties for our calculi.

Our calculi improve on some earlier calculi for logical deduction systems in a number of ways. By using de Bruijn indices, our calculi qualify as first-order term rewriting systems (TRS's), allowing us to use correctly certain results for TRS's about termination. Unlike in some other calculi, each of our calculi has only one cut rule and we do not need unusual features of sequents.

We show that the substitution and index-updating mechanisms of our calculi work the same way as the substitution and index-updating mechanisms of Kamareddine and Ríos' λs and λt, two well-known systems of explicit substitution for the standard λ-calculus. By a change in the format of sequents, we obtain similar results for a known λ-calculus with variables and explicit substitutions, Rose's λbxgc.

Coinductive predicates express persisting ‘safety’ specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration – a categorical abstraction of predicate logic. In this paper, we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical ‘size restriction’ axioms that guarantee stabilization of final sequences after ω steps. In its course, we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for binary relations (i.e. the logic of ‘binary predicates’) for which a coinductive predicate is bisimilarity, constructive logics (where interests are growing in coinductive predicates) and logics for name-passing processes.

In the literature ther are two main notins of model for the second order λ-calculus: one by Bruce, Meyer and Mitchell (the BMM-model, for short) in set-theoretical formulation and one category-theoretical by Seely. Here we generalise Seely's notion, using semifunctors and semi-adjunctions from Hayashi, and introduce λ2-algebras, λη2-algebras, λ2-models and λη-models, similarly to the untyped λ-calculus. Non-extensional abstraction of both term and type variables is described by semi-adjunctions (essentially as in Martini's thesis). We show that also for second order sume, the β-(and commutation!) conversions correspond to semi-functoriality and that the (additional) η-conversion corresponds to ordinary fuctioriality.

In the above framework various examples – well known ones and variations – are described. Also, we determine the place of the BMM-models; an earlier version of the latter has been reported by Jacobs.

We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets. We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).

We prove that the iterative construction of initial algebras converges for endofunctors F of many-sorted sets whenever F has an initial algebra. In the case of one-sorted sets, the convergence takes n steps where n is either an infinite regular cardinal or is at most 3. Dually, the existence of a many-sorted terminal coalgebra implies that the iterative construction of a terminal coalgebra converges. Moreover, every endofunctor with a fixed-point pair larger than the number of sorts is proved to have a terminal coalgebra. As demonstrated by James Worell, the number of steps here need not be a cardinal even in the case of a single sort: it is ω + ω for the finite power-set functor. The above results do not hold for related categories, such as graphs: we present non-constructive initial algebras and terminal coalgebras.

We focus attention on a language ℒ generated by a set of elementary actions under operations of sequential composition, external binary choice, iteration, and non-nested disjoint parallel composition: that is, on an especially simple parallel language without explicit internal, or ‘local’, nondeterminism. ℒ is nondeterministic, despite the restriction to external choice, since a given action may occur in both subterms F and G of the parallel composition F ║ G. We exhibit a single set of equations that axiomatizes both step bisimulation and pomset equivalence on ℒ Given that step bisimulation and pomset equivalence are incomparable on the language ℒ+ obtained from ℒ by relaxing just the constraint on choice, the coincidence of these equivalences on ℒ suggests that the elimination of explicit internal choice can result in simplifications at the semantic level. We reinforce this impression by showing for ℒ that step bisimulation (i) coincides with pomset bisimulation equivalence, (ii) is real-time consistent, and (iii) has step trees as concrete representatives of its equivalence classes. Moreover, we show that none of these results holds for the language ℒ+ Finally, step trace equivalence is proved not to coincide with step bisimulation equivalence on ℒ.

A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the λβ or the least sensible λ-theory ℋ (which is generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there are a minimal λ-theory and a minimal sensible λ-theory represented by it. In this paper, we give a positive answer to this question for the class of graph models à la Plotkin, Scott and Engeler. In particular, we build two graph models whose theories are the set of equations satisfied in, respectively, any graph model and any sensible graph model. We conjecture that the least sensible graph theory, where ‘graph theory’ means ‘λ-theory of a graph model’, is equal to ℋ, while in one of the main results of the paper we show the non-existence of a graph model whose equational theory is exactly the λβ theory.

Another related question is whether, given a class of lambda models, there is a maximal sensible λ-theory represented by it. In the main result of the paper, we characterise the greatest sensible graph theory as the λ-theory ℬ generated by equating λ-terms with the same Böhm tree. This result is a consequence of the main technical theorem of the paper, which says that all the equations between solvable λ-terms that have different Böhm trees fail in every sensible graph model. A further result of the paper is the existence of a continuum of different sensible graph theories strictly included in ℬ.

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 relationship between continuous-time dynamics and the corresponding discrete schemes, and its generally limited validity, is an important and widely acknowledged field within numerical analysis. In this paper, we propose another, more physical, viewpoint on this topic in order to understand the possible failure of discretisation procedures and the way to fix it. Three basic examples, the logistic equation, the Lotka–Volterra predator–prey model and Newton's law for planetary motion, are worked out. They illustrate the deep difference between continuous-time evolutions and discrete-time mappings, hence shedding some light on the more general duality between continuous descriptions of natural phenomena and discrete numerical computations.

Unfold/fold transformations have been used in logic programming for some years to transform programs into more efficient ones. We describe recent work on the extent to which these transformations produce programs which are equivalent to the original one. Various notions of equivalence are considered: same success set; finite failure set; least Herbrand model; completion. This is used to illustrate the rather unsatisfactory relationship between logic programming and logic shown by the wide variety of different declarative semantics proposed for logic programs.

It is the contention of the author that there is a preferred categorical structure appropriate for the analysis of imperative programming languages, namely the existence of finite sums and products and a distributive law of products over sums. An imperative language based on these operations is described.

This paper introduces guarded and strongly guarded monads as a unified model of a variety of different term algebras covering fundamental examples such as initial algebras, final coalgebras, rational terms and term graphs. We develop a general method for obtaining finitary guarded monads that allows us to define and prove properties of the rational and term graph monads. Furthermore, our treatment of rational equations extends the traditional approach to allow right-hand sides of equations to be infinite terms, term graphs or other such coalgebraic structures. As an application, we use these generalised rational equations to sketch part of the correctness of the term graph implementation of functional programming languages.

Every dialogue category comes equipped with a continuation monad defined by applying the negation functor twice. In this paper, we advocate that this double negation monad should be understood as part of a larger parametric monad (or a lax action) with parameter taken in the opposite of the dialogue category. This alternative point of view has one main conceptual benefit: it reveals that the strength of the continuation monad is the fragment of a more fundamental and symmetric structure – provided by a distributivity law between the parametric continuation monad and the canonical action of the dialogue category over itself. The purpose of this work is to describe the formal properties of this parametric continuation monad and of its distributivity law.

We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus αλ associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.