A Proposal for ESPRIT Basic Research Action

on

CATEGORICAL LOGIC IN COMPUTER SCIENCE

September 17, 1988

by

S.Abramsky, Imperial College, London, UK T.Coquand, INRIA, Rocquencourt, France

P-L.Curien, Y.Lafont, Ecole Normale Superieure, Paris, France

M.Hyland, Cambridge University, UK A.Pitts, Sussex University, UK A.Poigné, GMD, West Germany

G.Rosolini, University of Parma, Italy G.Winskel, Aarhus University, Denmark

Please send acknowledgement of receipt to:

Dr.Samson Abramsky Department of Computer Science

Imperial College of Science and Technology Queen’s Gate London SW7 United Kingdom

Summary

Theoretical Computer Science has emerged as a vital field within Computing Science, which increasingly feeds into and interacts with the more applied work. The distinctive feature of this field is its marriage of what is commonly seen as very “abstract” or “pure” mathematics—e.g. mathematical logic—with very practical engineering concerns. Our proposal is motivated by the belief that recent developments in category theory and the categorical approach to logic are ripe for application in a number of important areas in Computing Science:

• Type theory.

• Domain theory and the semantics of programming languages.

• Logics of computable functions.

• Logics and models for parallel computation.

• Unified theories of specification.

Some of the existing work on the applications of categorical techniques to the above topics suggests that it is possible to achieve treatments of striking conceptual simplicity—due in the main to the small number, but seemingly universal applicability, of the central concepts of category theory. As well as enhancing our understanding of these topics, a categorical treatment can have computational advantages. This is because, formally speaking, a large part of the language of category theory is essentially algebraic in character: thus a categorical explanation of some logical system can be organised as a translation of that sytem into a formally simpler, algebraic language. There is already good evidence that such translations can be put to advantage computationally. (For example, the work of Cousineau, Curien and Mauny on the Categorical Abstract machine). Of course, category theory also provides a framework and tools for constructing and comparing specific mathematical models for these formal systems. More radically, it may be the case that many mathematical objects actually are themselves categories, and this enables them to be organised into suitable models by direct application of categorical constructions.

The technical objectives of our project include:

• A deeper understanding of type structures for programming languages, currently one of the key areas of programming language design.

• Systematic accounts of denotational, operational and axiomatic semantics for programming languages, emphasizing the systematic connections between these kinds of semantics, and indeed the possibilities of automatic derivation of one from another.

• The development of logics for computable functions, which exploit constructivity and the powerful machinery of categorical logic to provide a better match between the logics and the computational concepts being modelled.

• The proposed work on logics and models of parallel computation, and unified theories of specification, both aim at developing a framework in which the highly diverse and superficially disparate work in these fields can be unified and integrated with work in other areas. This is essential if different programming and specification paradigms are to be successfully unified, and if the truly fundamental and enduring concepts are to emerge from the current Babel of competing formalisms.

1 SCIENTIFIC DESCRIPTION

1.1 Background to the proposal

This proposal is motivated by the belief that category theory and the categorical approach to logic are extremely suitable for constructing mathematical explanations of the meaning of very many formal systems which are used (or are proposed to be used) in computer science; and moreover, that these categorical constructs lend themselves to the production of computational systems. More generally, the strong unity of the concepts of category theory, coupled with their wide applicability make the subject an invaluable tool for the application of mathematical techniques in computer science.

An important aspect of the categorical approach to logic is the way it provides translations of possibly complicated logical constructs into formally simpler, categorical ones. The minimum requirement for such a translation is that it preserve the meaning of the logical constructs as embodied in an associated system of proof rules, or operational semantics. In the case that the logical construct formalizes a well-understood concept (i.e. if it is accepted that the proof rules completely capture the concept’s meaning), then it makes good sense to look for categorical translations which not only preserve, but also reflect meaning—resulting in an exact categorical characterization of the underlying concept. Generally speaking, this has proved possible for a remarkably large number of the basic concepts underlying traditional logic. (Substitution, quantification, higher-order functions, the powerset operation and the natural numbers are all examples.) However, many of the mathematical concepts which are of fundamental concern in computer science are not so well understood, in the sense that the operational semantics or proof rules of existing formalizations of these concepts are perceived to not completely capture our informal ideas. In this case, a translation into categorical language can play a dynamic role, suggesting new formal systems and sharpening our understanding of the original concept (or in some cases, showing that our original intuitions were not self-consistent). This use of categorical logic seems particularly promising in the following areas, which are described in more detail below:

