In earlier work we explored the expressiveness and algebraic theory Psi-calculi, which form a parametric framework for extensions of the pi-calculus. In the current paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with examples and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle/Nominal.

Mathematical logic and computer science have driven the design of a growing number of logics and related formalisms such as set theories and type theories. In response to this population explosion, logical frameworks have been developed as formal meta-languages in which to represent, structure, relate and reason about logics.

Research on logical frameworks has diverged into separate communities, often with conflicting backgrounds and philosophies. In particular, two of the most important logical frameworks are the framework of institutions, from the area of model theory based on category theory, and the Edinburgh Logical Framework LF, from the area of proof theory based on dependent type theory. Even though their ultimate motivations overlap – for example in applications to software verification – they have fundamentally different perspectives on logic.

In the current paper, we design a logical framework that integrates the frameworks of institutions and LF in a way that combines their complementary advantages while retaining the elegance of each of them. In particular, our framework takes a balanced approach between model theory and proof theory, and permits the representation of logics in a way that comprises all major ingredients of a logic: syntax, models, satisfaction, judgments and proofs. This provides a theoretical basis for the systematic study of logics in a comprehensive logical framework. Our framework has been applied to obtain a large library of structured and machine-verified encodings of logics and logic translations.

A cross-bifix-free set of words is a set in which no prefix of any length of any word is the suffix of any other word in the set. A construction of cross-bifix-free sets has recently been proposed in Chee et al. (2013) within a constant factor of optimality. We propose a Gray code for these cross-bifix-free sets and a CAT algorithm generating it. Our Gray code list is trace partitioned, that is, words with zero in the same positions are consecutive in the list.

We recast dataflow in a modern categorical light using profunctors as a generalisation of relations. The well-known causal anomalies associated with relational semantics of indeterminate dataflow are avoided, but still we preserve much of the intuitions of a relational model. The development fits with the view of categories of models for concurrency and the general treatment of bisimulation they provide. In particular, it fits with the recent categorical formulation of feedback using traced monoidal categories. The payoffs are: (1) explicit relations to existing models and semantics, especially the usual axioms of monotone IO automata are read off from the definition of profunctors; (2) a new definition of bisimulation for dataflow, the proof of the congruence of which benefits from the preservation properties associated with open maps; and (3) a treatment of higher-order dataflow as a biproduct, essentially by following the geometry of interaction programme.

We introduce term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. Our main result is that this mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find a more general solution. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.

We investigate universal algebra over the category Nom of nominal sets. Using the fact that Nom is a full reflective subcategory of a monadic category, we obtain an HSP-like theorem for algebras over nominal sets. We isolate a ‘uniform’ fragment of our equational logic, which corresponds to the nominal logics present in the literature. We give semantically invariant translations of theories for nominal algebra and NEL into ‘uniform’ theories, and systematically prove HSP theorems for models of these theories.

Argumentation is a proof theoretic paradigm for reasoning under uncertainty. Whereas a ‘proof’ establishes its conclusion outright, an ‘argument’ can only lend a measure of support. Thus, the process of argumentation consists of identifying all the arguments for a particular hypothesis φ, and then calculating the support for φ from the weight attached to these individual arguments. Argumentation has been incorporated as the inference mechanism of a large scale medical expert system, the ‘Oxford System of Medicine’ (OSM), and it is therefore important to demonstrate that the approach is theoretically justified. This paper provides a formal semantics for the notion of argument embodied in the OSM. We present a categorical account in which arguments are the arrows of a semilattice enriched category. The axioms of a cartesian closed category are modified to give the notion of an ‘evidential closed category’, and we show that this provides the correct enriched setting in which to model the connectives of conjunction (&) and implication (⇒).

Finally, we develop a theory of ‘confidence measures’ over such categories, and relate this to the Dempster-Shafer theory of evidence.

We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step, we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.

Computable analysis and effective descriptive set theory are both concerned with complete metric spaces, functions between them and subsets thereof in an effective setting. The precise relationship of the various definitions used in the two disciplines has so far been neglected, a situation this paper is meant to remedy.

As the role of the Cauchy completion is relevant for both effective approaches to Polish spaces, we consider the interplay of effectivity and completion in some more detail.

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.

We define the class of divisibility monoids that arise as quotients of the free monoid Σ* modulo certain equations of the form ab = cd. These form a much larger class than free partially commutative monoids, and we show, under certain assumptions, that the recognizable languages in these divisibility monoids coincide with c-rational languages. The proofs rely on Ramsey's theorem, distributive lattice theory and on Hashigushi's rank function generalized to these monoids. We obtain Ochmański's theorem on recognizable languages in free partially commutative monoids as a consequence.

