We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

We present a higher-order call-by-need lambda calculus enriched with constructors, case expressions, recursive letrec expressions, a seq operator for sequential evaluation and a non-deterministic operator amb that is locally bottom-avoiding. We use a small-step operational semantics in the form of a single-step rewriting system that defines a (non-deterministic) normal-order reduction. This strategy can be made fair by adding resources for book-keeping. As equational theory, we use contextual equivalence (that is, terms are equal if, when plugged into any program context, their termination behaviour is the same), in which we use a combination of may- and must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations with respect to normal-order reduction are the same as for fair normal-order reduction. We develop a number of proof tools for proving correctness of program transformations. In particular, we prove a context lemma for both may- and must- convergence that restricts the number of contexts that need to be examined for proving contextual equivalence. Combining this with so-called complete sets of commuting and forking diagrams, we show that all the deterministic reduction rules and some additional transformations preserve contextual equivalence. We also prove a standardisation theorem for fair normal-order reduction. The structure of the ordering ≤c is also analysed, and we show that Ω is not a least element and ≤c already implies contextual equivalence with respect to may-convergence.

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.

Session types allow high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. In collaboration with Malcolm Hole, we previously introduced a notion of subtyping for session types, which was formulated for an extended pi calculus. Subtyping allows one part of a system, for example, a server, to be refined without invalidating type-correctness of other parts, for example, clients. In this paper we introduce bounded polymorphism, which is based on the same notion of subtyping, in order to support more precise and flexible specifications of protocols; in particular, a choice of type in one message may affect the types of future messages. We formalise the syntax, operational semantics and typing rules of an extended pi calculus, and prove that typechecking guarantees the absence of run-time communication errors. We study algorithms for checking instances of the subtype relation in two versions of our system, which we call Kernel S≤ and Full S≤, and establish that subtyping in Kernel S≤ is decidable, and that subtyping in Full S≤ is undecidable.

We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with an equational specification. These tools consist of introducing a monoid of partial maps, listing the monoid relations corresponding to the local confluence diagrams of the rewrite system, introducing the group presented by these relations, and, finally, replacing the initial rewrite system with an internal process entirely sitting in this group. When the approach can be completed, one typically obtains a practical method for constructing algebras satisfying prescribed equations and for solving the associated word problem. The above techniques have been developed by the first author in a context of general algebra. The goal of this paper is to bring them to the attention of the rewrite system community. We hope that these techniques may be useful for more general rewrite systems.

is an untyped continuation-style formal language with a typed subset that provides a Curry–Howard isomorphism for a sequent calculus for implicative classical logic. can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for ; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the λ-calculus, Bloo and Rose's calculus of explicit substitutions λx, Parigot's λμ and Curien and Herbelin's .

was first presented in Lengrand (2003), where it was called the λξ-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).

We model micro-architectures with non-pipelined instruction processing and pipelined instruction processing using Maurer machines, basic thread algebra and program algebra. We show that stored programs are executed as intended with these micro-architectures. We believe that this work provides a new mathematical approach to the modelling of micro-architectures and the verification of their correctness and the anticipated speed-up results.

In this paper we study subtyping for inductive types in dependent type theories in the framework of coercive subtyping. General structural subtyping rules for parameterised inductive types are formulated based on the notion of inductive schemata. Certain extensional equality rules play an important role in proving some of the crucial properties of the type system with these subtyping rules. In particular, it is shown that the structural subtyping rules are coherent and that transitivity is admissible in the presence of the functorial rules of computational equality.

A simple type σ is retractable to a simple type τ if there are two terms Cσ→τ and Dτ→σ such that D ○ C λx.x. The retractability of types is affine if the terms C and D are affine, that is, when every bound variable occurs in them at most once in the scope of its declaration. This paper presents a system that derives affine retractability for simple types. It also studies the complexity of constructing these affine retractions. The problem of affine retractability is NP-complete even for the class of types over a single type atom and having limited functional order. In addition, a polynomial algorithm for types of orders less than three is presented.

Action-labelled transition systems (LTSs) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper we introduce Multiple-Labelled Transition Systems (MLTSs) as generalisations of LTSs that enable us to deal with system features that are becoming increasingly important when considering languages and models for network-aware programming. MLTSs enable us to describe not only the actions that systems can perform but also their usage of resources and their handling (creation, revelation . . .) of names; these are essential for modelling changing evaluation environments. We also introduce MoMo, which is a logic inspired by Hennessy–Milner Logic and the μ-calculus, that enables us to consider state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTSs and both MLTSs and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely μKlaim and the asynchronous π-calculus.

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

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.

Logical relations and their generalisations are a fundamental tool in proving properties of lambda calculi, for example, for yielding sound principles for observational equivalence. We propose a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus. The treatment is categorical, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Our approach has a number of interesting applications, including cases for lambda calculi with non-determinism (where being in a logical relation means being bisimilar), dynamic name creation and probabilistic systems.

We present a new data structure, called a Decomposition Tree (DT), for analysing Boolean functions, and demonstrate a variety of applications. In each node of the DT, appropriate bit-string decomposition fragments are combined by a logical operator. The DT has 2k nodes in the worst case, which implies exponential complexity for problems where the whole tree has to be considered. However, it is important to note that many problems are simpler. We show that these can be handled in an efficient way using the DT. Nevertheless, many problems are of exponential complexity and cannot be made any simpler: for example, the calculation of prime implicants. Using our general DT structure, we present a new worst case algorithm to compute all prime implicants. This algorithm has a lower time complexity than the well-known Quine–McCluskey algorithm and is the fastest corresponding worst case algorithm so far.

Given a map f in the category ω-Cpo of ω-complete posets, exponentiability of f in ω-Cpo easily implies exponentiability of f in the category Pos of posets, while the converse is not true. We investigate the extra conditions needed on f exponentiable in Pos to be exponentiable in ω-Cpo by showing the existence of partial products of the two-point ordered set S={0<1} (Theorem 2.8). Using this characterisation and the embedding through the Scott topology of ω-Cpo in the category Top of topological spaces, we compare exponentiability in each setting and find that a morphism in ω-Cpo that is exponentiable in both Top and Pos is exponentiable in ω-Cpo also. Furthermore, we show that the exponentiability in Top and Pos are independent of each other.

This paper proposes a new relevant logic B+⊓⊔, which is obtained by adding two binary connectives, intensional conjunction ⊓ and intensional disjunction ⊔, to Meyer–Routley minimal positive relevant logic B+, where ⊓ and ⊔ are weaker than fusion ˚ and fission +, respectively. We give Kripke-style semantics for B+⊓⊔, with →, ⊓ and ⊔ modelled by ternary relations. We prove the soundness and completeness of the proposed semantics. A number of axiomatic extensions of B+⊓⊔, including negation-extensions, are also considered, together with the corresponding semantic conditions required for soundness and completeness to be maintained.

The Symmetric Circulant Travelling Salesman Problem asks for the minimum cost tour in a symmetric circulant matrix. The computational complexity of this problem is not known – only upper and lower bounds have been determined. This paper provides a characterisation of the two-stripe case. Instances where the minimum cost of a tour is equal to either the upper or lower bound are recognised. A new construction providing a tour is proposed for the remaining instances, and this leads to a new upper bound that is closer than the previous one.

This paper is the journal version of Lenzi (2006). We consider the positive set theory with equality described these and propose a candidate model.

This paper presents an analysis of definitions and decidability for exponential functions on various matrix algebras. The main idea is to show that, generically, the entries of the exponential (or logarithm) of a matrix are Pfaffian functions of the entries of the matrix.