• type theory

• domain theory and the semantics of programming languages

• the logic of computable functions

• logic and models of parallel computation

• unified theories of specification.

The work that we are proposing to carry out under each of these heading has a high degree of interdependence. For example, as well as work under the first heading on semantics of type theories, we envisage using highly structured type theories as a key part of the syntax in the investigations under the headings of domain theory and of unified theories of specification. Thus the use of type theory is a common theme throughout. Another such theme is the use of constructive logics with effective computational content.

Category theory itself enters into the study of the above topics in several distinct ways. Firstly, it is the case that many mathematical objects actually are themselves categories, and this enables them to be organized into suitable models of the formal systems we are concerned with by the direct application of categorical constructions. (This idea underlies the work in [4] and [18], for example.) Secondly, the functorial methods of category theory provide us with powerful means of comparing different kinds of mathematical model once they have been organized into categories. (See [36] for an example of this.) Finally, apart from enhancing our technical understanding of these topics, the use of categorical methods can have computational advantages. This is because, formally speaking, a large part of the language of category theory is essentially algebraic in nature: thus a categorical explanation of some logical system can be formalized as a translation of the syntax into a formally simpler, algebraic language. There is already evidence that such translations can be put to use computationally. (The work in [10] on the compilation of functional programs into categorical combinators executing on the Categorical Abstract Machine is an example of this.)

World-wide, there are very few people indeed who have both a firm grasp of the technicalities of category theory and an understanding of the relevant problems in computer science. Europe has very strong workers in each of the two subjects who are actively engaged in persuing the connections between them, and who are brought together by this proposal. As well as carrying out the particular programme of research to be described below, an important aspect of this Basic Research Action will be its role in producing a supply of research workers in computer science who also have a thorough grounding in categorical methods. To achieve this, we are requesting support for a number a research assistants to be recruited both from mathematics and from computer science backgrounds, together with sufficient funds for their travel and subsistence.

1.2 Type theory

Type-theoretic notions are currently the subject of intensive research in several areas of computer science and information technology. Type theory is being used in the design of programming languages to achieve a number of beneficial effects: as well as facilitating the use of rich data structures, it can be used to enforce the writing of well-structured code and, through type checking, reduce the occurrence of certain kinds of error; moreover, the use of various kinds of polymorphic types permits the writing of generic algorithms. The logical systems which have been proposed in the study of the foundations of the mathematics of computation have type theory as an essential ingredient. Amongst the various logical formalisms which have been proposed for the process of specifying and proving properties of programs, type theories such as the higher order typed lambda calculus and Martin-Löf’s systems are distinguished by the fact that they lend themselves readily to mechanization. (Indeed their strongly constructive nature permits the theoretical possibility of automatic extraction of programs from specifications.) This has resulted in proof assistants and automated deduction systems such as LCF [15], AUTOMATH [2], NuPRL [3] and the Theory of Constructions [9]), but also to a beginning of the theory of modules for the programming language Standard ML [24].

In many of these developments it is the case that operational practice is in advance of rigorous explanations of the meaning of the constructs involved (such as dependent types, polymorphic and higher order type structures and universal types mixed with recursively defined types). Providing mathematical models for these concepts is a great challenge: classical set theory and logic are often inappropriate for this task, whereas category theory and categorical logic are proving to be well suited to it.

Under this topic we propose to continue the work on categorical semantics of type theories begun in [7, 5, 3, 18]. This work aims to understand the notion of domain used in denotational semantics from a categorical-topos point of view. It appears on the basis of [18] that this work will form the backbone of a very powerful language for highly modular algebraic specification. The case of complete algebraic lattices seems well-understood now [9, 18], but more research has to be done in order to cover the other notions of domain, like Scott domain, or the non-standard Girard-Berry domains [13]. From the work that has been done so far in this direction, it is clear for instance that the notion of Diers category will play an important role [11] (see also [23]). This notion is furthermore clearly connected with the concept of stable functions and stable ordering that appear in the work of [13, 37]. We get in this way new “relatively” cartesian closed categories (to use P. Taylor’s terminology [33]). This leads to a natural categorical generalisation of the notion of domains [4].

