CLICS II

Categorical Logic in Computer Science II

Project Number: 6811 Technical Annex

Chapter I

Description of the Project

I-1 Project number, title and acronym

Project number  6811
Title of the project Categorical Logic in Computer Science II
Acronym  CLICS-II

I-2 Synopsis

(* See next page *)

Categorical Logic in Computer Science II

CLICS II  6811

Work Area: Semantics and Logics of Programs

COORDINATOR Country Imperial College UK 180 Queen’s Gate London SW7 2BZ

Partners Aarhus University DK CAIMENS F University of Cambridge UK DISI-Genova I Chalmers-TH S Imperial College UK TH Darmstadt G GMD G University of Manchester UK University of Sussex UK

CONTACT POINT Samson Abramsky tel: +44 71 589 5111 fax: +44 71 581 8024

KeywordsCategory theory, Logic, Domain theory, Linear logic, Programming language semantics and logic, Concurrency, Type theory, Constructive mathematics

Start Date October 1, 1992 Duration 36 months

Status Starting

Abstract This Action aims to apply the concepts and techniques of category theory and categorical logic to a number of key areas in Computing Science. These include: the study of type structures for programming languages; the development of structuring principles and axiomatic frameworks for semantics, as a basis for computational logics; and unified treatments of logics and models for parallel computation, and of specification formalisms.

Aims

As the theoretical basis of Computer Science has developed, it is increasingly the case that significant advances in language design, programming methodology, and even language implementation and computer architecture, are based on the insights and analytical techniques made available by theoretical work. These advances are in turn essential for the opening up of new programming paradigms, enabling more sophisticated applications to be developed. Our objectives in the CLICS II project, continuing the existing CLICS I Basic Research Action (BRA 3003), are pitched at this enabling foundational level. We seek to address the following key issues:

• Unification of formalisms. All too many formalisms and theories have been proposed in Computer Science. This impedes understanding of what the really fundamental ideas and structures are, and limits both the depth and the generality of much current work in programming methodology and formal methods.

• Modularity. A key issue in the applicability of formalisms to large-scale examples is the ability to structure theories so as to be able to reuse components. The problem of modularity has obvious practical motivations, but it also raises deep and challenging questions at a foundational level.

• Simplicity. One obvious barrier to the wide-spread use of formal methods is the level of expertise required. How can the needs of practising engineers be reconciled with the increasing sophistication of the mathematical tools and theories currently being developed? One potentially very attractive approach is provided by the notion of internal logic; i.e. that one sets up a theory within some convenient “universe” (e.g. a topos), in such a way that much of the mathematical infrastructure of the theory is absorbed into the setting, so that a “user” of the theory can take a very naive view of it—typically, that he is manipulating sets and functions, in the style of elementary discrete mathematics.

• Statics vs. Dynamics. Traditionally, a sharp distinction has been drawn between denotational/operational, declarative/procedural, logical/computational. A number of recent developments give rise to new ideas for finding a middle ground between these dichotomies; a logical and geometric perspective on the dynamics of computation. This promises a number of exciting applications: deeper structural insights into execution paradigms, leading ultimately to improved architectures; extending useful type disciplines from functional languages to the concurrent process paradigm; extracting computational content from apparently non-constructive reasoning; and developing new geometrical paradigms for symbolic computation.

Approach and Methods

The CLICS project represents an ongoing attempt to tackle these key issues. CLICS I has already made very considerable progress on all these fronts, and encompasses much of the leading research in its area world-wide. The CLICS II programme aims to build on this work in order to make decisive progress in four main areas:

• Domain Theory, • Semantics and Logics of Programming Languages,

• Concurrency and Linear Logic,

• Type Theory and Constructive Mathematics.

The cooperation between partners will be organised around a number of specialized workshops focusing on specific themes: Sequentiality and Stability, Duality in Domain Theory, Logic of inductive and recursive datatypes, Subtypes and polymorphism in higher-order languages, Higher order modal program logics, Monadic programming language semantics, Applied Linear logic, Computational content of Classical logic, Symbolic computation. Each theme addresses issues that span across several or all the main objectives of the action. For each theme, there are several of the partners with strong expertise and interests in that topic.

The action involves partners from 6 countries: Denmark (Aarhus), France (CAIMENS), Germany (Darmstadt, GMD), Italy (Genova), Sweden (Chalmers) and United Kingdom (Cambridge, ICSTM, Manchester, Sussex). Several other researchers have expressed an interest in the proposed work.

Potential

The new formalisms and logical systems which result from the project should contribute to future developments in high-level programming language design and in mechanized checking or derivation of proofs of correctness of computer systems, including concurrent and parallel systems. A number of experimental implementations and case studies will form part of the project. The main potential for exploitation will lie in the fundamental insights and methods made available for more applied work.

I-3 Objectives

I-3.1 Background

Computer Science is fundamentally abstract in character. Software is built out of concepts and their symbolic representations; computation consists of the formal manipulation of these representations. The effective engineering of these abstract entities cannot be based on the traditional engineering foundations from physics; new theories, based on a new kind of “applied mathematics”, are required. Such theories have begun to be developed in Computer Science over the past 30 years: firstly formal languages, syntax analysis and parsing, and the analysis and synthesis of finite state machines; then programming language semantics, formal specification and verification of programs, modelling and verification of concurrent systems, and many more. The kind of mathematics these theories draw on is not the usual engineering mathematics, but rather logic, abstract algebra, lattice theory, and, increasingly, category theory—the mathematics of concepts and structure, rather than that of physical space.

As the theoretical basis of Computer Science has developed, it is increasingly the case that significant advances in language design, programming methodology, and even language implementation and computer architecture, are based on the insights and analytical techniques made available by theoretical work. These advances are in turn essential for the opening up of new programming paradigms, enabling more sophisticated applications to be developed. A few examples of this trend, drawn from a potentially very long list: logic and functional programming; type checking in programming languages; abstract interpretation and partial evaluation; language implementation techniques based on graph rewriting and categorical combinators; interactive machine-assisted proof systems, and their application to hardware and software verification; finite-state model checking of temporal formulae, with applications to verification of protocols and other distributed algorithms.

I-3.2 Key Issues

In our view, this reliance of major advances in software technology on theoretical insights is bound to continue, and indeed to increase. Our objectives in the CLICS II project, continuing the existing CLICS I Basic Research Action (BRA 3003), are pitched at this enabling foundational level. We seek to address the following key issues:

• Unification of formalisms. All too many formalisms and theories have been proposed in Computer Science. This impedes understanding of what the really fundamental ideas and structures are, and limits both the depth and the generality of much current work in programming methodology and formal methods.

A related question is that of the integration of various programming paradigms: logical, functional, procedural, object-oriented, process-based. We believe that this can only be done succesfully on the basis of deepening and unifying the underlying theories for these paradigms.

• Modularity. A key issue in the applicability of formalisms to large-scale examples is the ability to structure theories so as to be able to reuse components. This issue recurs at many different levels: for example, the question of how to modularise the semantic specification of programming languages; and again in the metatheory of formal systems (e.g. in Proof theory), where minor perturbations in the system lead to proofs of key properties such as Cut-elimination having to be restarted from scratch. The problem of modularity has obvious practical motivations, but it also raises deep and challenging questions at a foundational level.

• Simplicity. One obvious barrier to the wide-spread use of formal methods is the level of expertise required. How can the needs of practising engineers be reconciled with the increasing sophistication of the mathematical tools and theories currently being developed? There are several answers to this, one being the distillation of theoretical insights into tools and high-level languages. Another, potentially very attractive approach is provided by the notion of internal logic; i.e. that one sets up a theory within some convenient “universe” (e.g. a topos), in such a way that much of the mathematical infrastructure of the theory is absorbed into the setting, so that a “user” of the theory can take a very naive view of it—typically, that he is manipulating sets and functions, in the style of elementary discrete mathematics.

• Statics vs. Dynamics. Traditionally, a sharp distinction has been drawn between denotational/operational, declarative/procedural, logical/computational. Mathematical structure has chiefly resided in the first term of each dichotomy, computational dynamics and its associated intuitions in the second. A number of recent developments, perhaps most notably Girard’s Linear Logic, give rise to new ideas for finding a middle ground between these dichotomies; a logical and geometric perpsective on the dynamics of computation. This promises a number of exciting applications: deeper structural insights into execution paradigms, leading ultimately to improved architectures, especially parallel architectures; extending useful type disciplines from functional languages to the concurrent process paradigm; extracting computational content from apparently non-constructive reasoning (e.g. obtaining programs from proofs in Classical logic); and developing new geometrical paradigms for symbolic computation.

I-3.3 Technical Objectives

The CLICS project represents an ongoing attempt to tackle these key issues. We believe that CLICS I has already made very considerable progress on all these fronts, and encompasses much of the leading research in its area world-wide; further details are given in Section 9.

The CLICS II programme is structured under four main headings:

1. Domain Theory. Domain theory is the mathematical theory introduced by Scott in 1969 as the foundation for denotational semantics. Since then, it has been extensively developed, and has proved to be an extremely flexible and effective tool in understanding the mathematical structure of programming languages. It has also found increasing applications in semantics-based program analysis and optimisation, and as a theory of partial information in such areas as databases, AI, computational linguistics and constraint programming. The underlying theory itself has continued to develop vigorously, yielding deeper insights and opening up new applications. Our objectives here are as follows:

• Synthetic Domain Theory. Following the major progress made in CLICS I, we believe that the goal is in reach of making Synthetic Domain Theory a fully viable framework for the practice of Denotational Semantics and Program logics. This would have a major bearing on the issue of Simplicity, since Synthetic Domain Theory enables a view of domains as sets and functions, with all continuity and effectiveness considerations absorbed into the framework. It also relates to Unification and Statics vs. Dynamics, since it provides a setting in which domains sit as “observable sets” within a general-purpose non-computational set theory.

• Stability and Sequentiality. One main objective here is to place the relatively limited and ad hoc work on these topics in a much richer and more adequate mathematical framework, exhibiting connections with categorical logic, synthetic domain theory and duality theory. The stable and sequential versions of Domain theory directly address the Statics vs. Dynamics issue, since they precisely aim at bringing computational fine-structure within the denotational framework. As a specific application, we hope to build on current work towards a definitive analysis of sequentiality in programming languages, in the framework of the classical “full abstraction” problem for PCF.

• Categorical Domain Theory. Our aim here is to find a common generalization of domain theory and topos theory in its geometrical aspects. Our work in this direction is already finding applications, in models of rich type theories for functional programming languages, and in the semantics of datatypes. The isssue of Unification is strongly addressed here; with the real prospect of the immense strength of the techniques developed in topos theory being brought to bear on programming language and specification semantics.

• Duality. Our objective here is to study dualities between categories of “spaces” of points (which provide denotations of programs), and categories of “theories”, which allow program properties to be specified. Previous work by one of the members of the consortium [Abr91] provides one of the more striking examples to date of how a deeper mathematical treatment can have an impact on Unification and Modularity. One outcome of the study of dualities in the setting of “standard” Domain theory is to provide systematic methods of deriving a compositional proof system for a program logic from a denotational semantics, and vice versa. Our objective in CLICS II is to extend this kind of treatment to the Synthetic, stable and sequential, and categorical versions of Domain theory.

2. Semantics and Logics of Programming Languages. The main thrust of our work here is to pursue the monadic approach to programming language semantics originated by one of the members of the consortium [Mog91b], and already widely accepted as an important advance in structuring semantic descriptions. This approach promises to yield major advances in tackling the issue of Modularity in both programming language semantics, and the corresponding program logics. The monadic approach also offers a distinctive perspective on the Static-Dynamic dichotomy, with its distinction between computations and values. Another objective is to achieve the integration of computational types with recursive definitions and logic. Finally, we aim to test the monadic approach through some substantial case studies, involving language features which have proved highly resistant to formalization: local variables in higher-order procedural languages, continuations and exceptions.

3. Concurrency and Linear Logic. One major objective here is to unify the highly diverse models and theories of concurrency. Much progress to this end has already been achieved in CLICS I, using the categorical approach introduced by one of the members of the consortium [Win90]. Continuing development of this work has brought out strong links with our other major activity in this area, of Linear logic, and the new perspectives it brings to bear on the issue of Statics vs. Dynamics. Our main objective is to use these insights to develop a version of the Propositions-as-Types paradigm (or “Curry-Howard isomorphism”) for concurrent processes. This would make a useful type discipline available for concurrent programming, and also be a major contribution to the integration of the functional and process paradigms.

4. Type Theory and Constructive mathematics. Our main goal here concerns the issue of Statics vs. Dynamics. Firstly, we aim to build on the very strong line of research pursued under CLICS I by one of the members of the consortium [CG91, Coqb, Coq91a, Coqc], which is opening up new connections between computational notions of streams, processes and transition systems on the one hand, and logical ideas concerning the extraction of computational content from (apparently classical, non-constructive) proofs. We wish to emphasise the importance of non-trivial mathematical proofs as a source of challenging case studies which bring fundamental new notions to light. This work also has a major impact on the question of engineering formal systems, since the experience of actually using such systems, rather than merely studying them externally, raises new topics, of importance in the area of machine-assisted proof.

Another objective concerns new paradigms for symbolic computation, based on a more geometric and structural approach to rewriting. This addresses both Statics vs. Dynamics, and also the unification of the diverse frameworks for rewriting, and their integration with work in mathematics on word problems, combinatorial topology, and knots and braids.

I-3.4 Exploitation

Some promising new formalisms have already emerged from CLICS I, and a number of experimental implementations and case studies have been undertaken. However, the main potential for exploitation of CLICS II will remain the fundamental insights and methods made available for more applied work. The new formalisms and logical systems which result from the project should contribute to future developments in high-level programming language design and in mechanized checking or generation of proofs of correctness of computer systems (including concurrent and parallel systems).

I-4 Baseline and Rationale

The CLICS consortium represents an exceptional concentration of leading researchers in this field. The novelty of our approach is attested by the fact that in many cases the areas we propose to investigate were originated by, or shaped by major contributions from, members of the consortium. (A few examples: Curien’s work on sequential algorithms, Hyland’s work on the Effective topos, Rosolini’s work on Synthetic Domain theory, Abramsky’s work on Domain theory in logical form, Moggi’s work on computational monads, Coquand’s work on the Calculus of Constructions, …). The CLICS consortium can fairly be said to represent a sizeable proportion of the state of the art in its field, and indeed probably comprises the single greatest concentration of expertise in this area world-wide.

The key problem in achieving added value from collaboration is to find the right balance in a consortium between diversity and coherence. One gains most from collaboration if the partners offer a rich combination of different skills and expertise, so that one reaps the full benefits of “interdisciplinarity”. On the other hand, unless there are common themes within a shared framework, this diversity will not be harnessed into fruitful synergy.

