We consider the following question: in the simply-typed λ-calculus with algebraic operations, is the set of equations valid in a particular model exactly those provable from (β), (η) and the set of algebraic equations, E, that are valid in the model? We find conditions for determining whether βηE-equational reasoning is complete. We demonstrate the utility of the results by presenting a number of simple corollaries for particular models.

There are various logic-based approaches to modelling concurrent programming. The use of logic for system development concerns both the specification step and the study of the operational aspects (through proof analysis and construction) of such development. This means that we have to consider different logical systems for different uses of logic. Moreover, we can also consider concurrency from both points of view: we want to reason and to specify systems where some concurrency aspects are involved, but also to have some operational interpretation of concurrency within logic (focusing on the concept of proof). For this purpose, it seems clear that we have to identify and to study, on the one hand, the role and the treatment of objects (representation, inheritance, modularity, communication, and so on) in this context, and, on the other hand, the interaction of work on proofs and concurrency with the Object-Oriented Programming paradigm.

The ECOOP’96 workshop on ‘Proof Theory of Concurrent Object-Oriented Programming’ took place in Linz, Austria, in July 1996. Its objective was to provide an integrated forum for the presentation of research and the exchange of ideas and experiences in the topics concerned with proofs, concurrency and object-oriented programming (specification, proof development, and so on). The call for papers for this Special Issue of Mathematical Structures in Computer Science can be considered to have been a natural scientific continuation of the workshop.

The papers selected for this Special Issue address some of the topics discussed in the workshop. They present different alternative frameworks that are effectively based on a proof-theoretic approach. They illustrate, from different points of view, the interest, potentialities and difficulties of dealing with such an approach in the design of object-based concurrent systems.

We study the longstanding problem of semantics for input/output (I/O) expressed using side-effects. Our vehicle is a small higher-order imperative language, with operations for interactive character I/O and based on ML syntax. Unlike previous theories, we present both operational and denotational semantics for I/O effects. We use a novel labelled transition system that uniformly expresses both applicative and imperative computation. We make a standard definition of bisimilarity and prove bisimilarity is a congruence using Howe's method.

Next, we define a metalanguage [Mscr ] in which we may give a denotational semantics to [Oscr ]. [Mscr ] generalises Crole and Pitts' FIX-logic by adding in a parameterised recursive datatype, which is used to model I/O. [Mscr ] comes equipped both with an operational semantics and a domain-theoretic semantics in the category [Cscr ][Pscr ][Pscr ][Oscr ] of cppos (bottom-pointed posets with joins of ω-chains) and Scott continuous functions. We use the [Cscr ][Pscr ][Pscr ][Oscr ] semantics to prove that [Mscr ] is computationally adequate for the operational semantics using formal approximation relations. The existence of such relations is based on recent work of Pitts (Pitts 1994b) for untyped languages, and uses the idea of minimal invariant objects due to Freyd.

A monadic-style textual translation into [Mscr ] induces a denotational semantics on [Oscr ]. Our final result validates the denotational semantics: if the denotations of two [Oscr ] programs are equal, then the [Oscr ] programs are in fact operationally equivalent.

This special double issue of Mathematical Structures in Computer Science is in honour of Roger Hindley and is devoted to the topic of lambda-calculus and logic.

It is a great pleasure for us to greet Roger Hindley on the occasion of his retirement from the University of Wales, Swansea, and his 60th birthday. We have known Roger for many years and we have had the chance to collaborate with him and appreciate his intellectual standard, his remarkable mathematical rigor, and his inexhaustible sense of humour. This has enabled Roger to step back critically even in the face of a difficult mathematical task and help to solve it by a new way of looking at it.

Roger Hindley's dissertation concerned the Church–Rosser Theorem and was a significant contribution to the topic. His subsequent work spanned many aspects of lambda-calculus, covering both its models and applications. To mention just a few, he produced work on axioms for Curry's strong (eta) reduction, comparing lambda and combinatory reductions (and models), models for type assignment, and formulas as types for some nonstandard systems (intersection types, BCK systems, etc.).

Roger Hindley collaborated with Jonathan Seldin on two well-known introductory books on the subject (Bruce Lercher also collaborated as an author on the first of these). More recently, he has published an introduction to type assignment. He was also co-author with H. B. Curry and J. Seldin on Combinatory Logic, vol. II, which is an important research publication on the subject.