This work gives strong evidence of the usefulness in this area of some existing parts of category theory which are not easily accessible to the non-expert (such as the theory of classifying spaces (toposes), fibred categories and the theory of 2categories). Within the groups involved in this research proposal there are experts on these aspects of category theory and there are experts on the syntactic and computational aspects of type theory currently of interest in computer science. The proposal is intended to bring these different areas of expertise into close working cooperation. We would also expect this part of the proposal to interact with the work being carried out at Edinburgh and INRIA on mechanized frameworks for defining logics.

1.3 Domain theory and the semantics of programming languages

We envisage research on the categorical axiomatization of denotational semantics and on the relationships between denotational, operational and axiomatic semantics.

The categorical axiomatization of denotational semantics will be driven by the abstract properties of a “category of domains” which allow us to interpret various programming constructs; the axiomatisation is likely to cover far more than the well-known examples. This should lead to a better understanding of logics of computable functions, and ways to improve them, as well as a better understanding of the relationships and choices between the various categories of domains and other structures which have been proposed for programming language semantics. The discovery of new categories for semantics is bound to suggest new possibilities for language design.

Recent work on the categorical description of partial functions, partial cartesian closed categories etc. and its convergence with work by Plotkin on a computationally motivated reformulation of denotational semantics in terms of pre-domains, offer the prospect that good progress can be made in this area.

Much work has already been done on the relationships between denotational, operational and axiomatic semantics. What we seek are systematic connections, which give criteria for the appropriateness of definitions, and allow the systematic derivation of one kind of semantics from another. This idea has already been pursued successfully by one of the investigators with respect to the connections between denotational and axiomatic semantics, using ideas from Stone duality. We would like to see a similar development vis a vis operational semantics. The most promising approach is based on the constructor-selector paradigm (corresponding to the introduction rule-elimination rule paradigm in logic). This paradigm has been applied by Martin-Lof, Plotkin and some of the investigators to the systematic description of operational semantics for (functional) programming languages, and their relationship to denotational semantics. It offers the most convincing current formalisation of the eager and lazy evaluation paradigms. At the same time, well-known correspondences in categorical logic (e.g. between lambda calculi and cartesian closed categories) suggest that this paradigm can be captured in categorical-algebraic form. If so, one could systematically transform denotational into operational semantics, and even implementations—a novel approach to the long-standing research topic of “semantics-directed compiler generation”. Successful case studies of this kind have been carried out by one of the investigators [22].

1.4 Logic of computable functions

The general intention is to use ideas from category theory, and particularly topos theory, in order to build elegant proof systems for reasoning about and for generating programs. This approach has been advocated by D. Scott, [31], for many years but has not yet been tried effectively.

We aim to exploit the fact that many complex structures can be seen as simple structures inside a suitable topos. Complicated arguments and constructions can then be replaced by familiar (constructive) ones. This leads to the possibility of “synthetic” treatment of recursion theory (and of domain theory—see above) as a theory of functions in a topos, where the effectivity (and continuity) are encapsulated in the topos. We also wish to pursue the idea of (automatically) generating programs from constructive proofs [16]. (For this to be feasible we will need to develop syntax with clear proof theoretic properties. Category theory has itself proved of value in establishing such properties). We propose to study two concrete cases.

The first case is the use of various (pre)sheaf models. This approach shows in an elegant and simple way how to embed different logics conservatively in full (intuitionistic) higher-order logic. The use of intuitionistic logic is vital here, since such an embedding is not possible with classical logic. For instance, one of the investigators has shown that a strong form of polymorphism is compatible with (constructive) set theory [27] in constrast to a well-known negative result of Reynolds for classical set theories [29]. It must be noted that presheaf models are but the more elementary examples of Grothendieck toposes, and it is likely that the use of suitable topologies will bring new and interesting results. In particular, it may be interesting to understand how to generalise the work of [18] to Diers category [11] (considered recently in order to give a semantics of type theory) via a suitable topology on presheaf toposes.

The second case is the effective topos. It is our intention to continue our investigations of this topos and on the categories in it which enjoy such strong closure properties as to model polymorphic theories (cf. [17, 6, 19]). Although some of these models were already known under a different guise, it is clear now that only by understanding them within a universe for constructive set theory can we make further developments. This also supports the claim that a constructive approach to theories of computation and their models is indeed very suitable as functions defined constructively are necessarily continuous and effective [30]. It should be noted that, until now, only the basic notions of recursion theory have been used, and there are hopes of using more subtle notions of realisability (like that developed by Kleene for intuitionistic analysis) and more subtle arguments of recursion theory (like the priority method).