As CLICS I has demonstrated, our consortium does achieve this balance, and as a consequence offers a high level of added value. Collectively, we have internationally recognised expertise in the following areas: Category theory, Categorical logic, Realizability, Proof theory, Constructive mathematics, Semantics and logics of programming languages, Concurrency, and a wealth of related topics in Mathematics and Computer Science. We combine this range of expertise with a common focus on key foundational issues (see Section 5), and a common technical framework; we are not all equally expert on the same topics, but we all speak the same scientific language. This is not always the case in Computer Science, which is often disfigured by the mutual incomprehension of competing “schools”.

A key element in our common perspective is provided by the pervasive role of category theory, as a language, conceptual framework, and technical tool. Category theory does not of itself solve any problems; but it provides an indispensable medium for the proper formulation of both problem and solution. The common language it provides also reinforces the cohesion of the consortium.

I-4.1 Baseline of project

We review the context and baseline of our work in each of the main areas of the CLICS II programme.

I-4.2 Domain theory

Synthetic Domain Theory

Classical Domain theory, as originated by Scott, studies categories of domains as certain structured (partially-ordered) sets and structure-preserving functions. Effectiveness considerations must be added, laboriously, via explicit numbering of bases. About 1980, Scott suggested a radically different approach: Synthetic Domain theory (by analogy with Synthetic Differential Geometry [Koc81]), in which the explicit structure witnessing continuity and effectiveness is replaced by properties picking out the “observable sets” within a constructive universe. Hyland’s Effective topos [Hyl82] provided a good candidate for such a universe. However, the setting up of such a theory is attended by many subtleties. The first major step was taken in Rosolini’s thesis [Ros86]; a decisive push towards establishing a viable theory has only been made over the last couple of years, by Hyland’s student Phoa, and by Rosolini in collaboration with colleagues in the U.S.A. [FMRS90]. Then Phoa and Taylor showed how the Plotkin powerdomain construction could be elegantly mirrored within Synthetic Domain theory, and Taylor has shown how most of the theory of fixpoints and solutions of domain equations can ba carried over to Synthetic Domain theory in an elegant fashion [Tay91]. Hyland and Taylor have both worked on axiomatizations of the theory [Hyl]. Most of this work has been carried out under the auspices of CLICS I.

This first phase of intensive activity has demonstrated, at least in principle, that Synthetic Domain theory provides a viable basis for denotational semantics and program logics. The next step will be to carry this through in detail, and to see how some important themes and variations on the standard theory, notably duality, stability and sequentiality, are reflected in the synthetic theory. It will then be possible to reap the full benefits, potentially very great, of the synthetic approach.

Stability and Sequentiality

The semantic characterization of sequentiality, in the presence of higher-order functions, is the real Computer Science content of one of the classic (and still open) problems of programming language semantics, the full abstraction problem for PCF. The idea of stability, leading to a variant of domain theory, was introduced by Berry as an approximation to sequentiality. Then Berry and Curien [Cur86] developed a theory of sequential algorithms on the concrete data structures previously introduced by Kahn and Plotkin. They succeeded in constructing a cartesian closed category of sequential algorithms—a remarkable achievement given the complex and highly concrete nature of the definitions they had to work with. Despite these achievements, the full abstraction problem remained open, and work in this area lay dormant for some years. Then interest in stability was revived by Girard’s work on the functorial semantics of polymorphism, and a new perspective was openened up by Girard’s subsequent discovery of the decomposition of the stable function space into the linear function space and the “of course” comonad, which led in turn to Linear Logic. Taylor and Lamarche have studies the mathematics of stability and its relation to categorical logic in great depth and generality; both are associated with the CLICS consortium. Meanwhile, Curien’s students Bucciarelli and Erhard have studied a new notion of strong stability [BE91], and Erhard and Malacaria have studied dualities for stable functions [EM91].

More recently, exciting progress has been made on the underlying computational problem of the semantic characterization of sequentiality. Cartwright and Felleisen, in joint work with Curien, have proved a full abstraction result for, essentially, the sequential algorithms model extended with errors, with respect to PCF extended with errors and a form of exception handling. This seems to approach quite close to a satisfactory solution to the characterization problem. Stoughton and Jung have also been working on this problem, trying to obtain a more direct understanding of the (unique) order-extensional fully abstract model for PCF, and its relation to the standard model. This raises many hard technical problems.

Thus this area is once again in a vigorous state. There is a real prospect within the course of CLICS II of achieving a definitive solution to the problem of semantic characterization of sequentiality, and, via an appropriate duality, of the “logic” of sequentiality. This would combine denotational and intensional aspects, yielding important insights into the fine structure of computation.

Categorical domain theory

While the possibility in principle of lifting domain theory from posets to categories has always been clear, and some early work was done by Lehmann and Abramsky, a deeper approach, using tools from categorical logic, was initiated by Hyland and Pitts [HP89], who gave a model for the Coquand-Huet Calculus of Constructions using a relative cartesian closed category of toposes and geometric morphisms. Recent work by Vickers has given increased force to the idea that categorical generalizations of domain theory should play a role in modelling abstract data-types. Classes of such generalized domains should provide models for specification languages such as CLEAR and Z, and will in addition have more structure than is reflected in current specification languages.

Much of the duality theory of domains can also be extended to toposes. Just as Stone-type duality connects up propositional geometric theories, frames (the Lindenbaum algebras of such theories) and spaces of points, so in topos theory we have first-order geometric theories, Grothendiek toposes (which by Giraud’s theorem can be seen as generalized frames), and their spaces of “points”, i.e. the categories of models of these theories.

This point of view allows many constructions from domain theory and topology to be generalized to toposes. These constructions, and their interaction with the constructive logic of toposes, make it possible to model higher-order features of type theories. There has been work on these topics by J. Schmidt, who has been employed by CLICS, and by Vickers at Imperial.

I-4.3 Semantics and Logics of Programming Languages

While these topics have been investigated intensively over the past 20 years, many hard problems remain, both technical and methodological. A primary obstacle to making the techniques of semantics applicable to “real” programming languages is that of modularity.

One aspect of this problem is that of structure: large, unstructured, monolithic semantic specifications are as unusable as programs with these characteristics. Another aspect is generality; because of the subtle interactions which may occur between different language features, it is hard to build semantics incrementally, combining well-studied features in a safe fashion.

An important advance was made by Moggi’s proposal of computational monads as a basic structuring principle for semantics [Mog91b]. The idea is that each computational “feature” can be encapsulated as a strong monad T on an underlying category of values; if A is a type of values (i.e. an object) in the underlying category, then T A is the type of computations for values in A. Previous work by Scott, Plotkin, Milner et al. had provided elegant formalisms based on the typed λ-calculus for dealing with higher-order, recursively defined partial functions on datatypes. Moggi’s work has opened up the possibility of directly extending such formalisms to systems which can describe, with similar elegance and utility, more complicated aspects of computation, with imperative as well as functional features. These ideas also have an important bearing on modularity; the idea is to give the semantics of a language in a sequence of steps, each adding a few computational features, and possibly redefining, in a systematic way, some features previously introduced. This requires the development of a calculus of monad transformers.

Another important aspect relates to program logics. Just as Moggi’s monadic approach refines previous work in denotational semantics, so the LCF-style logics pioneered by Scott and Milner have been refined by Pitts, in two directions. Firstly, with his student Crole, he introduced the FIX logic [CP], which introduces a new approach to to recursive definitions based on Moggi’s computational λ-calculus. This succeeds in reproducing a large part of the LCF machinery, including Scott induction, without any explicit introduction of partial orders in the logic. This relates well to recent work by Freyd, and makes an important step towards “axiomatic domain theory”. Subsequently, Pitts introduced Evaluation logic, again based on Moggi’s computational λ-calculus. This is a typed constructive predicate logic, incorporating modal formulas about the evaluation of programs to values. This logic looks promising as a vehicle for developing theories for reasoning about problematic features of imperative languages, such as local variables in higher-order procedures. Once again, the idea is that the elegance and generality of LCF-like logics for functional languages can be lifted to a wider class of computational paradigms.

Another important topic which has been investigated is the compile-time/run-time distinction [Mog89b]. The aim here is to develop a topos-theoretic understanding of program modules, which is able to explain module facilities already available in current programming languages (e.g. Standard ML), and to suggest new ones. The categorical tools used to do this are indexed category theory and the categorical logic of dependent types.

Another important thrust of our work in CLICS I has been subtyping and polymorphism. Subtyping plays a foundational role in the semantics of inheritance in objectoriented languages. Curien and Ghelli have studied coherence and confluence properties of a second-order polymorphic calculus with subtypes and bounded quantification. They have solved a number of hard technical problems, which are basic to the understanding of these key language features.

Rosolini has studied the semantics of the rich type theory of Cardelli’s language QUEST, which combines polymorphism, subtyping and recursive types. His work applies ideas from Synthetic Domain theory to provide the first categorical model for this language. This work also sheds light on the interpretation of parametric polymorphism.

I-4.4 Concurrency and Linear Logic

One major topic in our recent work has been the development of a unified approach to the many extant theories of concurrency, using category theory to study the relationship between various categories of models. Winskel’s extensive work in this area is surveyed and further refined in a joint chapter with Nielsen for the handbook of Logic in Computer Science being published in Oxford Univerity Press. Among the recent results are an adjunction between categories of asynchronous transition systems and Petri nets, one consequence of which is that calculi such as CCS, CSP and OCCAM can be given a Petri net semantics via (a slight refinement of) the usual structured operational semantics. This is a good example of how foundational work using categorical tools can achieve a systematic solution to a problem which had previously been tackled in a piecemeal and ad hoc fashion by many researchers. There is also an intriguing analogy with topological duality theory, which may be exploitable to yield a logic for Petri nets.

Another line of research concerns compositional model checking techniques for deciding whether a concurrent program satisfies a specification [AW]. The particular feature of this work is its compositional and syntax-driven nature, which forms a bridge betwen traditional non-compositional model checking, and compositional proof systems. Categorical techniqes are playing a role here, in formulating appropriate proof systems.

Extensive work has also been carried out under CLICS I in the area of Linear Logic and its applications. Abramsky has studied computational interpretations of Linear logic, in the framework of the Propositions-as-types paradigm [Abr90]. In the Intuitionistic case, this leads to an interesting refinement of the usual typed λ-calculus, in which order of evaluation is captured at the logical level, without introducing the notion of divergence. In the classical case, it leads to a concurrent formalism, with an elegant operational semantics in the style of Berry and Boudol’s Chemical Abstract machine. More recently, Abramsky has studied Linear Realizability; he has formulated an axiomatic notion of Linear Realizability algebra, which captures exactly what is required from a process calculus to enable it to interpret Linear Logic (and hence also, via the interpretation of Intuitionistic Logic into Linear logic, λ-calculus). Such interpretations have been found for Milner’s π-calculus, and for concurrent constraint programming. He then gives a construction which builds a categorical model of (second-order) Linear Logic from a Linear Realizability algebra. The construction is analogous to the usual one of a category of PER’s from a partial combinatory algebra, but embodies some striking new features, in particular the use of the commutativity of “process” composition to give a direct computational explication of the classical dualities of Linear logic.

Lafont has developed the theory of interaction nets, generalizing the proof nets of the multiplicative fragment of Linear Logic to a general paradigm for distributed computation. He has shown the principles of interaction nets to be derivable from very general assumptions about computation. In this framework, it is possible to define a universal interaction system, in which any other system can be simulated in a way which preserves the structure of computations, in particular the complexity and degree of parallelism.

Brown, Gurr and de Paiva have studied categories of Petri nets which yield models of Linear Logic. They use the categorical combinators of Linear Logic to build complex nets in such a way that the behaviour of a net can be expressed in terms of the behaviour of its components. The morphisms in the category correspond to simulations between nets; because the category gives a model of Linear logic, the proof terms of Linear logic provide a notation for simulations. There have also been substantial contributions by Abramsky and Vickers and Brown and Gurr on quantales, and by de Paiva and Hyland on categorical models and proof theory for Linear Logic.

I-4.5 Type Theory and Constructive Mathematics

Computational content of classical mathematics

Coquand has extensively investigated the use of point-free topology in order to get constructive proofs using inductive definitions for combinatorial statements usually proved with non-constructive means [Coqa, Coqb, Coq91a, Coqc, Coq91b]. He has already treated the theorems of Paris-Harrington, Ramsey, Tychonoff, Kruskal and Nash-Williams. A consequence of this work has been the discovery of a new proof for the finite Ramsey theorem. The analysis of Ramsey’s theorem has led to the use of sheaf models, and suggests promising connections with Martin-Lof’s ideas of representing non-deterministic programs in this way. This work has also exhibited the fruitful interplay betwen Computer Science notions of process, stream and transition systems, and ideas from constructive mathematics such as choice sequences.

Symbolic Computation

Curien has studied coherence problems arising from the theory of dependent types, and used Penrose diagrams to perform the complex 2-categorical calculations involved. Subsequently, Lafont has built on the work of Burroni on higher-dimensional word problems to investigate Penrose diagrams as a new framework for symbolic computation. This raises interesting foundational questions, e.g. about the adaptation of Knuth-Bendix techniques to this more geometric framework, and also the practical goal of developing an interactive editor for drawing and transforming such diagrams.

Normalization proofs

Hyland and Ong have been developing a general approach to proving strong normalization theorems for various type theories; this addresses the problem of modularity as it arises in Proof theory. They replace the usual complex syntactic criteria on “candidates” by a semantic approach, using realizability ideas. This work promises to isolate the core of the proof of strong normalization for impredicative systems.

There has also been notable work by Pitts on “almost quantifier elimination” for second-order intuitionistic propositional logic [Pit], and by Ritter on categorical combinators for the Calculus of Constructions [Rit91].

Connections with other BRA projects

Types Chalmers is involved in Types as well as CLICS II. Their work on Types is mainly concerned with developing proof environments for Type theory, while that in CLICS II focusses on computational content of Classical logic, and the foundational study of inductive and coinductive types.

CONFER Imperial and ENS are involved in CONFER as well as CLICS II. CONFER is concerned with combining functional and process calculi, focussing on reduction strategies, operational semantics, and encodings of functional languages in process calculi. CLICS II is concerned with developing unified semantic frameworks, with major emphasis on types and program logics.

CONCUR, REACT These concurrency projects have no intersection of membership with CLICS II. They focus on specific approaches to concurrency using process algebras, and tools for analyzing concurrent systems respectively. By contrast, CLICS seeks to unify concurrency with other aspects of computation.

In general terms, we see CLICS II as clearly complementary to these other projects, and also as often working at a more foundational level. We will attempt to keep a flow of information between CLICS and related BRA projects, using our common membership of some projects, and also by inviting representatives from other projects to our Workshops as appropriate.

Chapter II

Programme of Work

II-1 Introduction to Workplan

The workplan is divided into nine research Topics. The scientific content of these topics is described in Section II-2. An estimate of the man-months to be devoted to each topic by the collaborating partners is given in a Table in Section II-2. The expected dependency and timing of the Topics are given below. As with any basic research, it is impossible to predict accurately what research will be done during a given period of time. Moreover, new ideas and links are liable to develop during the lifetime of the project. We will stimulate work on selected Topics by holding small workshops focused on specific topics involving only the relevant collaborating partners. The first such workshops will be on ”Evaluation Logic” and “Games, Processes and Logic” (Topics G and H); topics for subsequent workshops will be chosen at the review points. Progress will be checked, and the Workplan adapted accordingly, by means of the business meetings, involving all partners, planned to coincide with the project review points (see Section II-2).

