We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin. The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for existing category-theoretic notions of relational parametricity. We provide examples of parametric models and describe a way of constructing parametric models from given models of the second-order lambda calculus.

We study isomorphisms of inductive types (that is, recursive types satisfying a condition of strict positivity) in an extensional simply typed $\lambda$-calculus with product and unit types. We first show that the calculus enjoys strong normalisation and confluence. Then we extend it with new conversion rules ensuring that all inductive representations of the product and unit types are isomorphic, and such that the extended reduction remains convergent. Finally, we define the notion of a faithful copy of an inductive type and a corresponding conversion relation that also preserves the good properties of the calculus.

Continuous valuations have been proposed by several authors as a way of modelling probabilistic non-determinism in programming language semantics. Let $(X, {\cal O})$ be a topological space. A quasi-simple valuation on $X$ is the sup of a directed family of simple valuations. We show that quasi-simple valuations are exactly those valuations that extend to continuous valuations to the Alexandroff topology on the specialisation preordering of the topology $\cal O$. A number of applications are presented. In particular, we recover Jones' result that every continuous valuation is quasi-simple if $X$ is a continuous dcpo – in this case there is a least extension to the Alexandroff topology. We show that this can be refined if $X$ is algebraic, where every continuous valuation is the sup of a directed family of simple valuations based on finite elements. We exhibit another class of spaces in which every continuous valuation is quasi-simple, the so-called finitarily coherent spaces – in this case there is a largest extension to the Alexandroff topology. In general, the extension to the Alexandroff topology is not unique, unless, for example, the original valuation is bicontinuous. We also show that other natural spaces of valuations, namely those of discrete valuations and point-continuous valuations, can be characterised by similar extension theorems.

This paper studies coalgebras from the perspective of finite observations. We introduce the notion of finite step equivalence and a corresponding category with finite step equivalence-preserving morphisms. This category always has a final object, which generalises the canonical model construction from Kripke models to coalgebras. We then turn to logics whose formulae are invariant under finite step equivalence, which we call logics of rank $\omega$. For these logics, we use topological methods and give a characterisation of compact logics and definable classes of models.

This paper addresses a conjecture of Smyth that says that if $D$ and $[D \rightarrow D]$ are effectively algebraic directed-complete partial orders with least element (cpo's), then $D$ is an effectively strongly algebraic cpo, though what is meant by an effectively algebraic and an effectively strongly algebraic cpo was not made precise.

Notions of an effectively strongly algebraic cpo and an effective SFP domain are introduced and shown to be (effectively) equivalent. Moreover, the conjecture is shown to hold if instead of being effectively algebraic, $[D \rightarrow D]$ is only required to be $\omega$-algebraic and $D$ is forced to have a completeness test, that is a procedure that decides for any two finite sets $X$ and $Y$ of compact cpo elements whether $X$ is a complete set of upper bounds of $Y$. As a consequence, the category of effective SFP objects and continuous maps turns out to be the largest Cartesian closed full subcategory of the category of $\omega$-algebraic cpo's that have a completeness test.

We then consider whether such a result also holds in a constructive framework, where one considers categories with constructive domains as objects, that is, domains consisting only of the constructive (computable) elements of an indexed $\omega$-algebraic cpo, and computable maps as morphisms. This is indeed the case: the category of constructive SFP domains is the largest constructively Cartesian closed weakly indexed effectively full subcategory of the category of constructive domains that have a completeness test and satisfy a further effectivity requirement.

We show that the category of coalgebras of a wide-pullback preserving endofunctor on a category of presheaves is itself a category of presheaves. This illustrates a connection between Jacobs' temporal logic of coalgebras and Ghilardi and Meloni's presheaf semantics for temporal modalities.

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).

The first-order isomorphism problem is to decide whether two non-recursive types using product- and function-type constructors are isomorphic under the axioms of commutative and associative products, and currying and distributivity of functions over products. We show that this problem can be solved in $O(n \log^2 n)$ time and $O(n)$ space, where $n$ is the input size. This result improves upon the $O(n^2 \log n)$ time and $O(n^2)$ space bounds of the best previous algorithm. We also describe an $O(n)$ time algorithm for the linear isomorphism problem, which does not include the distributive axiom, thereby improving upon the $O(n \log n)$ time of the best previous algorithm for this problem.