Another area of research (also advocated by D. Scott and which is far from fully explored) is the logic of existence and partial elements (see for instance [12]). This logic was originally motivated by topos theory. One may hope to tie it up with the work on partial functions by Moggi and Plotkin [25], [28] and to develop from this a logic of programs (a preliminary version is in Rosolini’s thesis [30]).

A more non-standard, but already promising, topic is the study of functional interpretations, like the dialectica or modified realisability interpretation [34], from a categorical point of view. In the case of the dialectica interpretation this surprisingly led, as shown by a student of M. Hyland [26], to a model of linear logic [14]. The connections with more traditional models need to be clarified.

As for the work in type theory, since some members will be in close relationship with the development of mechanized frameworks for defining logics, we intend to study these various kind of logics in a concrete way (an implementation of Intuitionistic Zermelo-Fraenkel is already running in the construction system developed at INRIA).

1.5 Logic and models for parallel computation

The problem with the mathematical study of parallelism has not been the lack of models and proof systems but rather the multitude of them. Already category theory has proved useful in getting to the conceptual heart of the area. By regarding models of parallel computation as categories, with morphisms which relate behaviours, basic operations of parallel programming languages are being shown to arise as universal constructions. As an example in [36], it is shown how parallel compositions of the languages CCS, CSP and OCCAM in a variety of models are derived from products, while their non deterministic sums are coproducts. Further benefits then come from the use of adjunctions to relate different models, regarded as categories, relying on the preservation properties of adjoints to see formally how semantics in one model translate to semantics in another.

Morphisms can play a valuable role in reasoning about processes and, for instance, the behaviour of a parallel composition is that which projects, via the projection morphisms into behaviours of the components. Such facts have been exploited in [38], where a complete proof system for a parallel programming language is presented. It is compositional in the sense that the proof system works by, for example, reducing showing an assertion holds of a parallel composition to showing assertions hold of the components. The structure of the proof system has been guided by indexed category theory and categorical logic and makes essential use of some constructs on assertions which are best understood in this framework. The proof system is not just of theoretical interest; there are plans to incorporate its proof rules into an implementation of a compositional model checker, an algorithm which, directed by the structure of a term describing a finite-state process, deduces whether or not a model assertion holds of it.

A related area, amenable to similar techniques, is that of models, proof systems and model checkers, for hardware and circuits as used in VLSI design. Here the problems associated with abstractions from detailed models are especially pressing. Elementary uses of categorical logic have shown promise both for constructing proof systems and showing when simpler models and reasoning suffice (see [39], [40], [41]). An obvious, and probably not too hard, problem to solve is the relation between the model of switching circuits in [20] and the others.

Although there have been successes, the mathematical understanding of models and logic of parallel processes is far from complete. Many specific tasks remain in extending the work indicated here and understanding the general framework in which it fits. For instance how do we square domain theory with the work on parallelism? Results here are scanty. For the special language SCCS, the work of [1] successfully ties-up logic of powerdomains and the idea of bisimulation equivalence independently motivated by Milner’s work in parallelism. And then, there is work on the logic of event structures, a model for parallel computation, which also represent the nonstandard domain theory of Berry and Girard; work on this logic is now being understood as and example of work in Diers categories [11], [21]. Possibly there are benefits to be had from embedding models in a topos, and it seems there may be an abstract way of understanding modalities which would make more systematic the choice of assertions and logic appropriate to a particular model of computation.

Ultimately, we cannot expect the theory of parallel computation to remain so separate a study. Category theory and categorical logic furnish the most promising tools we know of to see its place in the general setting of a theory of computation.

1.6 A unified theory of specification

Whatever logical system they are based on, theories of specification invariably depend on certain operations and relations on modules. This observation suggests a unified theory of specification independent of the particular underlying logic. The concept of institutions developed by Burstall and Goguen is the most successful attempt so far to develop a unified theory of specification. Institutions are a formalization of abstract model theory of Barwise, but as such are restricted in that they do not yet support operational semantics or a theory of descriptions. Descriptions are an integral part of many specification theories (e.g. abstract syntax in denotational semantics, terms in algebraic specifications, programs for predicate transformer semantics) in that operations on modules refer to the level of descriptions (e.g. implementation of programming languages).