Topic A Sequentiality and stability.

Collaborating partners: Aarhus, Cambridge, Darmstadt, CAIMENS, Genova, Sussex. Interacts with B. Timing: months 0–24.

Topic B Duality in Domain Theory.

Collaborating partners: Aarhus, Cambridge, Darmstadt, CAIMENS, GMD, Imperial, Manchester. Interacts with A. Timing: months 0–36.

Topic C Logic of inductive and recursive datatypes.

Collaborating partners: Aarhus, Cambridge, Chalmers, Genova, Manchester.

Receives input from B. Interacts with E.

Timing: months 0–24.

Topic D Subtypes and polymorphism in higher order languages.

Collaborating partners: CAIMENS, Genova, Manchester, Sussex.

Depends on C.

Timing: months 6–30.

Topic E Higher order modal program logics.

Collaborating partners: Cambridge, Genova, Imperial. Interacts with C. Timing: months 0–24.

Topic F Monadic programming language semantics.

Collaborating partners: Cambridge, Genova, Sussex. Receives input from E. Timing: months 6–36.

Topic G Applied Linear logic.

Collaborating partners: Aarhus, Cambridge, CAIMENS, GMD, Imperial. Timing: months 0–36.

Topic H Computational content of classical logic.

Collaborating partners: Chalmers, Imperial, Manchester. Timing: months 0–36.

Topic I Symbolic computation.

Collaborating partners: Cambridge, Chalmers, CAIMENS, Genova, Manchester. Receives input from G and H. Timing: months 6–36.

Risk Assessment

The progress of basic research of the kind involved in CLICS II is notoriously difficult to predict. A line of enquiry which may initially have seemed promising may lead (at least temporarily) to a dead end, while new perspectives may emerge, causing major shifts in emphasis. Indeed, CLICS I provides a splendid example of the latter phenomenon. Synthetic Domain theory and Linear Logic were both just small clouds on the horizon at the time that the original proposal was written, but came to assume major importance during the lifetime of the project.

However, we will make some tentative comments about the objectives listed in Section I-3, relating them to the Topics listed above.

1. Domain Theory. Much of this work is in a relatively mature state, following the progress made in CLICS I. Much of what we propose to do in CLICS II is in the nature of synthesis and refinement rather than breaking fundamentally new ground. We are therefore quite confident of making good progress here, particularly in Topics B and C. However, challenging fundamental problems still exist in the area of sequentiality and the full abstraction problem for PCF (Topic A). Although encouraging progress has been made recently, it is hard to know exactly where our work in this area will lead.

2. Semantics and Logics of Programming Languages. This work has as a platform the considerable progress made in CLICS I on monadic semantics and Evaluation logic. However, the proposed case studies in Topic F (see the Workplan in the next Section) are very challenging, and we cannot be completely confident of success. However, we believe that the tools at our disposal are more powerful than those available in previous work on these questions, so that even if these case studies are not completely successful, much will be learned from the attempt. The work on Topics D and E relates in part to the work on Domain theory. However, as already explained, the work it relies on has already largely been developed in CLICS I and elsewhere, so we do not envisage major dependencies between these topics and topics A–C.

3. Linear logic and Concurrency. Work on Linear Logic continues to develop rapidly. Very recent work on game semantics looks to have considerable potential, with applications to many of the other areas of CLICS II. So we are confident of significant progress on topic G. However, the key objective of obtaining a useful version of Propositions as Types for concurrency is difficult, and success cannot be guaranteed. It may well be that a somewhat looser coupling between logic and concurrent computation, more akin to realizability, is the best that can be achieved. Even this would offer a major advance on the current state of the art.

4. Type theory and Constructive Mathematics. The work on computational content of Classical logic continues to look very promising. In particular, there seems a good chance of strong interactions between topics G and H, centred on game semantics. However, it is simply too soon to tell how this will work out.

The work on topic I concerning the geometric approach to rewriting involves some challenging fundamental problems. Progress is therefore difficult to predict. The work on Type Theory-related tools is more mature, and we are correspondingly more confident that good progress will be made.

As a general remark, we see more opportunities than risks in the connections between topics. That is, there are many possibilities of cross-fertilisation from one area into another, reflecting the coherent framework of the project as a whole. On the other hand, it is not really the case that success in one topic is an essential precondition for progress in another. This stems from the fact the each topic is building on the progress made in CLICS I, and related work. This allows us to work on a broad front, and to be quite flexible in adapting to developments as they arise—which is in our view quite essential for the sensible management of Basic Research.

II-2 The Workplan

This section sets out a series of research Topics that will be pursued in order to achieve the Technical Objectives described in section I-3. Each Topic requires the technical expertise of several partners. For each, we list the partners that will collaborate on it and outline the approach that will be taken.

Topic A: Sequentiality and stability

Collaborating partners: Aarhus, Cambridge, Darmstadt, CAIMENS, Genova, Sussex

This topic contributes to the project objectives in the areas of Domain Theory and Semantics of Programming Languages. We hope to build on current work to get a better analysis of sequentiality in programming languages, in the framework of the classical “full abstraction” problem for PCF.

We propose to study Milner’s fully abstract model M of PCF inside the standard model E built up from flat domains and Scott-continuous functions. Two issues arise. Firstly, we want to study how elements of E that are denotable in PCF can be distinguished from ones that are non-denotables. This question is in the same spirit as [Plo80], and recent work by Kurt Sieber using logical relations should bear fruit here. Secondly, we would like to give a concrete representation for Stoughton’s construction of M as an continuous quotient of the inductively reachable submodel, R(E), of E [Sto88]. We have already shown that a copy of M sits inside R(E) as the image of a continuous projection. This in itself provides the perhaps simplest description of M available at the moment. However, many basic questions about this projection appear to be difficult and deep. For example, we do not know whether the projection itself is PCF-definable, whether it is a homomorphism with respect to application, how it behaves on pure lambda-terms or whether it maps denotable elements to denotable elements. A similar study was undertaken by K. Mulmuley in 1987 [Mul86], in which M was studied as the image of a closure operation inside the continuous function model based on flat lattices. It seems that the two constructions are related to each other and that clarifying this connection will shed light on both as well as on M.

The new results obtained in CLICS I regarding the understanding of sequential algorithms and functions are very encouraging towards the goal of grasping the logic of sequentiality. The current joint work of Curien with Cartwright and Felleisen raises a number of questions. The extended sequential algorithms obtained by incorporating the notion of error values in the framework of concrete data structures turns sequential algorithms in real functions from extended concrete data structures to extended concrete data structures. Is there an abstract order-theoretic characterization of these functions. Can the theory be developped more abstractly? In this respect, connections with the interesting work developed by Brookes and Geva at CMU on the understanding of intensional semantics in terms of comonads should be looked at. Another problem stems from work at Aarhus on a “timing functor” for measuring the time taken to fill a cell in a concrete date structure, which led to the realisation that Berry and Curien’s sequential algorithms do not support sharing. This lack caused fundamental difficulties in extending the timing construction to a functor—only by cutting-down to “linear” algorithms could a functor, indeed a monad, be obtained. We would like to extend the model of concrete data structures and sequential algorithms to support sharing of the kind required to give a proper account of the computation time of sequential algorithms.

Stability is a condition intermediate between Scott continuity and sequentiality, which was discovered by Berry (and later rediscovered by Girard, for whom it was an essential ingredient in the birth of Linear logic). Work on Synthetic Domain Theory has hitherto concentrated on axiomatizations of analogues of Scott domains in terms of the recursively enumerable subset classifier Σ. It seems likely that we can axiomatize stable domains in a similar fashion. Indeed quite a lot follows from stipulating that 2^{Σ} ≅ 2 and Σ^{Σ} ≅ 2_{⊥}; but surely there are some more general principles. Also we should seek the principles essential to the variations on stability and sequentiality. We will be guided by looking at specific candidates for toposes that model a stable version of Synthetic Domain Theory. Here the idea will be to generate toposes (possibly only pretoposes) starting from a quantale to produce a canonical calculus of relations, and find in such a setting a good notion of partiality.

Topic B: Duality in Domain Theory

Collaborating partners: Aarhus, Cambridge, Darmstadt, CAIMENS, GMD, Imperial, Manchester

This topic contributes to the project objectives in the area of Domain Theory. Stone duality has been used in the context of computer science to connect logical specification and observation of programs with their denotations in certain categories of domains and continuous functions. We would like to extend this in several ways. Connecting with Topic A, we would like to produce a similar duality theory for the case of stable functions: we need to understand how to present locale-like structures for stability, in order to understand the logic of stability. We will also consider what notion of dual representation (or locale) we have in the context of Synthetic Domain Theory—that is, what is the logic of r.e. subsets. Abstractly the answer seems clear for the case of small ‘complete’ categories; we should consider the category of ‘limit’-preserving functors on the category of replete objects. But we lack the constructions at the level of presentations of locales which play a central role in Abramsky’s Logic of Domains.

Traditionally, domain theory deals with algebraic dcpo’s, thus excluding natural data types such as measure spaces or the real numbers. Widening the concept of ‘domain’ to include continuous dcpo’s easily subsumes these spaces. For example, the recently introduced probabilistic powerdomain [Gra88, JP89, Jon] automatically leads to continuous domains and in fact maps a certain class of continuous dcpo’s, ‘FS-domains’, (cf. [Jun90]) into itself. It appears open what an observable property of a probabilistic process should be; we wish to address this problem by developing a suitable domain logic. The lattice of Scott-open subsets of an FS-domain is completely distributive, a property which is retained if we turn this lattice upside down; constructing the space of points from this reversed lattice we get a natural dual space, but it is not in general an FS-domain. It therefore seems profitable to consider the wider class of stably locally compact (sober) spaces, which is closed under such dualization. For such spaces there are not enough subsets which are both open and compact, which forces us to interpret these two basic concepts separately. It is well established that open sets model observable properties of computation, but we lack a similarly clear understanding of compactness. In [Smy] it is suggested that the right information systems for stably locally compact spaces are the so-called proximity lattices and we will examine this claim by incorporating the above observations about compact saturated subsets and by developing a corresponding domain logic.

Going beyond the order-theoretic setting, we wish to extend the use of duality theory to encompass Categorical Domain Theory. Toposes have a dual nature; besides being constructive set-theories they can also be seen as generalized spaces and their categories of points as generalized domains. So, many constructions from topology and domain theory have topos-theoretic analogues. These constructions and their interaction with the constructive logics of the toposes make it possible to model higher-order features of type theories, such as type universes. The initial work by Hyland and Pitts in [HP89] has been extended by J. Schmidt [Sch], but many more models need examination. For example, we will examine the possibility of a relative cartesian closed category arising from the classifying toposes of Diers’ theories. Here there will be links with Topic A, since these theories are also closely connected with the concept of stable domains and stable functions. Recent work of Vickers has given increased force to the idea that categorical generalizations of domains should play a role in modelling data types. Classes of such generalized domains should provide models for languages in the style of CLEAR and Z, and will in addition have more structure than is reflected in current specification languages. We will study the models and extract appropriate languages.

Topic C: Logic of inductive and recursive datatypes

Collaborating partners: Aarhus, Cambridge, Chalmers, Genova, Manchester

This topic contributes to the project objectives in the areas of Type Theory and Semantics and Logics of Programming Languages. Principles for reasoning about simple inductive types (lists, trees, etc) are well established. We seek to establish similar principles for wider classes of recursively defined types.

One direction of research is to make precise an alternative explanation of closely connected induction schemes, that we can call “semi-positive inductive definitions”, whose characteristic is that they seem to require more than the usual Tarski fixed-point theorem, because of an apparent negative occurence in the definition. An early occurrence of such a definition for universes appears in Martin-Löf 1972 [ML72], and was explained in P. Aczel 1980 [Acz80] for Frege structures. Other instances of such definitions occur for defining logical relations [Coq90] and the Tait reducibility predicate for dependent types [ML72]. The alternative explanation of these definitions is best described by saying that it can be seen as completing P. Aczel’s explanation by an explicit consideration of proof objects.

We will also study datatypes of streams and the logic of the infinite objects they contain. P. Martin-Löf’s approach can be seen as representing a stream as the generic sequence in an extension of the current type theory we are working with. It seems that this idea can lead to a possible expression of logic of streams. Another approach is due originally to Lars Hallnäs, who has shown how to represent bisimulation using only ordinary recursion on natural numbers (and not, as usual, as a greatest fixed-point operator). Also here the idea of explicit consideration of proof-objects was essential, for it is via this consideration that the transfinite induction used in the ordinary definition of bisimulation (for transition systems that are not necessarily finitely branching) is reduced to ordinary induction. Recently, Nax Mendler has reconsidered this idea from a categorical point of view. We would like to understand if it is possible to do this reduction in an intensional framework, or if Mendler’s use of extensionality is essential. We hope to get a representation of streams and the logic about them in a Type Theory which has only ordinary induction operators. This will be an alternative to the addition of coinductive operators to Type Theory. One possible application of this work is a predicative constructive version of the functional programming approach to concurrency proposed by Dybjer and Sander. References are [Hal87, Lin89, Men91, DH89].

Finally, we will consider completely unrestricted recursive type definitions—one of the characteristic features of the current generation of strongly typed, higher order functional programming languages. Existing techniques for solving recursive domain equations provide models of these datatypes, but the domains that result can be exceedingly complicated and difficult to reason about; in particular no good induction principles exist for them. To get such principles one must examine the interaction between recursive definitions and partiality. We intend to investigate this in a setting combining O-category and computational monads. Recently Freyd has provided a promising new axiomatic approach to recursive domain equations. He studies abstract conditions on a category that suffice for modelling recursive types with strong properties. These conditions involve the existence of objects that are simultaneously inital algebras and final coalgebras for functorial type constructors. We will apply the methods of categorical logic to Freyd’s ideas: from his purely category-theoretic approach we would hope to develop a corresponding logic. Specifically, we will do this in the context of the computational lambda calculus and Evaluation Logic in order to tie this approach to recursive types in to the treatment of recursive functions via the notion of ‘fixpoint’ object given in CLICS I [CP]. (Freyd’s work already suggests a useful strengthening of the notion of fixpoint object.) Initial algebras are known to give rise to corresponding induction principles. More intriguingly, it seems that Freyd’s final coalgebra property should give rise to a general ‘co-induction’ technique involving bisimulations between computations (a particular example of which occurs in the work of Abramsky and Ong on lazy λ-calculus).

Topic D: Subtypes and polymorphism in higher order languages

Collaborating partners: CAIMENS, Genova, Manchester, Sussex