Roger has played an important role in the lambda-calculus community over the years as that community has grown; in particular, he has been an active organiser of many conferences on the topic. In fact, his success in disseminating knowledge about the lambda calculus, particularly in the United Kingdom, means that Roger may be considered a ‘Godfather’ of ML and its type system.

(In preparing this special issue of Mathematical Structures in Computer Science, we have been fortunate enough to receive too many excellent papers for one double issue. As a result, additional papers by colleagues who wish to honour Roger will appear in future issues of this journal.)

We show that the category whose objects are families of Markov processes on Polish spaces, with a given transition kernel, and whose morphisms are transition probability preserving, surjective continuous maps has semi-pullbacks, i.e., for any pair of morphisms fi:Si→S (i = 1, 2), there exists an object V and morphisms πi:V→Si (i = 1, 2) such that f1∘π1 = f2∘π2. This property holds for various full subcategories, including that of families of Markov processes on locally compact second countable spaces, and in the larger category where the objects are families of Markov processes on analytic spaces and morphisms are transition probability preserving surjective Borel maps. It also follows that the category of probability measures on Polish spaces and measure-preserving continuous surjective maps has semi-pullbacks. A main consequence of our result is that probabilistic bisimulation for labelled Markov processes on all these categories, defined in terms of spans of morphisms, is an equivalence relation.

Inspired by a question of Riecke, we consider the interaction of totality and full abstraction, asking whether full abstraction holds for Scott's model of cpos and continuous functions if one restricts to total programs and total observations. The answer is negative, as there are distinct operational and denotational notions of totality. However, when two terms are each total in both senses, they are totally equivalent operationally iff they are totally equivalent in the Scott model. Analysing further, we consider sequential and parallel versions of PCF and several models: Scott's model of continuous functions, Milner's fully abstract model of PCF and their effective submodels. We investigate how totality differs between these models. Some apparently rather difficult open problems arise that essentially concern whether the sequential and parallel versions of PCF have the same expressive power, in the sense of total equivalence.

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.

Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations.

The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixed points. It has already been applied to the theorem prover Isabelle (Paulson, 1994).

Scott domains, originated and commonly used in formal semantics of computer languages, were generalized by J. Adámek to Scott complete categories. We prove that the categorical counterpart of the result of D. Scott – the existence of a countable based Scott domain universal with respect to all countably based Scott domains – is no longer valid for the categorical generalization. However, all obstacles disappear if the notion of the Scott complete category is weakened to a categorical counterpart of bifinite domains.

We use a syntactical notion of Kripke models to obtain interpretations of subsystems of arithmetic in their intuitionistic counterparts. This yields, in particular, a new proof of Buss' result that the Skolem functions of Bounded Arithmetic are polynomial time computable.

The pioneering work of Hewitt and Baker on the foundations of concurrency during the seventies has inspired the development of the actor model as a promising object-based framework for understanding open distributed systems. So far, theoretical research on actors has focused on identifying the basic primitives of the model and on characterising the operational behaviour of distributed programming languages in terms of actor components. In this paper, we show that the actor model can also be used as a faithful basis for rigorously designing open distributed systems. We argue that a proof-theoretic approach is better suited to this purpose. An abstract-data-type-like axiomatisation of the actor primitives is proposed to support composing and reasoning from specifications of actor communities within a temporal logical system.

Given an automaton, its behaviour can be modelled as the sets of strings over an alphabet A that can be accepted from any of its states. When considering concurrent systems, we can see a concurrent agent as an automaton, where non-determinism derives from the fact that its states can offer a different behaviour at different moments in time. Non-deterministic computations between a pair of states can then no longer be described as a ‘set’ of strings in a free monoid. Consequently, between two states we will have a labelled structured set of computations, where the structure describes the possibility of two computations parting from each other while maintaining the same observable steps. In this paper, we shall consider different kinds of observation domains and related structured sets of computations. Structured sets of computations will be organised as a category of generalised trees built over a meet-semilattice monoid formalizing the observation domain. Theorems allowing us to introduce the usual concurrency operators in the models and relating different models will then be obtained by first considering ordinary functors (on and between the observation domains), and then lifting them to the categories of structured sets of computations.

The theory of algebraic module specifications and modular systems was developed initially mainly on the basis of equational algebraic specifications. We show that it is in fact almost independent of what kind of underlying specification framework is chosen. More specifically, we present a formulation where this framework appears as an indexed category or, equivalently, specification frame. The ensuing theory is called the theory of abstract module specifications. We are able to prove main results concerning the correctness and compositionality of abstract module specifications in a purely categorical way, assuming the existence of pushouts of morphisms between abstract specifications that allow model amalgamation, functor extension and/or suitable free constructions. Then, by instantiating the theory of abstract module specifications to the behaviour specification frame in the sense of Nivela and Orejas, we obtain a theory of behaviour module specifications.