Categorical logic provides another, and we believe richer, basis for a unified theory of specification. Lawvere’s doctrines provide a categorical notion of logical system (the weakest example being an indexed category) and functorial semantics provides a model theory. Doctrines distinguish between level of descriptions (the base category) and formulae (the fibres) where descriptions act as transformers on formulae. This paradigm is of enormous versatility covering traditional logics such as first and higher order predicate logics, programming logics such as Djikstra’s predicate transformer logic and Abramsky’s logic of domains allowing for a systematic analysis as well of the relation between the logics used for programming/specification as of the interplay of logical structure and specification method. Extension to a 2-categorical setting should allow us even to incorporate structural operational semantics [28], [32] into the paradigm.

Category theory provides a highly uniform specification language for logical systems a concrete representation of which (e.g. Lambek’s deduction calculus) can provide the foundation for a “meta” proof system (as polymorphic substitution for the Edinburgh LF project).

Within this area we propose to study the categorical axiomatization of some specific programming logics, including Abramsky’s logic of domains [1]. We shall analyse the minimal structural requirements for specification methods and how to handle specifications at different levels of abstraction (e.g. implementation of an equational specification by a specification in a programming logic). We hope also to develop a specification language for logical systems based on the categorical framework we are led to.

1.7 Research goals

Meta-language and logic for denotational semantics: The production of a richly typed meta-logic for denotational semantics with a corresponding categorical axiomatization. This requires the following programme of work:

(a) In type theory: The investigation of the internal type theories of existing categories of domains. This involves work on the use of fibred category theory to give a categorical axiomatization of dependent type structures, and the use of 2-category theory to treat recursively defined types and terms.

(b) In the logic of computable functions: The fusion of work on the higher order categorical logic of partial elements and partial lambda calculus with the work described in (a). We would like to use the fixed point category in the effective topos as the basis for an axiomatic theory of domains and of “total” types.

(c) In domain theory: Testing the denotational meta-logic against properties of various new “domain-like” categories which are currently under investigation (using techniques of categorical logic to do with classifying toposes of theories in geometric logic). Investigation of structured operational semantics for the meta-logic and its relationship to the categorical axiomatization. Epistemic type theory: Under this heading we intend to develop a a type theory which supports both classical and constructive logic. The aim is to have (in the same system) the means to use classical logic in arguing about the correctness of programs, and to derive programs automatically from constructive proofs. The main technique would be the use of realizability models. We would like to investigate in the context of type theories the value of deriving programs from proofs by realizability. Experience shows that (differences between) categorical models highlight a host of subtle differences between the strength of various rules in type theory. We aim to consider in particular the problematic rules for “existential” types and for identity types. Languages and proof systems for parallel processes: A language for parallel processes should support obvious operations like parallel composition and nondeterministic choice and have facilities for “hiding”(making actions internal) and recursive definitions. Ideally, it would also support an idea of one process implementing another and be higher order. The category theoretic understanding of these operations is incomplete, specifically we would like:

(a) To extend the existing relations between categories of models for concurrency by developing a method of handling recursively defined processes which works in a uniform way across the different models (the techniques of denotational semantics and type theory will be useful).

(b) To develop a categorical treatment of “hiding” as supported in many models of concurrency—this is likely to involve similar ideas to those in models of type theory through the idea that a process is modelled by its “type” of computations.

(c) To examine how morphisms representing the implementation of one process by another in the manner of (e) (there are several candidates around) interact with the categories and their constructions used in modelling parallel processes, and if successful test these results on a parallel programming language which supports the idea of implementation.

To strengthen our understanding of proof systems of parallel processes in terms of categorical constructions we shall, in particular, develop a a logic for event structures (ideas will derive from work on type theory and domain theory and affect that on specification). It is planned to automate some compositional proof systems which result, and in the decidable cases to get compositional assertion checkers. Another problem, probably not so hard, is to formally relate the models and proof systems of [20] and [40] used in hardware verification. A high level specification language: We plan to develop a high level specification language. Ideally, this would be a polymorphic system with a level of types and kinds, and a distinct level of algebraic specifications. One would pass from the latter to the former by taking initial models (“data” in the specification language CLEAR). This work will incorporate experience from the area of algebraic specification in general. It should specialise to a semantic treatment of signatures and structures in the programming language Standard ML. As subgoals we plan to give a categorical axiomatisation of several programming logics including Abramsky’s logic of domains for denotational semantics and, based on examples from work in domain theory and concurrency, to analyse the minimal assumptions on categories necessary to support the specification methods. One problem is how to treat specifications at different levels of abstraction in the sense of one object implementing another as in the work on concurrency above.