This topic contributes to the project objectives in the areas of Type Theory and Semantics of Programming Languages. Recent work by Abramsky, Mitchell, Scedrov and others on an abstract understanding of logical relations seems among others to offer a good explanation of so far “ad hoc” looking constructions for the modeling of the recursively defined types to be studied in Topic C. On the other hand subtyping receives a natural interpretation in a relational framework (in terms of inclusion of relations). This gives some hope of getting a rather simple, abstract and elegant understanding of the combinations of recursive types and subtyping, of which only quite technical models are known at the moment. Mitchell while visiting Paris has presented interesting ideas in this direction, and P.-L. Curien, who will be visiting DEC SRC, Palo Alto in 1992, would like to pursue this line of research next year, in connection with M. Abadi, L. Cardelli and J. Mitchell, who are prominent researchers in the area. This can give a valuable input to the European project.

A new method for producing models for the calculus of constructions of Huet-Coquand has been described by Rosolini and Robinson, and independently by Phoa. There are certain peculiar features of this new interpretation: besides exhibiting a better categorical behaviour, it retains part of the information about the variance of the variable types appearing, in fact sufficient to allow reconstruction of the functor in case the type was the restriction of one. The first basic results are in preparation. The next step in the research will be to expand the interpretation to include subtypes and recursive types. Because of the categorical/functional nature of the models, it will be necessary to introduce explicit coercions first, and then prove something in the lines of a coherence theorem as suggested in [BTCGS91]. This would produce the first categorical model where a strong extension of polymorphism is paired with subtypes and recursive types.

Topic E: Higher order modal program logics

Collaborating partners: Cambridge, Genova, Imperial

This topic contributes to the project objectives in the areas of Semantics and Logics of Programming Languages and Domain Theory. Scott and Milner’s classical LCF (see [GMW79]) approach to program correctness is based on a logic of domains. Programs are represented as λ-calculus terms using the techniques of denotational semantics; correctness assertions become LCF formulas involving these terms. On the other hand, the program logics proposed up to now (Hoare’s Logic, Dynamic Logics, Modal and Temporal Logics for Concurrency, see [KT90], and Reynolds’ Specification Logic, see [Rey81]) are tailored to specific programming languages (usually small languages with a very reduced set of datatypes) and programs enter into formulas via program modalities, rather than as terms. We intend to keep the general ideas of the LCF approach, namely: programs are represented by lambda terms, and correctness assertions correspond to formulas; and reasoning about programs is achieved by reasoning about the mathematical structures for program semantics. At the same time we intend to achieve a more transparent logic, along the line of Pitts’ Evaluation Logic (see [Pit91, Mog91a]). As it stands this logic lacks the full expressive power of (constructive) higher order logic: many set-theoretic constructions one would like to make in connection with denotational semantics cannot be carried out within it. We will try to extend Evaluation Logic to an intuitionistic higher order logic and consider whether and how modalities from existing program logics fit into such a logic.

We will also seek to integrate the work in CLICS I on program metalogics with another important strand of that project—the ‘synthetic domain theory’ of Hyland [Hyl], Phoa, Taylor, which has axiomatized computation theory within constructive higher order logic (reducing computational domains to a certain class of unstructured sets within the theory). One way of proceeding would be to study the internal logic of suitable toposes that both contain a standard model of the (predomains and inclusive subsets of them) as a full subcategory, and also model synthetic domain theory (i.e. contain internal small full subcategories of domain-like sets).

Topic F: Monadic programming language semantics

Collaborating partners: Cambridge, Genova, Sussex

This topic contributes to the project objectives in the area of Semantics and Logics of Programming Languages. When a programming language is extended its semantics needs to be extensively redefined. This is a major problem, when one is trying give semantics to real programming languages (see [Mos89]). The monadic approach may provide a way of approaching the problem of modularity, since in several case studies with monads it was possible to give a uniform redefinition (see [Mog89a, Mog90]). Other research in this area has led to methodologies for managing denotational specifications (see [Mos88]), but has not addressed the issue of constructing complex denotational models stepwise. The conceptual simplicity of our approach may also suggest a more uniform and systematic methodology for the specification of programming languages. We will also try to extend the stepwise construction of models for metalanguages to models for the Logic produced in Topic E. More specifically, we want to identify the modalities associated to monad transformers, how they should be redefined and study what theorems still hold after redefinition.

We will consider various test cases for the applicability of the methods described above. These tests centre around the aim of understanding better what are the fundamental principles underlying the observable behaviour of local state. Experience has shown that for programming languages with both local declarations and higher order features (procedures, functions), it is very difficult to give a denotational semantics that captures exactly (or at least reasonably closely) the observable behaviour of programs—i.e. the models lack abstraction. Most work on this problem has been done in the context of Algol-like languages: the work of Halpern, Meyer, Trakhtenbrot and Seiber modifying the classic Store Model, and the work of Reynolds, Oles, Tennent and O’Hearn using functor categories [Ole85, Ten90] are important examples. We will test our approach to programming semantics by seeing whether the treatment of local variables and interference (see [Ten90, O’H90]) fits in the monadic approach. We will test the expressiveness of the logic from Topic E, by considering small programming languages with imperative features such as exception mechanisms and dynamic allocation, and developing corresponding program logics for observable behaviour of programs. Then we will test the modular approach to program logics, e.g. by developing a program logic for a programming language of complexity comparable to that of idealised ALGOL via a modular approach, rather than directly as done for Reynolds’ Specification Logic.

Topic G: Applied Linear logic

Collaborating partners: Aarhus, Cambridge, CAIMENS, GMD, Imperial

This topic contributes to the project objectives in the area of Concurrency and Linear Logic. The proof terms of Linear logic can be thought of as constituting a parallel program language (see, for instance, [Abr90]). There is another promising categorical interpretation of Linear logic stemming from the work of [Bro, BGdP]. There, categories of Petri nets are exhibited which form models of Linear logic. The categories are very closely related to those which have arisen as models of parallel programming languages like CCS and CSP with the morphisms representing a form of simulation (or refinement). In such models the proof terms of Linear logic can serve as a notation for simulations, and this shows promise of being a useful reasoning technique. It would be interesting to relate this reading of the proof terms to the computational intuitions given in [Abr90].

Abramsky’s more recent work on Linear Realizability and Geometry of Interaction [AJ92] has opened up a number of promising lines of investigation. There is a definite prospect of achieving a version of the Curry-Howard isomorphism, which has proved so fruitful in the functional programming paradigm, for concurrent processes. There are also important issues arising from the construction of models of Linear logic out of Linear realizability, which have an important bearing on questions of the computational content of classical logic; in particular, the internal aspects of these models, and extensionality in higher-order Linear Logic will be investigated.

Lafont’s work on interaction nets has shown that they are a promising model for asynchronous distributed computation. Further work will examine the expressiveness of this framework, and the possibility of parallel implementation.

There has been success in CLICS I in organising and relating models for parallel computation by regarding them as categories. However it is not yet clear how to give a categorical account of hiding (making events internal) and changing levels of atomicity to support refinement (some initial ideas for which appear in [NRT90]). The tie-in with operational semantics will be more thoroughly worked-out. As yet it is not clear how to extend the approach to models based on equivalences, like bisimulation. The categorical models (especially the adjunction between categories of Petri nets and asynchronous transition systems) provide some hints as to the nature of logics for processes. A form of Linear logic looks promising as a logic for several forms of Petri nets. This treats logic on an individual net. At another level, the category of nets is closely related to one which is a model of Linear logic.

Topic H: Computational content of classical logic

Collaborating partners: Chalmers, Imperial, Manchester

This topic contributes to the project objectives in the area of Type Theory and Constructive Mathematics. We will pursue the analysis of the use of point-free topology in order to get constructive proofs using the notion of inductive definition for combinatorial statements usually proved with non-constructive means such as compactness theorems, König’s lemma, or the minimal bad sequence argument. So far, we have covered the case of Paris-Harrington, Ramsey, Tychonoff’s theorem and Nash-Williams minimal bad sequence argument [CG91, Coqa, Coqb, Coq91a, Coqc]. We know how to do Kruskal’s theorem in this framework, but this has not yet been published. A consequence of this work has been the discovery of a new proof for even the finite Ramsey’s theorem. While analysing this proof, it appeared to be best presented using a sheaf-theoretic language, and there seem to be deep connections with Martin-Löf’s idea of representing non-deterministic programs using sheaf models. An invited paper presented at the last LICS meeting, on a constructive and ‘dynamic’ presentation of a known proof of the infinite version of Ramsey’s theorem, has shown how much the terminology, notation and basic concepts of concurrency theory (like transition systems, temporal logic, operators on processes) can bring to constructive mathematics (especially the study of so-called choice sequences.) Since these proofs are using inductive definitions, there are clear connections with Topic C. This research is also complementary to, and in part motivated by, recent work connecting the theory of locales and several concepts in computer science [Abr91].

Topic I: Symbolic computation

Collaborating partners: Cambridge, Chalmers, CAIMENS, Genova, Manchester

This topic contributes to the project objectives in the area of Type Theory and Constructive Mathematics. It is clear from the work on Logical Frameworks how essential, on a practical level, it is to extend Type Theory with explicit substitutions, a calculus of contexts, and interpretations between contexts. This has clear connections with the work in CLICS I on categorical models of type theory. Categories used for this purpose have contexts as objects, and interpretation between contexts as morphisms. Implementations of the Calculus of Constructions based on such models are being developed. We want to use such ideas to try to analyse possible internalisations of normalisation theorems in Type Theory. It is not clear yet if it has to be using categorical combinators, or if a different approach, closer to the concrete syntax is better. We hope that recent work of Martin Hyland and Luke Ong in Cambridge will be relevant here too: it has led to a fresh semantic presentation of the strong normalization proofs for constructive type theories. This work needs consolidating and extending, and is likely to lead to important issues of coherence and the explicitness of syntax, where there should be interaction with any continuation of the LF research action.

We will also pursue a new paradigm for symbolic computation, based on a more geometric and structural approach to rewriting. Penrose diagrams are playing an increasing role in various areas in mathematics, theoretical physics and theoretical computer science. They express in a concise and geometric way proofs that would be awkward otherwise. They were successfully used by P.-L. Curien to tackle a coherence problem in the categorical semantics of type dependency (see 90/91 report of the previous CLICS project). We will pursue two directions of research here. Firstly a theoretical one, using Albert Burroni’s framework for higher-dimensional word problems. We are particularly interested in rewriting theory of Penrose diagrams; this implies the adaptation of the Knuth-Bendix framework to this more geometric framework. Secondly, a practical one, consisting in the development of interactive editors for drawing and transforming such diagrams (those tools would be directly usable by mathematicians).

II-2.1 Review points and milestones

There will be three milestones associated with this project: Milestone 1 at month 12. Milestone 2 at month 24. Milestone 3 at month 36.

The following chart shows the expected timing and interdependencies of the Topics A–I in the Workplan together with the timing of the review points, which will coincide with the project milestones.

[figure: month →; 0; 6; 12; 18; 24; 30; 36; \begin{matrix}topic \\ ↓ \end{matrix}; I; H; G; F; E; D; C; B; A; dependency ; ↓; review point →; ×; ×; ×]

The following table shows the effort in man-months (including non CEC-funded labour) to be devoted to each of the Topics A–I in the Workplan by each partner.

Topic A B C D E F G H I
Imperial  30  7  30 5  72
Aarhus  20 20 7  25  72
Principal CAIMENS 25 10  5  12  20 72
sites  Cambridge 10 10 12  12 12 10  6 72
Genova  3  3 6 6 9  3 30
Chalmers  12  12 12 36
Darmstadt 18 18  36
Associate GMD  10  2  12
sites  Manchester  8 8 8  4 8 36
Sussex  7  7  7  21
Total man-months 83 106 42 26 25 28 79 21 49 459

II-2.2 Deliverables

The Project deliverables will take the form of publications, research reports, and experimental implementations. A research report detailing progress with the Workplan Topics will be delivered at each Project Milestone. Each report will be accompanied by selected publications. All deliverables will have status P (Public).

The structure of the research reports will be as follows:

• Overview of the progress made in CLICS II in that year, difficulties encountered, major advances etc. This will be written by the coordinator.

• A detailed account, for each topic active in that year of the project, of progress made in that topic. This will be written by a designated “topic leader”. The initial assignment of topic leaders is as follows:

A P.L. Curien
B M. Hyland
C P. Dybjer
D G. Rosolini
E A. Pitts
F E. Moggi
G G. Winskel
H T. Coquand
I Y. Lafont

The topic reports will reference an associated list of publications produced within the project during that year; these will be included as an appendix.

The experimental implementations will be demonstrated at the Review meetings, and at the Project Workshops. Descriptions of these implementations will be included in the research reports, as appendices to the relevant topic reports.

Deliverables for Milestone 1

We anticipate reporting on (at least) the following specific work within each topic:

Topic A Connections between Linear logic, games and sequential algorithms. Full abstraction results for variants of PCF with sequential control operators.

Topic B Categorical domain theory: bagdomains, applications of geometric logic to internalise categories of domains. Duality theory for stable domains.

Topic C Proof principles for inductive and coinductive types, connections with algebraic compactness.

Topic D Semantic criteria for parametric polymorphism, and their equational consequences. Semantics for over-loading and sub-typing in object-oriented languages.

Topic E Evaluation logic for references in (a subset of) Standard ML.

Topic F Monadic semantics for references in (a subset of) Standard ML.

Topic G Game semantics for Linear logic, strong completeness results, connections with type theory and concurrency.

Topic H Game semantics for Classical logic, connections with Linear logic, applications to extracting computational content of classical proofs.

Topic I An experimental implementation in Standard ML of categorical abstract machines for reduction and type synthesis in the Calculus of Constructions. An experimental implementation in Standard ML of a Linear functional programming language based on Linear Logic, including ML-style polymorphic type reconstruction for Linear types, and compilation guided by Linear type information.

Deliverables for Milestones 2 and 3

Because of the nature of the CLICS II project, with the precise results being very hard to predict, we believe that the most appropriate way to proceed is to specify the Deliverables for Milestone 2, in as much detail as possible, as part of the first year progress report; and similarly to specify the deliverables for Milestone 3 in the second year progress report.

II-3 Reports and Reviews

II-3.1 Reports

As stipulated in Article 6 (“Reports”) of Annex II, the following reports will be submitted to the Commission for approval:

- a periodic management report as defined in Article 6 sub 1 (a), at every intermediate review point (i.e., every six months),

- a periodic progress report as defined under Article 6 sub 1 (b), at every major review point (i.e., every twelve months).

- a final report as defined in Article 6 sub 1 (c), within two months after the end of the Project.

The periodic management report due at every major review point will be combined with the periodic progress report at the major review point into one document. A “separate report” as defined in Article 6 sub 1 (d) will be generated only if the results of the Project warrant it. The periodic and final reports are public. “Edited” versions of the periodic and final reports as defined in Article 6 sub 1 (e) will be supplied upon request of the Commission. The format of the reports will be that prescribed by the Commission.

II-3.2 Reviews

Reviews as intended in Article 5 of Annex II will be scheduled at the major review points, i.e., at the milestones of the Project, and otherwise when so requested by the Commission under the rules of this Article. A review will be coupled to the business meeting scheduled at each milestone.