In this paper we introduce a new hierarchical graph model to structure large graphs into small components by distributing the nodes (and, likewise, edges) into a hierarchy of packages. In contrast to other known approaches, we do not fix the type of underlying graphs. Moreover, our model is equipped with a rule-based transformation concept such that hierarchical graphs are not restricted to being used only for the static representation of complex system states, but can also be used to describe dynamic system behaviour.

We develop a matching algorithm for an equational theory with multiplication, exponentiation and a unit element. The algorithm is proved consistent, complete and minimal using techniques based on initial algebras.

We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's dual-context system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically manageable axiomatisation without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads.

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.

Starting from the $\lambda$-calculus with names, we develop a family of calculi with explicit substitutions that overcome the usual syntactical problems of substitution. The key idea is that only closed substitutions can be moved through certain constructs. This gives a weak form of reduction, called closed reduction, which is rich enough to capture both the call-by-value and call-by-name evaluation strategies in the $\lambda$-calculus. Moreover, since substitutions can move through abstractions and reductions are allowed under abstractions (if certain conditions hold), closed reduction naturally provides an efficient notion of reduction with a high degree of sharing and low overheads. We present a family of abstract machines for closed reduction. Our benchmarks show that closed reduction performs better than all standard weak strategies, and its low overheads make it more efficient than optimal reduction in many cases.

This paper studies fundamental connections between profunctors (that is, distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) preserves open maps and open map bisimulation. Consequently, the composition of profunctors preserves open maps as 2-cells. A guiding idea is the view that profunctors, and colimit preserving functors, are linear maps in a model of classical linear logic. But profunctors, and colimit preserving functors, as linear maps, are too restrictive for many applications. This leads to a study of a range of pseudo-comonads and of how non-linear maps in their co-Kleisli bicategories preserve open maps and bisimulation. The pseudo-comonads considered are based on finite colimit completion, ‘lifting’, and indexed families. The paper includes an appendix summarising the key results on coends, left Kan extensions and the preservation of colimits. One motivation for this work is that it provides a mathematical framework for extending domain theory and denotational semantics of programming languages to the more intricate models, languages and equivalences found in concurrent computation, but the results are likely to have more general applicability because of the ubiquitous nature of profunctors.

The study of isomorphisms of types has, in the main, been carried out in an intuitionistic setting. We extend some of this work to classical logic for both call-by-name and call-by-value computations by means of polarised linear logic and game semantics. This leads to equational characterisations of these isomorphisms for all the propositional connectives.

In this paper we introduce a new mathematical modelling technique called Periodic Linear Programming; the periodic properties of Periodic Linear Programs (PLPs) permit the specification of inter-period constraints in embedded systems, in a straightforward and natural manner. We analyse PLPs in which the relationship between program variables is restricted to the class of difference constraints. Our analysis establishes that such PLPs can be reduced to simple linear programs, and hence decided in polynomial time. The class of difference constraints is extremely important from the perspective of embedded systems design, in that it permits the specification of complex timing constraints in real-time specification languages. A PLP can be thought of as a finite-description tool that represents infinite-state systems; although we use this tool purely for the purpose of modelling real-time scheduling problems, PLPs also find applications in other areas, such as concurrency design. In studying this programming paradigm, we develop novel techniques that, to the best of our knowledge, are not part of the literature. We build on the PLP structure to introduce a generalisation called Periodic Quantified Linear Programming; this programming paradigm permits the specification and analysis of uncertainty in the parameters of a PLP. Consequently, a Periodic Quantified Linear Program (PQLP) is the natural modelling tool to capture the requirements of periodic, embedded systems that are characterised by uncertainty in the execution times of processes, periodicity and relative timing constraints. In this paper, we use the PQLP structure to model and solve the periodic version of the zero-clairvoyant scheduling problem. Modelling uncertainty in the problem description is a typical technique used to incorporate a measure of fault-tolerance in the specification.