1.8 Work plan

With the enumeration

1. Type theory

2. Domain theory and the semantics of programming languages

3. Logics of computable functions

4. Logics and models for parallel computation

5. Unified theories of specification

we can summarise the main interests of the partners as follows:

• Imperial College: 2, 3, 4

• INRIA: 1, 2, 3

• Ecole Normale Superieure: 3

• Cambridge University: 1, 2, 3, 5

• Sussex University: 1, 2, 3 , 5

• GMD: 2, 4, 5

• University of Parma: 2, 3

• Aarhus University: 1, 2, 4,

There are a great many common interests amongst the different sites. We intend to have frequent visits to learn the most recent results of each others research and to coordinate future work. Each year there will be a workshop for all participants and associates. These will also function as review points. The final workshop will be open to the academic community.

Deliverables: Certainly, as deliverables each site shall produce reports and papers on their research. These will be issued on a yearly basis. In addition there will be a book of either the workshop proceedings or a choice of papers produced by the participants over the 3 year period. With work of a theoretical and exploratory nature it is hard to promise direct applications, though it seems highly likely that there will be some other deliverables in terms of implementations or descriptions of implementation of formal systems such as compositional assertion checkers, automatic proof assistants or or programs which extract executable code from constructive proofs.

References

[1] S.Abramsky. Domains in logical form. In the proceedings of LICS 1987.

[2] Nicholas G.deBruijn. “A survey of the project AUTOMATH.” In: J.P.Seldin and J.R.Hindley (eds), To H.B.Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism (Academic Press, London), 1980.

[3] Robert L.Constable et al, Implementing Mathematics with the NuPRL Proof Development System (Prentice-Hall, Englewood Cliffs NJ), 1986.

[4] Th. Coquand. “Categories of Embeddings.” To appear in the proceedings of Logic in Computer Science, Edinburgh, 1988.

[5] Th. Coquand and Th. Ehrhard. “An equational presentation of higher order logic.” In: D.H.Pitt, A.Poigné and D.E.Rydeheard (eds), Category Theory and Computer Science. Proceedings Edinburgh Springer Lecture Notes in Computer Science No.283, 1987.

[6] Carboni, Freyd, Scedrov. “A categorical approach to realizability and polymorphic types.” In the proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics, New Orleans, LA, 1987.

[7] Th. Coquand, C. Gunter and G. Winskel. “Domain theoretic models of polymorphism.” Cambridge Technical Report 116, submitted to Information and Control, 1987.

[8] Th. Coquand, C. Gunter and G. Winskel. dI-domains as a model of polymorphism. To appear in the proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics, New Orleans, LA 1987.

[9] Th. Coquand and G. Huet. “Constructions: a higher-order proof system for mechanizing mathematics.” In: B.Buchberger (ed.), EUROCAL ’85. Proceedings Vol.I, Lecture Notes in Computer Science No.203 (Springer-Verlag, Berlin–Heidelberg), 1985.

[10] G.Cousineau, P.-L.Curien andM.Mauny. “The categorical abstract machine.” In: Proc. ACM Conference on Functional Programming Languages and Computer Architecture, Nancy, 1985.

[11] Y. Diers. “Catégories Localisables.” Thèse de Doctorat d’Etat, Université Paris 6, 1977.

[12] M. Fourman. “The Logic of Topoi.” In the Handbook of Mathematical Logic, North Holland, 1977.

[13] J.Y. Girard. “The system F, fifteen years later.” Theoretical Computer Science, vol. 45, 1986.

[14] J.Y. Girard. “Linear Logic.” Theoretical Computer Science, vol. 48, 1987.

[15] Michael Gordon, Robin Milner and Christopher Wadsworth. “Edinburgh LCF: a Mechanized Logic of Computation.” Lecture Notes in Computer Science No.78 (Springer-Verlag, Berlin–Heidelberg), 1979.

[16] S. Hayashi and H. Nakano. “PX, a Computational Logic”, April 1987, Kyoto University, RIMS-573.

[17] M. Hyland. “The effective topos.” in The L.E.J. Brouwer Centenary Symposium (ed. by A.S. Troelstra and D. van Dalen), North Holland, 1982.