At each of the first two reviews, the reviewers will be required to judge whether progress towards the project objectives is at an acceptable rate, and in accordance with the approaches given in the Workplan; and at the last review they will be asked to judge whether the project has been successful (against the objectives given in Section I-3, subject to the Risk Assessment in II-1).

II-4 Information Dissemination

II-4.1 Workshops, travel and personnel exchanges

We will hold annual business meetings to monitor the overall progress of the project and to assimilate relevant work being done outside the project. These meetings will be timed to coincide with the project review points at months 12, 24 and 36.

In addition, we will hold a regular series of small-scale workshops. These are intended to act as focuses for collaboration on specific topics or themes within the Workplan and will involve only relevant personnel from the project sites. The first two workshops will be on “Evaluation Logic” and “Games, Processes and Logic”; topics for subsequent workshops will be chosen at the business meetings. We also plan to hold major workshops with invited external participants at Milestones 1 and 3 of the project. An outstandingly successful meeting of this type was held at the end of CLICS I.

Funds have also been requested for inter-site travel to facilitate collaboration between partners, and to cover expenses involved in presenting papers at international conferences on work carried out within the project. Members of the consortium have presented papers at the following conferences in the recent past: EATCS Colloquium on Automata Languages and Programming; Workshop on the Mathematical Foundation of Programming Lanuage Semantics; IEEE Symposium on Logic in Computer Science; ACM Principles of Programming Languages; ACM LISP and Functional Programming; Biennial Conference on Category Theory and Computer Science; Computer Science Logic; European Summer Meetings of the ASL.

II-4.2 Training activities

Members of the consortium have a substantial involvement in advanced training. We see this as an important aspect of our activities, since categorical logic and the other technical tools we employ are not yet widely understood in the Computer Science community, although they are becoming more so—in part through our own efforts!

Apart from the considerable number of Research students and Research Assistants who have been involved in CLICS, and received advanced training through this involvement, members of the consortium have been engaged in: editing and writing chapters of the Handbook of Logic in Computer Science, being published by Oxford University Press; organizing and lecturing in summer schools in Britain, Belgium, France, Italy and the Netherlands; giving invited tutorial lectures at a number of leading international conferences in the field; and writing a number of monographs and advanced textbooks [Vic89, Gir89], which often present recent research material in accessible form for the first time. We will continue all these activities in CLICS II.

Finally, in recognition of the importance of training, perhaps particularly for a project of the foundational character of CLICS, we will mount a summer school in the CLICS area during the period of the CLICS II programme. We believe, on the basis of past experience, that such a school would attract many able students from across the Community who are eager to acquire the techniques and insights of categorical logic and the other theoretical tools we deploy, but who do not have expertise in these subjects available to them locally. We also intend to produce a book based on the lecturing material developed for this summer school, which would provide authoritative surveys of the main research areas covered by CLICS II.

II-5 Project Management

The CLICS I consortium comprised the following sites:

Imperial (co-ordinating site) Aarhus Cambridge CAIMENS Paris INRIA Parma GMD Bonn

A number of developments have necessitated changes to the consortium. Coquand has moved from INRIA to Chalmers University, Göteborg, Sweden; Moggi, who was employed as a Research Assistant for 9 months on CLICS I, and has continued to maintain close contacts with the project, has moved to Genova; and Rosolini is likely to move there from Parma. Poigné has now taken on heavy administrative duties at GMD, which preclude major involvement by him in CLICS. Thus we now have the following revised list of Principal sites for CLICS II:

Principal Site  Principal Investigators
Imperial (co-ordinating site) Abramsky
Aarhus  Winskel
Cambridge  Hyland, Pitts
Chalmers (EFTA partner) Coquand, Dybjer
CAIMENS Paris  Curien, Lafont
Genova  Moggi, Rosolini

However, we still want to maintain contact with Poigné at GMD, and there are a number of other sites containing researchers with whom we already have close links, and who would significantly enhance the consortium: Darmstadt (Jung, Keimel), Manchester (Rydeheard, Simmons, Aczel), Sussex (Robinson, Stoughton). Including these sites on the same level as the principal sites would have made the project too large and unwieldy from the management point of view; also, several of these sites are represented by just one or two researchers rather than a sizeable ongoing research group as with most of the Principal sites. We therefore have a category of “Associate” sites, comprising:

Associate Site Principal Investigators
Darmstadt  Jung, Keimel
GMD  Poigné
Manchester  Rydeheard, Simmons
Sussex  Robinson, Stoughton

The management structure we propose is a Steering Committee comprising one Principal Investigator nominated by each Principal site. This Committee will meet at the annual business meetings to review progress and modify the workplan if necessary.

The Associate sites will each be “twinned” with a Principal site, and management issues relating to an Associate site will be handled between it and the corresponding Principal site, which reports back to the Steering Committee. The proposed twinning is:

Darmstadt Paris CAIMENS
GMD  Imperial
Manchester Cambridge
Sussex  Genova

In the case of any conflicts arising within the project, they will be resolved by an extraordinary meeting of all Principal Investigators within the project (from Associate as well as Principal sites), who will, if necessary, vote on the issue. Any decision reached in this way will be binding on all the partners.

II-5.1 Curriculum Vitae of Principal Investigators

Brief CV of S. Abramsky

Nationality: British

Academic qualifications. MA (Cambridge University), PhD (London University).

Professional employment and activities. Samson Abramsky is Professor of Computing Science and Head of the Theory and Formal Methods Section, Department of Computing, Imperial College of Science, Technology and Medicine, University of London. He was previously Reader and Lecturer at Imperial College, and Lecturer at Queen Mary College. He is Chairman of the UK SERC Special Initiative in Logic for IT. His other activities include membership of the Editorial Boards of a number of journals and monograph series, including the Journal of Theoretical Computer Science, the Journal of Mathematical Structures in Computer Science, the Cambridge Tracts in Theoretical Computer Science, and the North Holland Studies in Logic and Foundations of Mathematics. He has been an invited speaker at a number of international conferences and workshops. His research interests include: semantics and logics of programming languages, concurrency, Linear logic, lambda calculus, applications of logic, topology and category theory in Computer Science, semantics-based program analysis.

Selected publications.

S. Abramsky, “Reasoning about concurrent systems: a functional approach”, in Distributed Systems, F. Chambers, D. Duce and G. Jones, eds. (Academic Press) 1984, 307–319.

S. Abramsky, “The Lazy λ-Calculus”, in Research Topics in Functional Programming, D. Turner, ed., pages 65-117. Addison Wesley, 1990.

G. Burn, C. Hankin and S. Abramsky, “Strictness Analysis for Higher Order Functions”, Science of Computer Programming 7, (1986), 249–278.

S. Abramsky, “Observation Equivalence as a Testing Equivalence”, J. Theoretical Computer Science 53, (1987), 225–241.

S. Abramsky, “Domain theory in logical form”, Annals of Pure and Applied Logic 51 (1991), pages 1–77.

S. Abramsky, “Abstract Interpretation, Logical Relations and Kan Extensions”, J. Logic and Computation, 1(1), 1990, pages 5–40.

S. Abramsky and C.-H. L. Ong, “Full Abstraction in the Lazy λ-calculus”, J. Information and Computation, (1989). Accepted for publication. 122 pages.

S. Abramsky, “Computational Interpretations of Linear Logic”, J. Theoretical Computer Science (1990). Accepted for publication.

S. Abramsky, “Domain Theory in Logical Form”, in Symposium on Logic in Computer Science, (Computer Society Press of the IEEE) 1987, 47–53.

S. Abramsky, “A Generalized Kahn Principle for Abstract Asynchronous Networks”, in Symposium on Mathematical Foundations of Programming Language Semantics, M. Mislove, ed. (Springer-Verlag) 1990, pages 1–21.

Brief CV of P. Aczel

Nationality: British

Academic qualifications. Oxford University: 1st class B.A. Mathematics (1963), Ph.D. Mathematics (1966).

Professional employment and activities. Started at Manchester University in October 1968, permanent position 1970, Senior lecturer 1975, Reader 1981, Professor 1990. Presently Professor of Mathematical Logic and Computing Science, a joint position in the Mathematics and Computer Science departments at Manchester University. Visiting Positions: 1966–67 at Rutgers, 1967-68 at Wisconsin, Feb-June 1972 at Oslo, Oct–Dec 1975 at Caltech, Jan-June 1976 at Utrecht, Nov 84–March 85 at Stanford. Research Fellowships: 1968–69 PostDoc at Manchester, April–June 1985 Senior Research Fellowship at Edinburgh, Jan–Aug 1986 and Jan–Aug 1987 ICL Senior visiting Fellowship at Manchester CS department, 1990-91 SERC Senior Research Fellowship. Member of the Council of the Association of Symbolic Logic and on the editorial board of the Journal of Symbolic Logic. Also on the editorial board of the book series Cambridge Tracts in Theoretical Computer Science and advisory editor of the journal Annals in Pure and Applied Logic and the book series Bibliopolis Studies in Proof Theory. Author of 29 research papers and a book Non-Well-Founded Sets.

Selected publications.

P. Aczel, Term Declaration Logic and Generalised Composita, in the proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pp22-30, July, P. Aczel and R. Lunnon, Universes and Parameters, to appear in Situation Theory and its Applications, Vol. 2, the proceedings of the Second Conference on Situation Theory and its Applications, edited by Jon Barwise and Gordon Plotkin, CSLI Lecture Notes, Stanford University.

Peter Aczel, David Carlisle and Nax Mendler, Two frameworks of theories and their implementation in Isabelle, in Logical Frameworks, the proceedings of the first workshop on Logical Frameworks, edited by Gerard Huet and Gordon Plotkin, Cambridge University Press, 1991.

Brief CV of Th. Coquand

Nationality: French

Professional employment and activities. Researcher, INRIA, March 85-June 89, in the Formel project (headed by G.Huet). Directeur de Recheche, INRIA, since July 89 (Responsable permanent, Formel project). Research Associate, Department of Computer Science, Carnegie-Mellon University, September 85–June 86. Research Associate, Cambridge University Computer Laboratory, September 86–January 88. Research Associate, Department of Computer Science, University of Pennsylvania, September–October 88. Guest Professor at Chalmers University, Göteborg, since January 90.

Selected publications.

Th. Coquand, Sur l’analogie entre les propositions et les types. Springer-Verlag LNCS 242 1986, english translation in Proccedings of the Year of Programming Institute Austin, 1987.

Th. Coquand, An analysis of Girard’s paradox. Logic in Computer Science, Boston, 1986.

Th. Coquand, Metamathematical investigations of a calculus of constructions. Logic and Computer Science, P. Odifreddi editor, Academic Press 1990.

Th. Coquand, Categories of Embeddings. Proceedings of the 3rd LICS conference, 1988. Theoretical Computer Science, 1989.

Th. Coquand and Th. Ehrhard, An equational presentation of Higher-Order Logic. In Category Theory and Computer Science, Lecture Notes in Computer Science, 283.

Th. Coquand and G. Huet, Constructions: A higher-order proof system of mechanizing mathematics. In EUROCAL85, Lecture Notes in Computer Science, Vol. 203, 1985.

Th. Coquand and G. Huet, The Calculus of Constructions. Information and Computation, 1988.

Th. Coquand, C. Gunter and G. Winskell, DI-Domains as a model of Polymorphism. Proceedings of MFPLS, New Orleans 1987.

Th. Coquand and Ch. Paulin-Mohrin, About inductively defined types. LNCS 417, Colog-88, P. Martin-Löf and G. Mints editors.

Th. Coquand and G. Stolzenberg, About Wiener Theorem and certain of its applications. Bulletin of the American Mathematical Society, Volume 24, January 1991

Brief CV of P.-L. Curien

Nationality: French

Academic qualifications. Born at Paris 9/8/53. He received the third prize at the ”Concours Général de Mathématiques” (1970) and the third prize at the Olympiads of Mathematics, Budapest (1970). He entered the Ecole Normale Supérieure in 1972. He obtained the Agrégation de Mathématiques in 1975, his Thèse de Troisième Cycle in 1979 and his Thèse d’Etat in 1983, both at the University Paris VII, under the supervision of Maurice Nivat. He received the IBM France Award 1990 in Computer Science.

Professional employment and activities. Since 1981 he is employed as a researcher by the CNRS. He is Directeur de Recherche since 1988, and his present laboratory is the Laboratoire d’Informatique de l’Ecole Normale Supérieure. He is an editor of Theoretical Computer Science, Mathematical Structures in Computer Science and Journal of Functional Programming. He participated in various program committees, including LFP, ICALP and LICS. He coedited two LNCS volumes (242,530). He supervises several theses and teaches graduates courses at Paris VII. His research interests cover domain theory (particularly in its interface to operational semantics), and evaluation techniques for various computational paradigms.

Selected publications.

P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman (1986).

M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Le’vy, Explicit substitutions, to appear in Journal of Functional Programming (short version in Proc. POPL 90).

P.-L. Curien, G. Ghelli, Coherence of Subsumption: applications to type-checking and minimum property in F_{≤}, to appear in Mathematical Structures in Computer Science (short version in Proc. CAAP 90, LNCS).

Brief CV of P. Dybjer

Nationality: Swedish

Academic qualifications. Civilingenjörsexamen (Master of Science), technical physics, Lund University 1977. Master of Science, Computer Science, UCLA 1980. Teknisk doktorsexamen (Ph.D.), Computer Science, Chalmers University 1983. Docent in Computer Science, Chalmers University 1986.

Professional employment and activities. Research lecturer in Computer Science. Fields of interests: programming logic, especially intuitionistic type theory and logic of concurrent systems; program optimization, especially strictness analysis. Program committee member for Category Theory and Computer Science 1987, 1989, 1991; olloquium on Trees and Algebras in Programming (CAAP) 1991; and Logic in Computer Science 1991. Invited lectures at the Workshop on Category Theory and Computer Programming, Guildford 1985; Workshop on General Logic, Edinburgh 1987; Logic for IT Summer School on Category Theory and Constructive Logic, Isle of Thorns 1988; IFIP TC2 Working Conference on Programming Concepts and Methods, Tiberias 1990; Conference on Symbolic Logic and Computer Science, Kyoto 1990; and LMS-Symposium on Applications of Category Theory in Computer Science 1991.

Selected publications.

An inversion principle for Martin-Löf’s type theory, in Proceedings of the Workshop on Programming Logic, PMG-Report 54, Department of Computer Sciences, Chalmers University, 1989

A functional programming approach to the specification and verification of concurrent systems, Formal Aspects of Computing (1989) 1: 303-319

Comparing integrated and external logics of functional programs, Science of Computer Programming 14 (1990) 59-79.

Inverse image analysis generalises strictness analysis, Information and Computation (1991) Vol 90, No 2, 194-216.

Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Logical Frameworks, eds. G. Huet and G. D. Plotkin, 1991.

Brief CV of J. M. E. Hyland

Nationality: British

Academic qualifications. BA in Mathematics, 1970, Diploma in Mathematics, University of Cambridge, 1971, and D.Phil in Mathematical logic, Oxford University, 1976.