In standard realizability one works with respect to an untyped universe of realizers called a partial combinatory algebra (pca). It is well known that a pca [Ascr ] gives rise to a categorical model of impredicative type theory via the category Asm([Ascr ]) of assemblies over [Ascr ] or the realizability topos over [Ascr ].

Recently, John Longley introduced a typed version of pca's (Longley 1999b). The above mentioned construction of categorical models extends to the typed case. However, in general these are no longer impredicative. We show that for a typed pca [Tscr ] the ensuing models are impredicative if and only if [Tscr ] has a universal type U. Such a type U can be endowed with the structure of an untyped pca such that U and [Tscr ] induce equivalent realizability models: in other words, a typed pca [Tscr ] with a universal type is essentially untyped. Thus, a posteriori it turns out that nothing is lost by restricting to (untyped) pca's as far as realizability models of impredicative type theories are concerned.

For instance, we show that for a typed pca [Tscr ] the fibred category of discrete families in Asm([Tscr ]) is small if and only if [Tscr ] has a universal type. As the category of ¬¬-separated objects of the modified realizability topos is equivalent to Asm([Tscr ]) for an appropriate typed pca [Tscr ] without a universal type, it follows that the discrete families in the subcategory of ¬¬-separated objects of the modified realizability topos do not provide a model of polymorphic λ-calculus.

Retrenchment is a flexible model evolution formalism that compensates for the limitations imposed by specific formulations of refinement. Its refinement-like proof obligations feature additional predicates for accommodating design data describing the model change. The best results are obtained when refinement and retrenchment cooperate, the paradigmatic scheme for this being the commuting square or tower, in which ‘horizontal retrenchment rungs’ commute with ‘vertical refinement columns’ to navigate through a much more extensive design space than permitted by refinement alone. In practice, the navigation is accomplished through ‘square completion’ constructions, and we present and prove a full suite of square completion theorems.

In ACP-style process algebra the interpretation of a constant atomic action combines action execution with termination. In a setting with timing, different forms of termination can be distinguished: some-time termination, termination before the next clock tick, urgent termination, having terminated. In a setting with the silent action $\tau$, we also have silent termination. This leads to problems with the interpretation of atomic actions in timed theories that involve some form of the empty process or some form of the silent action. Reflection on these problems led to a redesign of basic process algebra, where action execution and termination are separated. Instead of actions as constants, we have action prefix operators. Sequential composition remains a basic operator, and thus we have two basic constants for termination: $\delta$ for unsuccessful termination (deadlock) and $\epsilon$ for successful termination (skip). We can recover standard ACP-style process algebras as subtheories of the new theory. The new approach has definite advantages over the standard approach. The paper contributes to ongoing work on relationships between algebras with different timing features.

While developing a method for reasoning about programs, Pitts defined the [top ][top ]-closed relations as an alternative to the standard admissible relations. This paper reformulates and studies Pitts's operational concept of [top ][top ]-closure in a semantic framework. It investigates the non-trivial connection between [top ][top ]-closure and admissibility, showing that [top ][top ]-closure is strictly stronger than admissibility and that every [top ][top ]-closed relation corresponds to an admissible preorder.

System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a ‘decomposition’ theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.

We define session types as projections of the behaviour of processes with respect to the operations processes perform on channels. This calls for a parallel composition operator over session types denoting the simultaneous access to a channel by two or more processes. The proposed approach allows us to define a semantically grounded theory of session types that does not require the linear usage of channels. However, type preservation and progress can only be guaranteed for processes that never receive channels they already own. A number of examples show that the resulting framework validates existing session-type theories and unifies them to some extent.

In this survey we discuss the generalisation of stochastic Kripke models for general modal logics through predicate liftings for functors over general measurable spaces. We derive results on expressivity and show that selection arguments allow us to incorporate the discussion of bisimilarity, provided the underlying spaces are assumed to be standard Borel.

We present a type-based flow analysis for simply typed lambda calculus with booleans, data-structures and recursion. The analysis is exact in the following sense: if the analysis predicts a redex, there exists a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.

It follows that the analysis is non-elementary recursive – more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the techniques employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.

A preliminary version of this paper has previously been published (Mossin 1997b). The present paper extends, elaborates and corrects this previously published abstract.

In the paper we introduce and study the uniform regular enumerations for arbitrary recursive ordinals. As an application of the technique, we obtain a uniform generalisation of a theorem of Ash and a characterisation of a class of uniform operators on transfinite sequences of sets of natural numbers.