We look at two different ways of interpreting logic in the dependent type system λP. The first is by a direct formulas-as-types interpretation à la Howard where the logical derivation rules are mapped to derivation rules in the type system. The second is by viewing λP as a Logical Framework, following Harper et al. (1987) and Harper et al. (1993). The type system is then used as the meta-language in which various logics can be coded.

We give a (brief) overview of known (syntactical) results about λP. Then we discuss two issues in some more detail. The first is the completeness of the formulas-as-types embedding of minimal first-order predicate logic into λP. This is a remarkably complicated issue, a first proof of which appeared in Geuvers (1993), following ideas in Barendsen and Geuvers (1989) and Swaen (1989). The second issue is the minimality of λP as a logical framework. We will show that some of the rules are actually superfluous (even though they contribute nicely to the generality of the presentation of λP).

At the same time we will attempt to provide a gentle introduction to λP and its various aspects and we will try to use little inside knowledge.

Synthetic domain theory (SDT) is a version of Domain Theory where ‘all functions are continuous’. Following the original suggestion of Dana Scott, several approaches to SDT have been developed that are logical or categorical, axiomatic or model-oriented in character and that are either specialised towards Scott domains or aim at providing a general theory axiomatising the structure common to the various notions of domains studied so far.

In Reus and Streicher (1993), Reus (1995) and Reus (1998), we have developed a logical and axiomatic version of SDT, which is special in the sense that it captures the essence of Domain Theory à la Scott but rules out, for example, Stable Domain Theory, as it requires order on function spaces to be pointwise. In this article we will give a logical and axiomatic account of a general SDT with the aim of grasping the structure common to all notions of domains.

As in loc.cit., the underlying logic is a sufficiently expressive version of constructive type theory. We start with a few basic axioms giving rise to a core theory on top of which we study various notions of predomains (such as, for example, complete and well-complete S-spaces (Longley and Simpson 1997)), define the appropriate notion of domain and verify the usual induction principles of domain theory.

Although each domain carries a logically definable ‘specialization order’, we avoid order-theoretic notions as much as possible in the formulation of axioms and theorems. The reason is that the order on function spaces cannot be required to be pointwise, as this would rule out the model of stable domains à la Berry.

The consequent use of logical language – understood as the internal language of some categorical model of type theory – avoids the irritating coexistence of the internal and the external view pervading purely categorical approaches. Therefore, the paper is aimed at providing an elementary introduction to synthetic domain theory, albeit requiring some knowledge of basic type theory.

This paper shows how it is possible to express many techniques of categorical domain theory in the general context of topical categories (where ‘topical’ means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as ‘generalized topological spaces’ to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.

In this paper we describe a method for proving the normalization property for a large variety of typed lambda calculi of first and second order, which is based on a proof of equivalence of two deduction systems. We first illustrate the method on the elementary example of simply typed lambda calculus, and then we show how to extend it to a more expressive dependent type system. Finally we use it to prove the normalization theorem for Girard's system F.

This paper presents a filter model for π-calculus and shows its full abstraction with respect to a ‘may’ operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder that mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as filters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types and on the construction of terms, which test when an arbitrary term has a fixed type.

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

In constructive theories, an apartness relation is often taken as basic and its negation used as equality. An apartness relation should be continuous in its arguments, as in the case of computable reals. A similar approach can be taken to order relations. We shall here study the partial order on open intervals of computable reals. Since order on reals is undecidable, there is no simple uniformly applicable lattice meet operation that would always produce non-negative intervals as values. We show how to solve this problem by a suitable definition of apartness for intervals. We also prove the strong extensionality of the lattice operations, where by strong extensionality of an operation f on elements a, b we mean that apartness of values implies apartness in some of the arguments: f(a, b)≠f(c, d) ⊃a≠c∨b≠d.

Most approaches to computable reals start from a concrete definition. We shall instead represent them by an abstract axiomatically introduced order structure.

Recall that M is easy if it is consistent with every combinator. We say that M is m-easy if there is no proof with < m + 1 steps that M is inconsistent with any combinator. Obviously, if M is easy, it is m-easy for each m. Here we shall show that for infinitely many m there are m but not m + 1 easy terms.