Professional employment and activities. Dr.Hyland is a University Lecturer in the Department of Pure Mathematics and Mathematical Statistics, Cambridge University. From 1976-81 he was a University Assistant Lecturer there. His research work includes: The syntax and semantics of the lambda calculus, general recursion theory, sheaf models for intuitionistic theories, general categorical logic and topos theory, the effective topos (of which he is the inventor) and other realizability toposes and constructive mathematics as developed in such frameworks, topos theoretic models for polymorphism and dialectica categories and non-standard categorical logic (in particular models for variants of linear logic). Dr.Hyland has been an invited speaker to over 15 international conferences and workshops in Europe and the United States.

Selected publications.

J. M. E. Hyland, The Effective Topos. In The L. E. J. Brouwer Centenary Symposium (North-Holland, Amsterdam, 1982), pp 165–216.

J. M. E. Hyland, A small complete category, Annals of Pure and Applied Logic 40(1988) 135-165.

J. M. E. Hyland and A. M. Pitts, The theory of constructions: categorical semantics and topos-theoretic models, Contemporary Math. 92(1989) 137–199.

J. M. E. Hyland, E. P. Robinson and G. Rosolini, The discrete objects in the efective topos, Proc. Lond. Math. Soc.(3) 60(1990) 1-36.

J.M.E. Hyland, E. P. Robinson and G. Rosolini, Algebraic types in PER models, in the Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, New Orleans, 1989 (M. Main et al. Eds.) Lecture Notes in Computer Science 442, Springer, Berlin (1990) 333-350.

J. M. E. Hyland, First steps in synthetic domain theory. In A. Carboni, M. C. Pedicchio, and G. Rosolini (eds), Category Theory ’90 (Springer-Verlag, Berlin, 1991), to appear.

Brief CV of A. Jung

Nationality: German

Academic qualifications. Diploma in Mathematics (Minor in Computer Science), Technische Hochschule Darmstadt, January 1984. Doctorate in Mathematics, Technische Hochschule Darmstadt, July 1988.

Professional employment and activities. Researcher at the Gesellschaft für Mathematik und Datenverarbeitung, Darmstadt, January to August 1984. Teaching Assistant, Carnegie Mellon University, Pittsburgh, USA, September 1984 to May 1985. Assistant in the Department of Mathematics, Technische Hochschule Darmstadt, September 1985 to present. Guest researcher in the Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA, February 1989 to April 1989. Research Assistant in the Department of Computing, Imperial College, London, October 1989 to June 1990. Research interests: Domain Theory and Semantics of Programming Languages, Ordered sets and lattices, Topology, Universal Algebra, Cryptology, Databases.

Selected publications.

A. Jung, E. Nelson, J. Adámek, J. Reiterman, A. Tarlecki, Comparison of Subset Systems, Commentationes Mathematicae Universitatis Carolinae, 29(1988) 169–177.

A. Jung, Cartesian Closed Categories of Domains. CWI Tract 66, 1989, 110pp.

A. Jung, Cartesian Closed Cartegories of Algebraic CPO’s, Theoretical Computer Science 70(1990) 233–250.

A. Jung and C .Gunter, Coherence and Consistency in Domains, Journal of Pure and Applied Algebra, 63(1990) 49–66.

A. Jung, The Dependent Product Construction in Various Categories of Domains, Theoretical Computer Science 79(1991) 359–364.

P. Buneman, A. Jung and A. Ohori, Using Powerdomains to Generalize Relational Databases, Theoretical Computer Science 86(1991), to appear.

A. Jung, New Results on Hierarchies of Domains. In: Mathematical Foundations of Programming Language Semantics, edited by M. Main, A. Melton, M. Mislove and D. Schmidt, Lecture Notes in Computer Science, vol. 298, Springer-Verlag, 1988, pp 303-310.

A. Jung and C .Gunter, Coherence and consistency in domains (extended outline.) In: Logic in Computer Science, IEEE Computer Society Press, 1988, pp 309–319.

A. Jung, The Classification of Continuous Domains (extended outline.) In: Logic in Computer Science, IEEE Computer Society Press, 1990, pp 35–40.

Brief CV of K. Keimel

Nationality: German

Academic qualifications. ‘Philosophicum’ at Tübingen University, 1961. ‘Staatsexamen’ (Master’s Degree) in Mathematics and Physics, Tübingen University, 1964. Doctoral Student in Paris, France, 1965–66. ‘Doctor rerum naturalium’ (Ph.D.), Tübingen University, 1967. ‘Doctorat d’Etat ès Sc. Math.’ at Faculté des Sciences, Paris, France, 1970.

Professional employment and activities. Research Assistant at Tulane University, New Orleans, USA, 1964–65. Assistant Associé, Faculté des Sciences, Paris, France, 1966–68. Maĩtre de Conférences Associé, Tours University, France, 1968–71. Professor of Mathematics at Darmstadt University, Germany, 1971–present. Communicating editor for Semigroup Forum (since 1976) and Order (since 1984). Co-editor of Universal Algebra and its Links with Logic, Combinatorics, and Computer Science, Heldermann Verlag, Berlin, 1983.

Selected publications.

A General Character Theory for Partially Ordered Sets and Lattices, Memoirs Amer. Math. Soc. \underline{122}(1972), 121pp. (joint with K.H.Hofmann.)

A Compendium of Continuous Lattices, 1980, Springer Verlag, xx+371pp. (joint with G.Gierz, K.H.Hofmann, J.D.Lawson, M.Mislove, and D.S.Scott.)

A lemma on primes and its appearance in algebra and analysis, Houston J. Math., \underline{3}(1977), pp 207–224, (joint with G.Gierz.)

Topologische Darstellung von Verbänden, Math. Zeitschrift, \underline{150}(1976), pp 83–99, (joint with G.Gierz.)

Verfeinerungs- und Kürzungssätze fr̈ direkte Produkte geordneter topologischer Räume und Funktionen(halb)verbände, in:\underline{871}(1981), Springer Verlag, pp 20–44, (joint with H.Bauer and R.Köhler.)

Continuous ideal completions and compactifications, ibid., pp 97–124, (joint with Gierz.)

• Halbstetige Funktionen und stetige Verbände, in: Continuous Lattices and Related Topics, Mathematik Arbeitspapiere, \underline{27}(1982), Universität Bremen, pp 59–67, (joint with G.Gierz.)

Brief CV of Y. Lafont

Nationality: French

Academic qualifications. Born in 1961 at Meaux, France. Entered Ecole Normale Supérieure in 1981, obtained the Agrégation de Mathématiques in 1983, an his Thèse de Doctorat in 1988 under the supervision of J.-Y. Girard.

Professional employment and activities. Since 1988 he is employed as a researcher by the CNRS. He is Senior Chargé de Recherche since 1991. Y. Lafont lectured in several International Summer Schools on Linear Logic and its applications to Computer Science. His present interest is in the design of Interaction Nets (inspired by linear logic) as a programming paradigm, and in the exploration of a geometric understanding of rewriting.

Selected publications.

J.Y. Girard, Y. Lafont & P. Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science (Cambridge University Press, 1989).

Y. Lafont, The Linear Abstract Machine, TCS 59 (1988) 157-180.

Y. Lafont & A. Prouté, Church-Rosser Property and Homology of Monoids, à paraĩtre dans MSCS (Cambridge University Press).

Y. Lafont, Interaction Nets, Proceedings of ACM Symposium on Principles of Programming Languages (1990).

Brief CV of E. Moggi

Nationality: Italian

Academic qualifications. Laurea in Computer Science, Università di Pisa 1983, Diploma, Scuola Normale Superiore di Pisa 1983, and Ph.D. in Computer Science, University of Edinburgh 1988.

Professional employment and activities. Eugenio Moggi is Professor of Computer Science Università di Genova (since November 1990). His previous employments include: Research Associate LFCS University of Edinburgh (1987-89), Ricercatore Dipartimento di Informatica Università di Pisa (1988-89), Visiting Professor CS Department Stanford University (Spring 1989), Lecturer in Computer Science University of Edinburgh (1989-91), Research Associate Computer Laboratory University of Cambridge (1990), Visitor Ecole Normal Supérieure Paris (May 1990). Eugenio Moggi’s research interests include: semantics of programming languages and formal systems for reasoning about programs. His main original contributions have been: categorical semantics of polymorphic types, the study of formal systems for partial functions, notions of computations as monad and computational lambda calculus, categorical semantics of program modules. Eugenio Moggi has contributed to the following projects: UK SERC “Computer Assisted Reasoning”, Stimulation Project “Typed Lambda-Calculus”, ESPRIT BRA “Categorical Logic in Computer Science” and UK SERC “Logical and Semantical Frameworks”. He has been invited speaker to CTCS87, CT91 and CTCS91.

Selected publications.

The partial Lambda-Calculus, Ph.D. Thesis in Computer Science, Univ. of Edinburgh, Nov 1988.

Partial Morphisms in Categories of Effective Objects, Information and Computation, vol. 73, Nos. 2/3, Feb 1988.

Computational lambda-calculus and monads, in the proceedings of the Fourth IEEE Conference on Logic in Computer Science, Asilomar CA, Jun 1989.

Higher Order Modules and the Phase Distinction (with R. Harper, J. Mitchell), in the proceedings of the International Conference on Principles of Programming Languages, San Francisco, CA USA, Jan 1990.

Empty Types in Polymorphic Lambda-calculus (with A. Meyer, J. Mitchell, R. Statman), in Logical Foundations of Functional Programming, Ed. G. Huet, University of Texas at Austin Year of Programming Series, 1990.

A category-theoretic characterisation of functional completeness (with G. Longo), Theoretical Computer Science, vol. 70, 1990.

Kripke-style Models for the Typed Lambda-calculus (with J. Mitchell), in Annals of Pure and Applied Logic, vol. 51, 1991.

Notions of computation and monads, in Information and Computation, vol. 93, No. 1, July 1991.

A category-theoretic account of program modules, in Mathematical Structures in Computer Science, vol. 1, 1991.

Relating Models of Impredicative Type Theories (with B. Jacobs, T. Streicher), in the proceedings of the conference on Category Theory and Computer Science, Paris, Sep 1991.

Constructive Natural Deduction and its Modest Interpretation (with G. Longo), to appear in Mathematical Structures in Computer Science.

Brief CV of A. M. Pitts

Nationality: British

Academic qualifications. BA(1977), MA(1981) and PhD(1982) in Mathematics from University of Cambridge.

Professional employment and activities. Dr. Pitts has been a University Lecturer in the University of Cambridge Computer Laboratory since January 1989. For three years prior to that he was a Royal Society University Research Fellow in the Mathematics Division at the University of Sussex—having previously held postdoctoral and visiting positions in Cambridge, McGill and Buffalo Universities. His expertise lies in the areas of category theory and mathematical logic; his research interests concern the application of these subjects to computer science in general and particularly to the semantics of programming languages and type theories, and to formal logics for reasoning about program properties. He served on the programme committee of the IEEE Symposium on Logic in Computer Science in 1990 and 1991 and is currently a member of its organizing committee. He served on the programme committee of the Category Theory in Computer Science Conferences in 1989 and 1991. He was principal organizer of the LMS Symposium on Applications of Categories in Computer Science, Durham 1991. He is an Associate Editor of the journal Mathematical Structures in Computer Science and on the Editorial Advisory Board of the London Mathematical Society. He participates as the Cambridge responsible scientist on the ESPRIT BR Action CLICS and is principal investigator for the UK-SERC research project “Verifying ML Programs using Evaluation Logic”.

Selected publications.

Applications of sup-lattice enriched category theory to sheaf theory, Proc. London Math. Soc. (3) 57(1988) 433–480.

Conceptual completeness for first order intuitionistic logic: an application of categorical logic, Annals Pure applied Logic 41(1989) 33–81.

A note on Russell’s paradox in locally cartesian closed categories, Studia Logica 48(1989) 377–387. (With P. Taylor.)

New Foundations for Fixpoint Computations, Proc. 5th Annual Symposium on Logic in Computer Science, Philadelphia (IEEE Computer Society Press, Washington, 1990), pp 489–497. (With R. L. Crole.) [Full version accepted for publication in Information and Computation.]

The theory of constructions: categorical semantics and topos-theoretic models, Contemporary Math. 92(1989) 137–199. (With J. M. E. Hyland.)

Polymorphism is set theoretic, constructively. In Lecture Notes in Computer Science No. 283 (Springer-Verlag, Berlin, 1987), pp 12–39.

Non-trivial power types can’t be subtypes of polymorphic types. In: Proc. 4th Annual Symp. Logic in Computer Science (IEEE Computer Soc. Press, Washington, 1989), pp 6–13.

Evaluation Logic. In: IVth Banff Higher Order Workshop, Workshops in Computer Science (Springer-Verlag, Berlin, 1991), to appear.

On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic, Jour. Symbolic Logic, to appear.

Brief CV of A. Poigné

Nationality: German

Academic qualifications. Diploma in Electrical Engineering, Technical University of Darmstadt 1972, and Ph.D. in Computer Science, University of Dortmund 1979

Professional employment and activities. Currently Axel Poigné is acting head of the institute of Systems Engineering at GMD. From beginning of 91 he will head a section on specification of complex systems within the institute of System Design Techniques. Previously he was research and teaching assistent at the University of Dortmund and lecturer at Imperial College, both in the Departments of Computer Science. His professional activities include: coordinator of a German research project on correct software involving 14 leading German universities and industrial laboratories; member of the organisation and program committees of the International conferences on Category Theory and Computer Science 85, 87, 89, 91; member of the program committee of CAAP 91, 92. Axel Poigné’s research interests include: semantics of programming languages, applications of category theory in computer science, categorical models of type theory, formal specification methods (particularly axiomatic (algebraic) specification and specification of distributed systems), high-level Petri models Axel Poigné has collaborated at the national and international level: in ESPRIT BRAs CLICS (partner), DEMON (researcher), COMPASS (scientific correspondant). He is currently involved as project coordinator in the German national project KORSO on correct software construction, and as project leader in a subproject on specification of reliable reactive systems.

Selected publications.

Basic Category Theory, Chapter in : Abramsky, Gabbay, Maibaum (eds.) Handbook of Logic in Computer Science, Oxford University Press, to appear.

Typed Horn Logic,in B. Rovan (ed.) Mathematical Foundations of Computer Science ’90, LNCS 452, Springer-Verlag, 1990

A Note on Inconsistencies caused by Fixpoints in a Cartesian Closed Category, in : Theoretical Computer Science 73, 1990.

Brief CV of E. P. Robinson

Nationality: British

Academic qualifications. MA (Cambridge), PhD (Cambridge).

Professional employment and activities. Research Associate, Department of Computer Science, University of Edinburgh (under Prof. R.M. Burstall), January–December 1984. Research Fellow, Peterhouse, Cambridge, January 1985–August 1987. Assistant Professor, Department of Computing and Information Science, Queen’s University, Kingston, Ontario, September 1987–December 1989. Lecturer in Computer Science, School of Cognitive and Computing Sciences, University of Sussex, Brighton, England, January 1990–present.

Selected publications.

A characterization of pie limits (with A.J. Power), Mathematical Proceedings of the Cambridge Philosophical Society, 110 (1991) 33-47.