[18] M. Hyland and A. Pitts. ‘The theory of constructions: categorical semantics and topos-theoretic models.” In: J.Gray and A.Scedrov (eds), Categories in Computer Science and Logic, Contemporary Math. (Amer. Math. Soc., Providence RI), to appear.

[19] M. Hyland, E. Robinson, G. Rosolini. “The discrete objects in the effective topos.” submitted to Proc. of the L.M.S., 1987.

[20] C.A.R.Hoare. “Towards a calculus of total correctness for the design of C-MOS switching circuits”. In preparation.

[21] P.Johnstone. “A syntactic approach to Diers’ localizable categories”. In proc. of Durham conference on Applications of Sheaves 1977, Springer lecture notes in Mathematics 153, 1979.

[22] Y. Lafont. PhD thesis, Ecole Normale Superieure, Paris, 1987.

[23] F. Lamarche. “A simple model of the theory of constructions.” In: J.Gray and A.Scedrov (eds), Categories in Computer Science and Logic, Contemporary Math. (Amer. Math. Soc., Providence RI), to appear.

[24] D. MacQueen. “Using Dependent Types to Express Modular Structure.” in ACM Principles of Programming Languages, 1986.

[25] E.Moggi. The partial lambda calculus. PhD thesis, C.Sc. dept., Univ. of Edinburgh , forthcoming (1988).

[26] V. de Paiva. “Dialectica Categories.” In: J.Gray and A.Scedrov (eds), Categories in Computer Science and Logic, Contemporary Math. (Amer. Math. Soc., Providence RI), to appear.

[27] A. Pitts. “ Polymorphism is set-theoretic, constructively.” In: D.H.Pitt, A.Poigné and D.E.Rydeheard (eds), Category Theory and Computer Science. Proceedings Edinburgh, Springer Lecture Notes in Computer Science No.283, 1987.

[28] G.D.Plotkin. Types and partial functions. Handwritten lecture notes for a course at C.Sc. dept., Univ. of Edinburgh (1984).

[29] J.C.Reynolds. Polymorphism is not set-theoretic. In the proceedings of the conference on Abstract Datatypes, Sophia-Antipolis, France in June 1984, Lecture notes in C.Sc. 173 (1984).

[30] G. Rosolini. “Continuity and effectiveness in topoi” Technical Report CMU-CS-86-123, Carnegie-Mellon University, 1986.

[31] D. Scott. “Relating Theories of the Lambda-Calculus.” In: J.P.Seldin and J.R.Hindley (eds), To H.B.Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism (Academic Press, London, 1980).

[32] R.A.G.Seely. Modelling computations: a 2-categorical framework. In the proceedings of LICS 1987.

[33] P. Taylor. “Recursive domains, indexed category theory and polymorphism.” Ph.D. Thesis, University of Cambridge, 1987.

[34] A.S. Troelstra. “Metamathematical Investigation of Intuitionistic Arithmetic and Analysis.” Springer Lecture Notes in Mathematics 344.

[35] G.Winskel. “Categories of models for concurrency.” In the proceedings of the workshop on the semantics of concurrency, Carnegie-Mellon University, Pittsburgh, Springer Lecture Notes in Computer Science 197 (July 1984).

[36] G.Winskel. “Category theory and models of parallel computation.” In proceedings of the Workshop on Category Theory and Computer Programming, University of Surrey, Guildford, September 1985, published in Springer Verlag Lecture notes series.

[37] G. Winskel. “Event structures.” Invited lectures for the Advanced Course on Petri nets, in Springer Lecture Note in Computer Science 255, 1986.

[38] G.Winskel. “ A category of labelled nets and compositional proof system”. To appear in the proceedings of the the conference “Logic in Computer Science”, Edinburgh July 1988.

[39] G.Winskel. “ Lectures on models and logic of MOS circuits.” Four invited lectures for the Marktoberdorf Summer School, July 1986. Published by Springer.

[40] G.Winskel. “A compositional model of MOS circuits”. In “VLSI Specification, Verification and Synthesis”, G.M. Birtwistle and P.A. Subrahmanyam (eds) Kluwer Press 1987.

[41] G.Winskel. “ Relating two models of hardware”. In: D.H.Pitt, A.Poigné and D.E.Rydeheard (eds) Category Theory and Computer Science. Proceedings Edinburgh, Springer Lecture Notes in Computer Science No.283, 1987.

2 ADMINISTRATIVE AND FINANCIAL IN-FORMATION

3 PARTICIPATING SITES AND INDIVIDU-ALS