Colimit completions and the effective topos, (with G. Rosolini) Journal of Symbolic Logic, 55(2) (1990) 678-699.

Polymorphism, set theory, and call-by-value (with G. Rosolini), in the Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, 1990, 12-18.

The discrete objects in the effective topos, (with J.M.E. Hyland and G. Rosolini), Proceedings of the London Mathematical Society (3) 60 (1990) 1-36.

How complete is PER?, in the Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, Computer Society Press, 1989, 106-111.

Algebraic types in PER models, (with J.M.E. Hyland and G. Rosolini), in the Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, New Orleans, 1989 (M. Main et al. Eds.) Lecture Notes in Computer Science 442, Springer, Berlin (1990) 333-350.

A note on inequivalence of realizability toposes, (with P.T. Johnstone), Mathematical Proceedings of the Cambridge Philosophical Society, 105 (1989) 1-3.

Categories of partial maps, (with G. Rosolini), Information and Computation 79 (1988) 95-130.

Logical aspects of denotational semantics, in Category Theory and Computer Science,” Proceedings of the Edinburgh Conference, September 1987, (Eds. D.H. Pitt, A. Poigné & D.E. Rydeheard), Lecture Notes in Computer Science 283, Springer Verlag (1987), 238-253.

Brief CV of G. Rosolini

Nationality: Italian

Academic qualifications. Laurea con lode in Matematica, Università di Parma, Italy 1978, D.Phil in Mathematics, University of Oxford, UK, 1986.

Professional employment and activities. Dr. Rosolini has held research fellowships at: Consiglio Nazionale delle Ricerche, Italy (1976-81), C.N.R.-N.A.T.O (1984-85), Carnegie-Mellon University, Pittsburgh PA, USA (1985-86), Ricercatore universitario, Università di Parma (1981-84), Research associate, University of Cambridge, UK (1986-88), Ricercatore universitario, Università di Parma, March ’88- present. He was one of the organizers of the International Summer Conference in Category Theory ’90. He is a member of the Association for Symbolic Logic and the Peripatetic Seminar on Sheaves and Logic. His research interests include topos theory with special attention to the realizability toposes, small complete categories in locally cartesian closed categories, and more generally in strong intuitionistic type theories, the synthetic approach to domain theory.

Selected publications.

Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986. [Available as Technical Report CMU-CS-86-123, Carnegie Mellon University.]

Categories and effective computations. In D.H. Pitt, A.Poigné, and D.E. Rydeheard, editors, Category theory and Computer Science, volume 283 of Lectures Notes in Computer Science, pages 1–11, Edinburgh, 1987. Springer-Verlag.

Representation theorems for special p-categories. In F.Borceux, editor, Categorical Algebra and its Applications, volume 1348 of Lectures Notes in Mathematics, pages 307–315, Louvain-la-Neuve, 1988. Springer-Verlag.

E.P. Robinson and G.Rosolini. Categories of partial maps. Inform. and Comput., 79:95–130, 1988.

P.J. Freyd, P.Mulry, G.Rosolini, and D.S. Scott. Extensional PERs. In Proc. 5th Symposium in Logic in Computer Science, pages 346–354, Philadelphia, 1990. I.E.E.E. Computer Society.

J.M.E.Hyland, E.P.Robinson, and G.Rosolini. Algebraic types in PER models. In M.Main, A.Melton, M.Mislove, and D.Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 442 of Lectures Notes in Computer Science, pages 333–350. Springer-Verlag, 1990.

J.M.E. Hyland, E.P. Robinson, and G.Rosolini. The discrete objects in the effective topos, Proc. London Math. Soc., 60:1–60, 1990.

E.P. Robinson and G.Rosolini, Colimit completions and the effective topos, Journ. Symb. Logic, 55:678–699, 1990.

E.P. Robinson and G.Rosolini. Polymorphism, set theory and call by value. In Proc. 5th Symposium in Logic in Computer Science, pages 12–18, Philadelphia, 1990. I.E.E.E. Computer Society.

About modest sets, Int. J. Found. Comp. Sci., 1:341–353, 1990.

An EXPER model for Quest. In Mathematical Foundations of Programming Semantics, Pittsburgh, 1991. To appear.

Brief CV of D. E. Rydeheard

Nationality: British

Professional employment and activities. Research Fellow in University of Edinburgh, Dept. Computer Science, 1980-1983. Lecturer in University of Manchester, Dept. Computer Science, 1983–. Member of the Committee of the British Colloquium for Theoretical Computer Science. Member of the Organising Committee of the Conference on Category Theory and Computer Science (CTCS). Principal investigator for the following research projects: “The Mathematics of Program Design: The Role of Category Theory” (SERC £45K, 1985–88); “Programming Environments and Categorical Logic” (SERC £3K, 1989– 91); “Programming Environments and Categorical Logic (II)” (SERC £82K, 1990-93).

Selected publications.

Computational Category Theory. D.E. Rydeheard and R.M. Burstall (1988) Prentice Hall International Series in Computer Science (C.A.R. Hoare ed.), Hemmel Hempstead.

A Categorical Unification Algorithm. D.E. Rydeheard and R.M. Burstall. Proc. Summer Workshop on Category Theory and Computer Science, Surrey, 1985. Lecture Notes in Computer Science 240, pp 493–505, Springer-Verlag.

Foundations of Equational Deduction: A Categorical Treatment of Equational Proofs and Unification Algorithms. D.E. Rydeheard and J.G. Stell. Proc. Summer Workshop on Category Theory and Computer Science, Edinburgh, 1987. Lecture Notes in Computer Science 283. pp. 114–139. Springer-Verlag.

Towards a Categorical Semantics of Type Classes. B.P. Hilken and D.E. Rydeheard. Proc of Mathematical Foundations of Computer Science, Poland 1991. Springer Lecture Notes in Computer Science 520, pp 191–201.

Indexed Categories for Program Development. B.P. Hilken and D.E. Rydeheard. To appear in Cahiers de Topologie et Geométrie Differentielle.

Categorical ML – Category-Theoretic Modular Programming. E. Dennis-Jones and D.E. Rydeheard. To appear in Formal Aspects of Computing (The International Journal of Formal Methods).

Brief CV of H. Simmons

Nationality: British

Academic qualifications. B.Sc. (Mathematics) University of Bristol 1963, Ph.D. (Mathematics) University of Bristol 1966.

Professional employment and activities. University of Bristol, Assistant Lecturer in Mathematics 1965 - 1968. University of Aberdeen, Lecturer in Mathematics 1968 - 1977. University of Aberdeen, Senior Lecturer in Mathematics 1977 - 1990. Coordinator of the SERC funded initiative Logic for IT 1988–. Reader in Logic and Computing Science, Department of Computer Science, The University, Manchester, 1990–. Current research grants held: SERC GR/F/61974 “Logic Programming, Abstract Data Types, and Many-sorted Model Theory” (January 1990 to December 1991); SERC GR/H18449 “Executable modal logics through theorem proving” (November 1991 to October 1994).

Selected publications.

A framework for topology, in Logic Colloquium 77 (North Holland, 1978) 239-251.

Spaces with boolean assemblies, Colloquium Math. 43 (1980) 23-39.

A couple of triples, Topology and Appl. 13 (1982) 201-223.

An algebraic version of Cantor-Bendixson analysis, in Categorical aspects of topology and analysis, Springer Lecture Notes in Mathematics vol. 915 (1982) 310-323.

Near-discreteness of modules and spaces as measured by Gabriel and Cantor, J. Pure and Applied Alg. 56 (1989) 119-162.

Compact representations - The lattice theory of compact ringed spaces, J. Alg. 126 (1989) 493-531.

The realm of primitive recursion, Arch. math. 27 (1988) 177-188.

Separating the discrete from the continuous by iterating derivatives, Bull. Soc. Math. Belg. 41 (1989) 417-463.

Brief CV of A. Stoughton

Nationality: USA

Academic qualifications. University of California, Los Angeles, BS Mathematics/Computer Science, June 1979 and MS Computer Science, December 1981. University of Edinburgh, PhD Computer Science, January 1987.

Professional employment and activities. Computer Science Department, University of California, Los Angeles, Teaching Assistant, 1979–80. Computer Science Department, University of California, Los Angeles Programmer, 1980–81 and 1976–79. Information Sciences Institute, Los Angeles, Research Assistant, 1981–82. Department of Computer Sciences, Chalmers University of Technology, Göteborg, Visiting Research Fellow, January–July 1986. Computer Science and Artificial Intelligence Subject Group, University of Sussex, Research Fellow, September 1986– March 1988. Computer Science and Artificial Intelligence Subject Group, University of Sussex Lecturer in Computer Science, April 1988–. Allen Stoughton’s research interests are in programming language semantics, particularly the relationship between operational and denotational semantics and the problem of finding fully abstract semantics.

Selected publications.

Interdefinability of Parallel Operations in PCF, Theoretical Computer Science, to appear, 1991.

Equationally Fully Abstract Models of PCF. In Proceedings of the 5th International Conference on the Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, vol. 442, Springer-Verlag, 1990, pp. 271–283.

Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science, Pitman/Wiley, 1988, 123 pp. A revision with additions of the University of Edinburgh PhD thesis of the same name, Technical Report CST–40–86, Computer Science Department, University of Edinburgh, November 1986.

Substitution Revisited. Theoretical Computer Science, 59, 1988, pp. 317–325. Previously appeared as Technical Report 1/87, Computer Science Subject Group, University of Sussex, April 1987.

D. Parker, G. Popek, G. Rudisin, A. Stoughton, B. Walker, E. Walton, J. Chow, D. Edwards, S. Kiser and C. Kline. Detection of Mutual Inconsistency in Distributed Systems, Transactions on Software Engineering, SE–9, 3, May 1983, pp. 240–247.

V. Kini, D. Martin, and A. Stoughton. Tools for Testing Denotational Semantic Definitions of Programming Languages. Technical Report ISI/RR–83–112, Information Sciences Institute, May 1983, 77 pp.

V. Kini, D. Martin and A. Stoughton. Testing the INRIA Ada Formal Definition: The USC-ISI Formal Semantics Project. Proceedings of the ADATec Conference on Ada, October 1982, pp˙120–128.

Access Flow: A Protection Model which Integrates Access Control and Information Flow. In: Proceedings of the 1981 Symposium on Security and Privacy, April 1981, pp. 9–18.

G. Popek, M. Kampe, C. Kline, A. Stoughton, M. Urban and E. Walton. UCLA Secure Unix. In: Proceedings of the National Computer Conference, June 1979, pp. 355–364.

Brief CV of G. Winskel

Nationality: British

Academic qualifications. BA in Mathematics, University of Cambridge, 1975, M.Sc specialising in Mathematical Logic, University of Oxford, 1976, and a Ph.D in Computer Science from the University of Edinburgh, 1980.

Professional employment and activities. From July 1988, Glynn Winskel has been Professor of Computer Science at the University of Aarhus, Denmark. Previously he was Reader in Theoretical Computer Science, at the Computer Laboratory, and a fellow at King’s College, University of Cambridge. Before joining Cambridge as a University Lecturer he was a Research Scientist at Carnegie Mellon University (1982-84) and Royal Society Postdoctoral Fellow at Aarhus (1980-82). Prof.Winskel has been invited to lecture at several international summerschools and conferences in computer science. He has served on several programme committees of conferences and workshops, as a referee for many international journals and conferences and was one of the organisers of the joint UK-US Seminar on Concurrency (1984), the proceedings of which appear as volume 197 of the Springer Lecture Notes in Computer Science. He is on the Editorial Board of the journal “Mathematical Structures in Computer Science”and is currently a reviewer for EEC Basic Research Actions. He is interested in theoretical computer science and related mathematics generally, the semantics of programming languages and its mathematical foundations, logic of programs, models and proof systems for parallel computation, models and proof systems for the specification and verification of hardware, type theories, functional programming, and automated proof. These interests are reflected in the research projects he is involved in: DART (A project involving Danish universities and industry, aiming to encourage collaborative research with Industry), and the Esprit Basic Research Actions CLICS (Categorical logic in computer science) and CEDISYS (Compositional distributed systems).

Selected publications.

A complete proof system for SCCS with modal assertions, Fundamenta Informaticae 6, pp.401-420, 1986.

Petri nets, algebras, morphisms and compositionality, Information and Computation, vol.72, No.3 Mar.1987.

Coquand, T., Gunter, C., and Winskel, G., Domain theoretic models of polymorphism, Information and Computation Vol.81, No.2, May 1989.

On model checking the modal ν-calculus, ICALP ’89 special issue of TCS 1991.

Winskel, G. and Larsen, K., Using information systems to solve recursive domain equations. In Information and Computation, 1991.

A compositional proof system on a category of labelled stransition systems. In a special conference issue of Information and Computation,vol.87, August 1990.

Coquand, T., Gunter, C., and Winskel, G., dI-domains as a model of polymorphism. In the proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics, New Orleans, LA 1987.

Relating two models of hardware. In the proceedings of the conference “Category theory and computer science”, Edinburgh, September 1987, Springer Lecture Notes in C.S.

A category of labelled nets and compositional proof system. In the proceedings of the the conference “Logic in Computer Science”, Edinburgh July 1988.

A note on model checking the modal ν-calculus. In the proceedings of ICALP 1989, Springer Lecture Notes in C.S., vol.372.

Engberg, U., and Winskel, G., Petri nets as a model of linear logic. In the proceedings of CAAP ’90, Copenhagen 1990, Springer Lecture Notes in Computer Science vol.431, 1990.

On the compositional checking of validity. In the proc of CONCUR’90, Springer Lecture Notes, 1990.

Camilleri, J.A., and Winskel, G., CCS with priority choice. Proceedings of LICS, IEEE, 1991.

Andersen, H.R., and Winskel, G., Compositional checking of satisfaction. To appear in the proceedings of Computer Aided Verification, Springer Lecture Notes in Computer Science, 1991.

Chapter III Resources

47

6811 CLICS II 48

Form III.1

NO.  6811

III.1 RESOURCE BREAKDOWN

1.1.1 Proposal Title (max 240 characters)

Categorical Logic in Computer Science II

1.1.2 Acronym (max 20 characters) CLICS II 1.1.3 Type of Proposal P

1.2.1 1.2.2 1.2.3 1.2.4 1.2.5 1.2.6 1.2.7 1.2.8

No Organisation Name Coun-Role Assoc.

Costs CEC funding

Effort in

try to No in ECU in ECU Man Years^{1}

1 IMPERIAL COLLEGE UK C 200000 200000

6 (3)

2 AARHUS UNIVERSITY DK P 195000 195000

6 (2.25)

3 CAIMENS F P 180000 90000 6 (2.4)

4 UNIVERSITY OF CAMBRIDGE UK P 191000 191000

6 (2.5)

5 DISI-GENOVA I P 206000 103000

2.5 (2.5)

6 CHALMERS TH S P 242000 0

3 (0)

7 TH DARMSTADT G A 3 29000 29000

3 (0)

8 GMD G A 1 21000 21000 1 (0)

9 UNIVERSITY OF MANCHESTER UK A 4 40000 40000

3 (0)

10 UNIVERSITY OF SUSSEX UK A 5 31000 31000

1.7 (0)

1.3  1.3.1  1.3.2  1.3.3
Totals1335  900  38.2 (12.65)
1.3.4 Project Duration in months (max 60 months)  36

Remarks:

This part to be filled in by the Coordinating Partner and should always be submitted to the CEC in cases of major changes in partnership or project objectives.

1Effort in man years: The first number represents the actual effort envisioned per partner over the period of the action; the number in parentheses represents the man years for which CEC funding is requested.

TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: Imperial College

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  67.113  69.867  35.81  172.79
2. Travel and Subsistence  5  5  5  15
3. Durable Equipment  0  0  0  0
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  4.07  4.07  4.07  12.21
Total  76.183  78.937  44.880  200
(1)  (1)  (1)  (1)
Total Costs  200 KECU
Funding requested from CEC:  200 KECU
in % of Costs  100 %

National Currency for this Participant: Pounds sterling Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
0.714 0.714 0.714

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: AARHUS UNIVERSITY

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  46.5  115.5  18  180
2. Travel and Subsistence  5  5  5  15
3. Durable Equipment  0  0  0  0
4. Consumables  0  0  0  0
5. Computer Services  0  0  0  0
6. Other costs^{(3)}  0  0  0  0
Total  51.5  120.5  23  195
(1)  (1)  (1)  (1)
Total Costs  195 KECU
Funding requested from CEC:  195 KECU
in % of Costs  100 %

National Currency for this Participant: Danish kroner Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
7.9  7.9  7.9

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: CAIMENS

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  62.531  65.658  29.011  157.2
2. Travel and Subsistence  4  4  4  12
3. Durable Equipment  0  0  0  0
4. Consumables  0  0  0  0
5. Services  3.6  3.6  3.6  10.8
6. Other costs^{(3)}  0  0  0  0
Total  70.131  73.258  36.611  180
(1)  (1)  (1)  (1)
Total Costs  180 KECU
Funding requested from CEC:  90 KECU
in % of Costs  50 %

National Currency for this Participant: Franc Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
7  7  7

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: CAMBRIDGE

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  50  50  43  128
2. Travel and Subsistence  7  7  6  20
3. Durable Equipment  10  0  0  10
4. Consumables  1.5  1.5  1.5  4.5
5. Services  0  0  0  0
6. Other costs^{(3)}  4.5  4.5  4.5  13.5
Total  73  63  55  191
(1)  (1)  (1)  (1)
Total Costs  191 KECU
Funding requested from CEC:  191 KECU
in % of Costs  100 %

National Currency for this Participant: Pounds sterling Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
0.714 0.714 0.714

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: DISI-GENOVA

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  57  57  55  169
2. Travel and Subsistence  8  8  8  24
3. Durable Equipment  7  0  0  7
4. Consumables  0  0  0  0
5. Services  2  2  2  6
6. Other costs^{(3)}  0  0  0  0
Total  74  67  65  206
(1)  (1)  (1)  (1)
Total Costs  206 KECU
Funding requested from CEC:  103 KECU
in % of Costs  50 %

National Currency for this Participant: Lire Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
1541  1541  1541

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: CHALMERS TH

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  72  72  72  216
2. Travel and Subsistence  5  5  5  15
3. Durable Equipment  7  0  0  7
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  2  1  1  4
Total  86  78  78  242
(1)  (1)  (1)  (1)
Total Costs  242 KECU
Funding requested from CEC:  0 KECU
in % of Costs  0 %

National Currency for this Participant: Swedish kroner Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
7.42  7.42  7.42

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: TH DARMSTADT

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  0  0  0  0
2. Travel and Subsistence  5  6  6  17
3. Durable Equipment  10  0  0  10
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  0  1  1  2
Total  15  7  7  29
(1)  (1)  (1)  (1)
Total Costs  29 KECU
Funding requested from CEC:  29 KECU
in % of Costs  100 %

National Currency for this Participant: Deutschmark Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
2.05  2.05  2.05

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: GMD

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  0  0  0  0
2. Travel and Subsistence  7  7  7  21
3. Durable Equipment  0  0  0  0
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  0  0  0  0
Total  7  7  7  21
(1)  (1)  (1)  (1)
Total Costs  21 KECU
Funding requested from CEC:  21 KECU
in % of Costs  100 %

National Currency for this Participant: Deutschmark Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
2.05  2.05  2.05

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: MANCHESTER UNIVERSITY

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  0  0  0  0
2. Travel and Subsistence  9  10  10  29
3. Durable Equipment  11  0  0  11
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  0  0  0  0
Total  20  10  10  40
(1)  (1)  (1)  (1)
Total Costs  40 KECU
Funding requested from CEC:  40 KECU
in % of Costs  100 %

National Currency for this Participant: Pounds sterling Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
0.714 0.714 0.714

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract TABLE III.2 Project Budget: Partner cost/cost types per year (KECU)

Project: 6811 Acronym: CLICS II

Participant: SUSSEX UNIVERSITY

Year  Year 1  Year 2  Year 3  Total
Cost category  KECU  KECU  KECU  KECU
1. Labour^{(2)}  2  2  2  6
2. Travel and Subsistence  5  4  4  13
3. Durable Equipment  2  2  2  6
4. Consumables  0  0  0  0
5. Services  0  0  0  0
6. Other costs^{(3)}  2  2  2  6
Total  11  10  10  31
(1)  (1)  (1)  (1)
Total Costs  31 KECU
Funding requested from CEC:  31 KECU
in % of Costs  100 %

National Currency for this Participant: Pounds sterling Conversion rates used: Value of 1 ECU in National Currency

Year 1 Year 2 Year 3
0.714 0.714 0.714

N.B. All amounts must be net of VAT, sales tax and customs duties (cf. Art.3.3 of the Contract)

(1) to be carried forward to Table III.3

(2) including overhead costs as applicable (Annex II Art. 25 or Art. 35 of the contract)

(3) to be used strictly in accordance with Annex II Art. 31 of the contract

6811 CLICS II 59

TABLE III.3 Project Budget (KECU) per year Project: 6811 Acronym: CLICS II

Year  Year 1  Year 2  Year 3  Total  Funding
Participants  KECU  KECU  KECU  KECU  to Project
IMPERIAL COLLEGE  76.2  78.9  44.9  200  200
AARHUS UNIVERSITY  51.5  120.5  23  195  195
CAIMENS  70.13  73.25  36.6  180  90
CAMBRIDGE  77  68  46  191  191
DISI-GENOVA  74  67  65  206  103
CHALMERS TH  86  78  78  242  0
TH DARMSTADT  15  7  7  29  29
GMD  7  7  7  21  21
MANCHESTER  20  10  10  40  40
SUSSEX  11  10  10  31  31
Total KECU  487.8  519.6  327.5  1335  900
(1)  (1)  (1)  (2)  (2)
Total Costs  1335 KECU
Requested Project Funding from CEC:  900 KECU

(1) Values carried over from Table III.2

(2) These totals must comply with Art.3 of the Contract

Bibliography

[Abr90] S. Abramsky. Computational interpretations of linear logic. Technical Report DOC90/20, Imperial College, London, 1990.

[Abr91] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1–77, 1991.

[Acz80] P. Aczel. Frege structures and the notions of propositions, truth and set. In The Kleene Symposium. North-Holland, Amsterdam, 1980.

[AJ92] S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. In 7th LICS Conf. IEEE, 1992.

[AW] H.R. Andersen and G. Winskel. The compositional checking of satisfaction. To appear in Computer Aided Verification, Aalborg, July 1991.

[BE91] A. Bucciarelli and Th. Ehrhard. Extensional embedding of a strongly stable model of pcf. In Proceedings of International Conference on Automata, Languages, and Programming (ICALP’91), Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1991.

[BGdP] C. Brown, D. Gurr, and V.C.V. de Paiva. General petri nets and simulation morphisms. To be submitted to the proceedings of the LMS Durham Symposium on Applications of Categories in Computer Science.

[Bro] C. Brown. Linear logic and Petri nets: categories, algegra and proof. PhD thesis.

[BTCGS91] V. Breazu-Tannen, T. Coquand, C.A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and computation, 93:172–221, 1991.

[CG91] Th. Coquand and Stolzenberg G. Wiener’s theorem and certain of its applications. Bulletin of the American Mathematical Society, 24, 1991.

[Coqa] Th. Coquand. An analysis of ramsey’s theorem. Invited talk at LICS 1991, Amsterdam.

[Coqb] Th. Coquand. A direct proof of the intuitionstic ramsey theorem. Invited talk at CTCS 1991, Paris.

[Coqc] Th. Coquand. An intuitionistic proof of tychonoff’s theorem. Journal of Symbolic Logic. to appear.

[Coq90] Th. Coquand. An algorithm for testing conversion in type theory. In Huet G. and Plotkin G., editors, Logical Frameworks 90, 1990.

[Coq91a] Th. Coquand. Constructive topology and combinatorics. In Proceedings of the conference Constructivity in Computer Science, 1991. to appear.

[Coq91b] Th. Coquand. A remark about interactive programs. Draft, 1991.

[CP] R.L. Crole and A.M. Pitts. New foundations for fixpoint computations: Fixhyperdoctrines and fix-logic. Information and Computation. To appear.

[Cur86] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986.

[DH89] P. Dybjer and Sander H. A functional programming approach to the specification and verification of concurrent systems. Formal Aspects of Computing, 1:303–319, 1989.

[EM91] T. Ehrhard and P. Malacaria. Stone duality for stable functions. In Proceedings of Category Theory and Computer Science, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1991.

[FMRS90] P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott. Extensional pers. In Proc. 5th Symposium in Logic in Computer Science, pages 346–354. IEEE Computer Society Press, Washington, 1990.

[Gir89] J.-Y. Girard. Proofs and Types. Cambridge University Press, 1989. Translated and with appendices by Paul Taylor and Yves Lafont.

[GMW79] M.J.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of LNCS. Springer Verlag, 1979.

[Gra88] S. Graham. Closure properties of a probabilistic powerdomain construction. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Language Semantics, volume 298 of Lecture Notes in Computer Science, pages 213–233. Springer-Verlag, Berlin, 1988.

[Hal87] L. Hallnäs. An intensional characterisation of the largest bisimulation. Theoretical Computer Science, 1987.

[HP89] M. Hyland and A. Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. In J.W. Gray and A. Scedrov, editors, Categories in Camputer Science and Logic, volume 92 of Contemporary Mathematics. American Mathematical Society, Providence RI, 1989.

[Hyl] J.M.E. Hyland. First steps in synthetic domain theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Proceedings, Category Theory ’90, Como, Lecture Notes in Mathematics. Springer-Verlag, Berlin. to appear.

[Hyl82] J.M.E.H. Hyland. The effective topos. In L. E. J. Brouwer Centenary Symposium, pages 165–216. North-Holland, Amsterdam, 1982.

[Jon] C. Jones. Probabilistic Non-determinism. PhD thesis, University of Edinburgh. Also published as Technical Report No. CST-63-90.

[JP89] C. Jones and G.D. Plotkin. A probabilistic powerdomain of evaluations. In Symposium on Logic in Computer Science, pages 186–195. IEEE Computer Society Press, Washington, 1989.

[Jun90] Jung. The classification of continuous domains. In Symposium on Logic in Computer Science, pages 35–40. IEEE Computer Society Press, Washington, 1990.

[Koc81] A. Kock. Synthetic Differential Geometry. Cambridge University Press, 1981.

[KT90] D Kozen and J. Tiuryn. Logics of programs. In Handbook of TCS. North Holland, 1990.

[Lin89] I. Lindström. A construction of non-well-founded sets in martin-löf’s type theory. Journal of Symbolic Logic, 1989.

[Men91] N.P. Mendler. Sigma is cocontinuous. Note, 1991.

[ML72] P. Martin-Löf. An intuitionistic theory of types. Unpublished report, 1972.

[Mog89a] E. Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Edinburgh Univ., Dept. of Comp. Sci., 1989. Lecture Notes for course CS 359, Stanford Univ.

[Mog89b] E. Moggi. A category-theoretic account of program modules. In Proceedings of the Conference on Category Theory and Computer Science, Manchester, UK, Sept. 1989, volume 389 of LNCS. Springer Verlag, 1989.

[Mog90] E. Moggi. Modular approach to denotational semantics. Workin Draft, CLICS Deliverable, 1990.

[Mog91a] E. Moggi. Computational types and logic: Evaluation logic. Draft presented at the Meeting on Applications of Categories in Computer Science, Durham UK, 1991.

[Mog91b] E. Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.

[Mos88] P. Mosses. The modularity of action semantics. Technical Report DAIMI IR-75, Comp. Sci. Dept., Aarhus Univ., 1988.

[Mos89] P. Mosses. Denotational semantics. Technical Report DAIMI-PB-276, CS Dept., Aarhus University, 1989. to appear in North Holland Handbook of Theoretical Computer Science.

[Mul86] K. Mulmuley. Fully abstract submodels of typed lambda calculus. Journal of Computer and System Sciences, 33:2–46, 1986.

[NRT90] M. Nielsen, G. Rozenberg, and P.S. Thiagarajan. Elementary transition systems and refinement. Technical report, 1990.

[O’H90] P. O’Hearn. The Semantics of Non-Interference: a Natural Approach. PhD thesis, Queen’s University, Kingstone, CA, 1990.

[Ole85] F.J. Oles. Type algebras, functor categories and block structure. In M. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, 1985.

[Pit] A.M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. Journal of Symbolic Logic. To appear.

[Pit91] A.M. Pitts. Evaluation logic. In G. Birtwistle, editor, IV Higher Order Workshop, Banff 1990, Workshops in Computing. Springer-Verlag, Berlin, 1991.

[Plo80] G.D. Plotkin. Lambda-definability in the full type hierarchy. In J.P. Seldin and J.R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, London, 1980.

[Rey81] J. Reynolds. The essence of algol. In J. de Bakker and J. van Vliet, editors, Algorithmic Languages. North Holland, 1981.

[Rit91] E. Ritter. Categorical combinators for the calculus of constructions. Technical report, University of Cambridge Computer Laboratory, 1991.

[Ros86] G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986.

[Sch] J. Schmidt. Toposes and Types. PhD thesis, University of Aarhus. In preparation.

[Smy] M.B. Smyth. Stable local compactification i. Journal of the London Mathematical Society. To appear.

[Sto88] A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Pitman/Wiley, 1988.

[Tay91] P. Taylor. The fixed point property in sythetic domain theory. In Proc. 6th Symposium in Logic in Computer Science, pages 152–160. IEEE Computer Society Press, Washington, 1991.

[Ten90] R. Tennent. Semantic analysis of specification logic. Information and Computation, 85:135–162, 1990.

6811 CLICS II 63

[Vic89] S.J. Vickers. Topology via Logic. Cambridge University Press, 1989.

[Win90] G. Winskel. A compositional proof system on a category of labelled transition systems. Information and Computation, 87(1/2), 1990.