CLICS II

Categorical Logic in Computer Science II Basic Research Action Project Number: 6811

⋆ ⋆ ⋆ ⋆ ⋆ ⋆⋆ ⋆ ⋆ ⋆ ⋆⋆

Final Report February, 1996

Contents

1 Executive summary 2 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Technical objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Research topics and workplan . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Summary of achievements . . . . . . . . . . . . . . . . . . . . . . . . 6 1.5 Selected publications . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Reports on research topics 14

2.1 Topics A and G: Sequentiality and Stability, and Concurrency and

Linear Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2 Topic B: duality in domain theory . . . . . . . . . . . . . . . . . . . . 19 2.3 Topic C: logic of inductive and recursive datatypes . . . . . . . . . . 29 2.4 Topic D: subtypes and polymorphism in higher order languages … 34 2.5 Topics E and F: higher order modal program logics and monadic

programming language semantics . . . . . . . . . . . . . . . . . . . . 40 2.6 Topic H: computational content of classical proofs . . . . . . . . . . . 45 2.7 Topic I: symbolic computation . . . . . . . . . . . . . . . . . . . . . . 49

3 Conclusions and exploitation of results 51

Chapter 1

Executive summary

1.1 Introduction

The CLICS project started in October 1989 (BRA 3003) and continued as CLICS-II (BRA 6811) until December 1995. The objectives of the project were pitched at an foundational level. This was motivated by the observation 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. The aim of the project was 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 practicing 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.

Main Areas and Technical Objectives. To address the above issues the CLICS II programme planned 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. Section 1.2 recalls the technical objectives set out for each area.

Research Topics. The cooperation between partners was organized around nine research topics (spanning across several or all the main areas): Sequentiality and Stability, Duality in Domain Theory, Logic of inductive and recursive data-types, 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.

Partners. The partners involved in the project were from six countries: Denmark (Aarhus), France (CAIMENS), Germany (Darmstadt, GMD), Italy (Genova), Sweden (Chalmers) and United Kingdom (Cambridge, ICSTM, Manchester, Sussex). Also other researchers have expressed an interest in the proposed work.

1.2 Technical objectives

This section recalls the technical objectives set out in the TA (Section I-3.3).

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 optimization, 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 data-types. The issue 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 Abramsky 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.

Semantics and Logics of Programming Languages. The main thrust of our work here is to pursue the monadic approach to programming language semantics proposed by Moggi, 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.

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

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 Coquand, 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 emphasize 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.

1.3 Research topics and workplan

The workplan was organized into nine research topics. The scientific content of these topics and the results achieved are described in Chapter 2. As with any basic research, it was impossible to predict accurately what research will be done during a given period of time. The plan was to stimulate work on selected topics by holding workshops focused on specific topics involving only the relevant collaborating partners, and to adapt the Workplan at each review point. The dependency and timing of the topics as given in the TA are reported below: partners expected to play a secondary role and changes to the original plan are indicated in parenthesis.

Topic A Sequentiality and stability.

Partners: Aarhus, Cambridge, Darmstadt, CAIMENS, (Genova, Sussex). Interaction with B. (Interaction with G, Imperial made major contribution) Timing: months 0–24. (0–36)

Topic B Duality in Domain Theory.

Partners: Aarhus, Cambridge, Darmstadt, CAIMENS, GMD, Imperial, (Manchester). Interaction with A. (Interaction with E) Timing: months 0–36.

Topic C Logic of inductive and recursive data-types.

Partners: (Aarhus), Cambridge, Chalmers, (Genova), Manchester. Input from B. Interaction with E. Timing: months 0–24. (0–36)

Topic D Subtypes and polymorphism in higher order languages.

Partners: CAIMENS, Genova, Manchester, Sussex. Depends on C. Timing: months 6–30.

Topic E Higher order modal program logics.

Partners: Cambridge, Genova, Imperial. Interaction with C. (Interaction with B) Timing: months 0–24.

Topic F Monadic programming language semantics.

Partners: Cambridge, Genova, Sussex. Input from E. Timing: months 6–36.

Topic G Applied Linear logic.

Partners: Aarhus, Cambridge, CAIMENS, (GMD), Imperial. (Interaction with A) Timing: months 0–36.

Topic H Computational content of classical logic.

Partners: Chalmers, (Imperial, Manchester). Timing: months 0–36.

Topic I Symbolic computation.

Partners: (Cambridge), Chalmers, CAIMENS, (Genova, Manchester). Input from G and H. Timing: months 6–36.

1.4 Summary of achievements

This section summarizes the main achievements of the project.

• Sequentiality and Stability (Topic A). The project has made a breakthrough by solving the classical full abstraction problem for PCF. The key tool to achieve this result has been game semantics. In fact, game semantics has been very important for other project topics: concurrency (Topic G) and computational contents of proofs (Topic H). The potential of game semantics has still to be fully exploited.

The project has pursued also a more extensional approach (already in CLICS-I), originating from the classical notions of stability and sequential algorithms. This more traditional line of research has improved the previous state of the art, but it has not lead to major breakthroughs as the game-theoretic approach.

• Synthetic domain theory (Topic B). The project has taken seriously the original idea of Dana Scott of domains as sets and worked hard to make it viable, with important technical contributions by Peter Freyd and people in Edinburgh. This research topic was the most speculative in the project, and more work needs to be done. Synthetic domain theory itself is meant for semanticists, but it is the mathematical underpinning for more usable formalisms, e.g. evaluation logic and a new version of LCF (Topic E). The main contributors to the mathematical foundations of the subject are Hyland, Phoa, Rosolini and Taylor.

• Classical domain theory (Topic B). CLICS has made important contributions to the already well-developed subject of domain theory. The notion of duality in the context of domain theory (useful for example for generating program logics from denotational semantics) was proposed by Abramsky and has been extended to larger classes of domains in CLICS-II. Other contributions are of a more technical nature: linear decompositions of categories of domains, systematic investigation of various forms of power-domains (for non-determinism, probabilistic computations and databases), new notions of bidomain and stronger notion of stability. Most of this work has been of a mathematical nature, but some of it has been motivated also by applications, e.g. to database theory and full abstraction.

• Categorical semantics of type theory and polymorphism. The project has been at the forefront of research here, both in making precise the categorical structure necessary to model various form of dependent and polymorphic types, and in studying specific models. It is difficult to image how certain meta-theoretic results about type theory (e.g. Hofmann’s interpretation of extensional type theory in the intensional one) or the widespread use of realizability models (e.g. to validate rich typed languages) could have been achieved without this foundational work. In the second part of the project this foundational work has produced two lines of research: logic and semantics for inductive and recursive types (Topic C), subtypes and polymorphism in higher order languages (Topic D).

Under this heading one should mention: the work of Hyland and Ong on a modified realizability, which suggests a new semantic technique for proving Strong Normalization; and the categorical analysis of coherence problems in type theory by Curien and Dybjer.

• Logic for inductive and recursive types (Topic C). The work done on simultaneous inductive-recursive definitions may provide the mathematical underpinning for more powerful proof assistants based on type theory (the present ones cannot deal with induction on universes or reflection principles). The expressiveness of inductive-recursive definitions has been tested by formalizing type theory in itself (internal type theory). A similar line of research regarding coinductive definitions has been inconclusive. Under this heading one should include also the categorical analysis of logical predicates and induction by Hermida.

Various reasoning principles have been developed for recursive definitions (FIXlogic) and relational properties of domains. The study of relational properties of domains was inspired by Freyd’s analysis of recursive types in the context of algebraically compact categories, and resulted in mixed induction-coinduction principles. The usability of these principles has been tested by establishing properties of functional programs, and by providing a more systematic way of establishing adequacy results.

There has been fruitful interaction between research under Topic C and the research of the ESPRIT BRA TYPES. Our research contributed to the development of the type theories underlying the proof assistants Alf, Coq, and Lego developed by TYPES. While these proof assistants have been used for implementing some of our work on internal type theory and normalization under Topic C and our work on new versions of LCF under Topic B. In January 1995 we organized a joint workshop with TYPES on Categories and Type Theory in Göteborg.

• Subtypes and polymorphism in higher order languages (Topic D). The main focus has been on relational parametric polymorphism, while little progress has been made on sub-typing. Parametric polymorphism has been investigated both at the syntactic and semantic level. System F has been extended to incorporate the ability of expressing properties of relations, and various known properties of parametric models have been established formally. On the semantic side, the notion of categorical model of system F has been refined to account for relations, and a general definition of parametric model has been proposed. Moreover, a general construction has been given, to turn categorical models of system F into parametric ones.

• Monadic approach. The monadic approach to programming language semantics was developed as part of CLICS-I and is now a well-established tool. Thanks to Phil Wadler, it has had a major impact also on the design of functional languages (in particular Haskell). In the second part of the project this has produced two closely related lines of research: higher order modal program logics (Topic E) and monadic programming language semantics (Topic F).

The work on program logics was focused on evaluation logic, and at a later stage has incorporated ideas from FIX-logic and SDT into a general purpose metalanguage. Another important aspect incorporated in this metalanguage is the incremental approach to semantics. However, the incremental approach and evaluation logic have not had a major impact, yet. Their main potential is as part of computer assisted program verification tools.

The work on monadic semantics was focused on functional programs with references (as in Standard ML). It has produced two metalanguages: the nu-calculus and the monadic store calculus. The first highlights in its simplicity the difficulties of reasoning about dynamic creation of names, while the latter is closer to SML. For the first calculus it was possible to give a denotational semantics based on dynamic allocations monads, while for the store calculus a more operational approach was adopted, based on applicative bisimulation. The denotational approach has been applied more successfully to CCS-like languages. Indeed it was possible to construct a fully abstract model of the π-calculus, without developing any new technique.

• Applied linear logic (Topic G). Here the main objective was to contrast the plethora of calculi and models through unifying concepts and precise links with logic: a categorical approach to relate different models of concurrency, an abstract notion of bisimulation in terms of open maps, the use of linear logic as a specification language for processes, the link between data-flow networks and Girard’s geometry of interaction. Under this heading, one should mention the work on interaction nets, a simple computational model directly inspired by linear logic, and interaction categories, which originated from early work in CLICS, and have been extensively used in the BRA CONFER.

• Computational content of classical proofs (Topic H). The work on this topic has investigated two lines of research: to improve known extraction methods, and to use ideas from formal topology. The first line of research has resulted in better algorithms extracted from classical proofs, and the ability to cope with proofs using the axiom of choice. The second line has produced only heuristic methods, which however can extract algorithms from proofs, when more general methods fail.

• Symbolic computation (Topic I). There have been two main contributions in this area: calculi with explicit substitution, and a more geometric approach to rewriting based on Penrose diagrams. Calculi with explicit substitution were considered mainly in CLICS-I. They are closely linked to the categorical semantics of type theory, and have been very useful in the implementation of languages such as QUEST. The geometric approach to rewriting has been pursued in CLICS-II. A general theory of rewriting for these diagrams has been more complicated than expected, and has been only partially developed by Lafont. On the implementation side, Massol has produced a graphical tool for manipulating diagrams.

• Information dissemination. Particular attention was paid to making the results of the project available to more applied researchers. Besides publications in international journals and conference proceedings, CLICS members have been very active in writing monographes or advanced textbooks, teaching courses at various summer schools and producing lecture notes. There were several contributions to the handbook of “Logic in Computer Science”: Domain Theory, Full Abstraction, Categorical Logic, Models of Concurrency. In September 1995 the project has organized in Cambridge a very well-attended summer school (about 100 participants, mainly post-graduates and post-docs). Moreover, there were useful interactions with two closely related ESPRIT BRA: CONFER and TYPES.

• Prototype implementations. Some sites have produced experimental implementations:

– An interactive tool for manipulating Penrose diagrams by Yves Lafont and Anne Massol at Marseilles;

– A functional language LiLac based on linear logic by Ian Mackey at Imperial;

– A Categorical Abstract Machine for the Calculus of Construction by Eike Ritter at Cambridge. Because of its good performance compared with other implementations, Ritter’s CAM is likely to be used in a new implementation of the LEGO proof assistant.

Moreover, Chalmers used the ALF-implementation (produced by the TYPES project) for implementing various idea developed in Topic C.

1.5 Selected publications

This section gives a selection of publications produced by the project (classified by topic), and a list of publications which count as information dissemination.

Topic A

[AJM95] S. Abramsky, R. Jagadeesan and P. Malacaria. Full Abstraction for PCF. 60 pages. Submitted for publication, 1995.

[BE] A. Bucciarelli and T. Ehrhard. A theory of sequentiality. Theoretical Computer Science. To appear.

[Ehr93] T. Ehrhard. Hypercoherences: A strongly stable model of linear logic. Mathematical Structures in Computer Science, 3:365–386, 1993.

[HO95] M. Hyland and C.-H. L. Ong. On Full Abstraction for PCF. 130 pages. Submitted for publication, 1995.

[JS93] A. Jung and A. Stoughton. Studying the fully abstract model of PCF within its continuous function model. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 230–244. Springer Verlag, 1993.

[McM96] G. McCusker. Games and Full Abstraction for FPC. To appear in Proceedings of the 11th International Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

Topic B: classical domain theory

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

[Haa96] C. Haack. A decomposition theorem for domains. Information and Computation, 124(1):62–67, 1996.

[JP95] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. In M. Main and S. Brookes, editors, 11th Conference on Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V., 1995.

[JS96] A. Jung and Ph. Sünderhauf. On the duality of compact vs. open. In S. Andima, R. C. Flagg, G. Itzkowitz, P. Misra, Y. Kong, and R. Kopperman, editors, Papers on General Topology and Applications: Eleventh Summer Conference at University of Southern Maine, Annals of the New York Academy of Sciences, 1996. To appear.

[Sch93] A. Schalk. Domains arising as algebras for powerspace constructions. Journal of Pure and Applied Algebra, 89:305–328, 1993.

[Sün95] Ph. Sünderhauf. A faithful computational model of the real numbers. Theoretical Computer Science, 1995. To appear.

Topic B: synthetic domain theory

[FMRS92] P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott. Extensional pers. Information and Computation, 98, 1992

[Hyl91] J.M.E. Hyland. First steps in Synthetic Domain Theory. In A. Carboni, M.C. Pedicchio and G. Rosolini eds, Category Theory ’90, volume 1488 of LNM, pages 131–156, 1991.

[HM95] J.M.E. Hyland and E. Moggi. The S-replete construction. In CTCS 1995, volume 953 of LNCS. Springer Verlag, pages 96–116, 1995 [Pho90] W. Phoa. Effective domains and intrinsic structure. In 5th LICS Conf.

IEEE, 1990.

[Tay91] P. Taylor. The fixed point property in Synthetic Domain Theory. In G.Kahn editor, 6th Symposium on Logic in Computer Science, Amsterdam, July 1991, pages 152–160.

Topic B: categorical domain theory

[Joh93] P.T. Johnstone, Fibrations and partial products in a 2-category. Applied Categorical Structures, 1:141-179, 1993.

[Joh94] P.T. Johnstone. Variations on the Bagdomain Theme. Theoretical Computer Science 136: 3-20, 1994.

[Vic92] S.J. Vickers. Geometric theories and databases. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, L.M.S. Lecture Notes Series no. 177. Cambridge University Press, 1992.

Topic C

[AHS95] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David Pitt, David E. Rydeheard, and Peter Johnstone, editors, Springer LNCS 953, Category Theory and Computer Science, 6th International Conference, CTCS ’95, Cambridge, UK, August 1995.

[CD93] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. to appear in Mathematical Structures in Computer Science), 1996.

[Dyb94b] Peter Dybjer. Inductive families. Formal Aspects of Computing, pages 440–465, 1994.

[Gor95] Andrew D. Gordon. Bisimilarity as a theory of functional programming. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, 1995.

[Pit94] Andrew M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124, 1994.

[Pit96] A. M. Pitts. Relational properties of domains. Information and Computation, ?:?–?, 1996. To appear.

Topic D

[ACC93] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theo. Comp. Sci., 121:9–58, 1993.

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

[FRR92a] P. Freyd, E. Robinson, and G. Rosolini. Dinaturality for free. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, L.M.S. Lecture Notes Series no. 177. Cambridge University Press, 1992.

[HO93] J.M.E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In M. Bezem, J.F. Groote (Eds), Typed Lambda Calculi and Applications, LNCS 664 (Springer-Verlag, 1993), 179-194.

[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 Computer Science and Logic, volume 92 of Contemporary Mathematics. American Mathematical Society, Providence RI, 1989.

[HR92] B.P. Hilken and D.E. Rydeheard. Towards a categorical semantics of type classes. Fund. Inf., 16:2, 1992.

[Mog91] E. Moggi. A category-theoretic account of program modules. Mathematical Structures in Computer Science, 1, 1991.

[Ros92] An exper model for Quest. In Mathematical Foundations of Programming Semantics (S. Brookes, M. Main, A. Melton, M. Mislove, D.Schmidt ed.), volume 598 of Lectures Notes in Computer Science, 1992, pag. 436–445. Springer-Verlag.

[RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In S. Abramsky, editor, Proc. 9th Symposium in Logic in Computer Science, pages 364–371, Paris, 1994. I.E.E.E. Computer Society.

Topic E

[CP92] R.L. Crole and A.M. Pitts. New foundations for fixpoint computations: Fix-hyperdoctrines and fix-logic. Information and Computation, 98, 1992.

[Mog94a] E. Moggi. A general semantics for evaluation logic. In 9th LICS Conference. IEEE, 1994.

[Mog95] E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.

[Mog96] E. Moggi. Metalanguages and applications. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 1996. To appear.

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

Topic F

[Mog91] E. Moggi. Notions of computations and monads. Information and Computation, 93:55–92, 1991.

[CM93] P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of the Conference on Category Theory and Computer Science, Amsterdam, Sept. 1993, 1993. CWI Tech. Report.

[PS93] A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdańsk, 1993, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, Berlin, 1993.

[Sta96] Ian Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1), 1996.

[Pit96] Andrew M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 1996. To appear.

Topic G

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

[BBHP93] Benton, Bierman, Hyland, de Paiva , A term calculus for Intuitionistic Linear Logic. In TLCA, LNCS 664, 1993.

[Laf95] Y. Lafont, “Interaction Combinators”, submitted to publication, available by ftp anonymous on lmd.univ-mrs.fr in pub/lafont (file combinators.ps.Z)

[JNW94] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Technical Report RS-94-7, May 1994. 42 pp. Journal version of LICS ’93 paper.

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

[WN] G.Winskel and M.Nielsen. Models for Concurrency. Appears in the Handbook of Logic in Computer Science, vol.4, Oxford University Press, 1995.

Topic H

[BBC95] S. Berardi, M. Bezem and Th. Coquand. On the Computational Content of the Axiom of Choice. TLCA Edimburgh, LNCS 902, 1995.

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

[Coq94] Th. Coquand. An Analysis of Ramsey’s Theorem. Information and Computation, Vol. 110, 1994, p. 297-304.

[Coq95] Th. Coquand. A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic, Vol. 60, 1995, p. 325-337.

[Ong96] C.-H. L. Ong. A Semantic View of Classical Proofs: Type-Theoretic, Categorical and Denotational Characterizations. To appear in Proceedings of the 11th International Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

Topic I

[ACCL91] M. Abadi, L. Cardelli, P.-L. Curien, and J. J. Levy, Explicit substitutions. Journal of Functional Programming, 1(4), 1991.

[Laf95a] Y. Lafont, “Equational reasoning with 2-dimensional diagrams”, in “Term Rewriting”, Lecture Notes in Computer Science 909, pp 170–195, Springer-Verlag, 1995.

[Laf95b] Y. Lafont, “A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)”, Journal of Pure and Applied Algebra 98, pp 229-244, 1995.

Information dissemination

[AJ94] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, 1994.

[Cro94] R. L. Crole. Categories for Types. Cambridge University Press, 1994.

[DP9?] P. Dybjer and A. M. Pitts, editors. Semantics and Logics of Computation. Cambridge University Press, 199? Based on lectures given at the CLICS-II Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge UK, September 1995.

[FJM+96] M. P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark. Domains and denotational semantics: History, accomplishments and open problems. Technical Report CSR-96-2, School of Computer Science, The University of Birmingham, 1996. 30pp., available from

http://www.cs.bham.ac.uk/.

[Ong94] C.-H. L. Ong. Correspondence between operational and denotational semantics: the full abstraction problem for PCF. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, 1994.

[Pit] A. M. Pitts. Categorical logic. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, to appear.

[Ros95] G. Rosolini. Notes on Synthetic Domain Theory. available by ftp from theory.doc.ic.ac.uk, 1995.

[Win93] G. Winskel. The Formal Semantics of Programming Languages. An Introduction. MIT Press, 1993.

Reports on research topics

This chapter consists of seven topics reports. Each report recalls the original plan for the topic (as outlined in the TA of CLICS-II) and summarizes the achievements and misses (as given in the PPRs).

1. Topic A (Sequentiality and Stability) and Topic G (Applied Linear Logic), by Samson Abramsky and Glynn Winskel

2. Topic B (Duality in Domain Theory), by Achim Jung and Martin Hyland

3. Topic C (Logic of Inductive and Recursive Data-types), Peter Dybjer

4. Topic D (Subtypes and Polymorphism in Higher Order Languages), by Giuseppe Rosolini

5. Topic E (Higher Order Modal Program Logics) and Topic F (Monadic Programming Language Semantics) by Eugenio Moggi and Andrew Pitts

6. Topic H (Computational Content of Classical Proofs) by Thierry Coquand

7. Topic I (Symbolic Computation), by Yves Lafont.

2.1 Topics A and G: Sequentiality and Stability, and Concurrency and Linear Logic

2.1.1 Objectives

The main objective of our work on sequentiality and stability was to place the work on this topic in a much richer and more adequate mathematical framework. As a specific application, we hoped to build on current research towards a definitive analysis of sequentiality in programming languages, in the framework of the classical “Full Abstraction” problem for PCF.

A major objective of the work on concurrency was to unify the highly diverse models and theories of concurrency. Much progress to this end had already been achieved in CLICS I, using the categorical approach introduced by one of the members of the consortium [WN]. The following were the specific objectives.

1. One aim was to understand concrete data structures and sequential algorithms more abstractly, and also to see how to refine concrete data structures so as to be able to model sharing.

2. We aimed to study the fine structure of the fully abstract model of PCF. Our initial idea was to do this by viewing it as a sub-model of the Scott model of all continuous functions.

3. One notable problem was to find a general way to adjoin bisimulation to categories of models for concurrency. Although Milner and Park’s traditional bisimulation on transition systems is well understood, it is much less clear how to generalise the notion to independence models like event structures and Petri nets.

4. Investigate the relation between strong stability and the traditional definition of sequentiality.

2.1.2 Results

2.1.2.1 Sequentiality

Our progress towards a definitive analysis of sequentiality exceeded our expectations. In 1993, two groups within the CLiCS project (Abramsky, Jagadeesan and Malacaria at Imperial, and Hyland and Ong at Cambridge) used game semantics to obtain the first syntax-independent descriptions of the fully abstract model for PCF. This was a goal that had eluded researchers during the previous 20 years. Comprehensive accounts of this work have now been written and submitted for journal publication [AJM95, HO95]. This advance has subsequently been extended considerably. Ong has given a categorical analsysis and fully complete game semantics for Parigot’s λμ-calculus, which gives a computational interpretation of Classical logic, thus confirming the relevance of game semantics to this topic [Ong96]. Abramsky and McCusker extended the AJM approach to recursive types [AM95a], and the lazy λ-calculus [AM95b], and McCusker has subsequently obtained full abstraction results for FPC, a rich functional language incoporating sums, products, functions and recursive types [McM96]. Also, Abramsky has significantly extended the scope of game semantics to address the issues of state and local variables, and also concurrency [Abr95]. Game semantics is having a growing impact on the semantics of programming languages; work on this topic has largely emanated from the CLiCS project. As regards dissemination, expository accounts of game semantics were given by Abramsky and Hyland at the CLiCS summer school in Cambridge in September 1995; these will appear in the proceedings of the summer school.

Some interesting connections between game semantics and abstract machines have recently been made by Danos, Herbelin and Regnier [DHR96]. This draws different strands of research together in a very promising fashion.

There was also considerable clarification of similarities and differences between game semantics and sequential algorithms on concrete data structures in a paper by Curien [Cur94]. Interestingly, one of the original technical objectives for the project, to refine concrete data structures to allow sharing to be represented, is solved in the game semantics setting as part of Abramsky’s recent work on modelling Idealized Algol. The different interpretation of the ! modality of Linear Logic in game semantics as compared with concrete data structures plays a crucial role, and is exactly what is needed to allow sharing and state to be accurately modelled.

2.1.2.2 Concurrency

The handbook chapter [WN] was completed early in the life of the project. It should be a useful reference on the various models for concurrent computation. It contains many new results, proofs and relations between models regarded as categories expressed as adjunctions. In particular it shows the models’ relationships to an operational semantics expressed using transition systems with independence structure— this was promised in the Workplan. The models dealt with and related include Mazurkiewicz trace languages, event structures, dI-domains, Petri nets, transition systems with independence, ordinary transition systems and Hoare traces.

The presentation of models for concurrency as categories begs the question of how to define equivalences like bisimulation between objects in a category—an issue raised in the Workplan. The paper [JNW94] has been accepted for a LICS93 Special issue of Information and Computation. In it an abstract definition of bisimulation is presented. The concept is based on open maps in a topos, as they appear in the work of Joyal and Moerdijk. Nielsen and Winskel have shown that the results also apply to Petri nets, an article appearing in TCS [NW], and significantly that the same bisimulation equivalence is obtained there. Preliminary ideas in [JNW94] have been significantly extended by Cattani and Winskel’s work on presheaf models for concurrency [CW]. Presheaves over pomsets for example can be seen as generalisations of event structures (the category of event structures embeds fully and faithfully into presheaves over pomsets). Such presheaf models have several technical advantages over existing models. In particular, they can be made into a bifibration which is useful in the abstract approach initiated by Winskel into weak bisimulation, based on a monad to account for the invisibility of internal actions. More generally, by results dating back to Kan’s work, presheaf models are related by naturally occurring functors which have been shown to preserve open maps by Cattani and Winskel [CW]—a very useful general result. An early suspicion that the new presheaf models supported “refinement” operators e.g. of the kind treated in [DGR92], has been formally confirmed in the results of Cattani (PhD student of Winskel); for example, the refinement of event structures by finite pomsets (wellknown from the work of van Glabeek and others) appears especially simply as the restriction of a general construction on presheaves. Work is continuing on extending presheaf models to higher order, including late value passing and process passing [Win96].

There has been work on control structures (joint work between C. Hermida (Aarhus) and A.J. Power (Edinburgh)). Progress has been made towards a categorical refinement of Milner’s work on action/control structures, which recast the main ideas of this latter in a more traditional categorical logic framework, using fibrations with structure. The emphasis is placed upon a purely categorical account of the manipulation of ‘names’ within actions (or processes), while keeping a precise correspondence with Milner’s original and current work.

2.1.2.3 The MacLane Conjecture

A highlight has been Sergei Soloviev’s proof of a long open conjecture of Saunders Mac Lane. In detail, Soloviev provides sufficient conditions on a symmetric monoidal closed (SMC) category C such that a diagram in the free SMC category, generated by the set of atoms, commutes iff all its interpretations in C are commutative. In particular, the category of vector spaces on any field I satisfies these conditions (in the original Mac Lane conjecture only this case was considered). Soloviev’s proof hinges on the reformulation of categorical properties in terms of the proof theory of linear logic: Instead of diagrams pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent iff all their interpretations in C are equal. Taking into account a mistake in the R.Voreadou’s proof of the “abstract coherence theorem”, found by Soloviev, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of the Mac Lane conjecture proves also correctness of the modified description. The paper has been submitted to “Annals of Pure and Applied Logic”, with extended abstract appearing in the proceedings of CTCS-6, Cambridge, 1995 (see [Sol]).

2.1.2.4 Strong stability

The work on strong stability has been motivated by the wish to capture sequentiality directly at the level of functions, without moving to the more intensional models like sequential algorithms or games. Early in the project, Ehrhard showed that strongly stable functions were the extensional collapse of sequential algorithms, a result securing strong stability as an important notion, backed up by Ehrhard and Colson’s paper [Col94].

Another tack holds promise for producing directly extensional models of PCF, and hopefully of the fully abstract model of PCF. Bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other output in the behaviour of functions. In [PW94], bistructures form a categorical model of Girard’s classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry’s bidomains. The use of bistructures in modelling PCF, and the theory on PCF terms induced, are studied in [Win94]. In this, the stable case, there are close connections with earlier work of Ehrhard and Bucciarelli. Bistructures have broader potential however. In particular, by incorporating the work of Ehrhard on hypercoherences, they extend to sequentiality. A journal paper is being prepared jointly by Curien, Plotkin and Winskel.

It is noteworthy that all the approaches to categories of domains and their representations are informed by ideas from linear logic; the cartesian closed categories are obtained from more primitive linear categories modelling linear logic.

2.1.2.5 Interaction Nets

Yves Lafont has pursued his work on Interaction Nets, a model of concurrency inspired by Linear Logic. For instance, recently, he has introduced a very simple system of Interaction Combinators with only 3 symbols and 6 rules, which is universal in a strong sense: any other interaction system can be translated into it, and this translation preserves the complexity of computation as well as the degree of parallelism. This system has a nice interpretation in terms of stack machines, which is analogous to the Geometry of Interaction for Linear Logic. All this is explained in [Laf95], which has just been submitted to publication.

2.1.3 Conclusions

Looking back over the project several areas seem important and likely to have a lasting strong influence on the semantics of computation. Certainly game semantics through its deep connection with logic, sequentiality and full abstraction shifts our perspective and understanding of programming languages. We have a deeper understanding of sequentiality through the work on strong stability, and possibly more is to be uncovered in the work on bistructures. New paradigms of computation come to life in the implementation of interaction nets. The abstract way of presenting bisimulation via open maps and its tie in with presheaf models holds promise of unifying concurrency with more traditional domain theory, and could be very influential. Substantial effort during the project went into producing tutorial material on the techniques and methodologies developed under this Topic of the project, and in particular for the book for the CLICSII Summersdchool at the Newton Institute, Cambridge.

2.1.4 References

[AJM95] S. Abramsky, R. Jagadeesan and P. Malacaria. Full Abstraction for PCF. 60 pages. Submitted for publication, 1995.

[HO95] M. Hyland and C.-H. L. Ong. On Full Abstraction for PCF. 130 pages. Submitted for publication, 1995.

[Abr95] S. Abramsky. A Game semantics for Idealized Algol. Lecture at Linear Logic Workshop, Isaac Newton Institute, Cambridge, November 1995.

[AM95a] S. Abramsky and G. McCusker. Games for Recursive types. In Proceedings of Theory and Formal Methods Workshop, ed. C. Hankin, Imperial College Press, 1995.

[AM95b] S. Abramsky and G. McCusker. Games and Full Abstraction for the Lazy λ-calculus. Proceedings of 10th International Symposium on Logic in Computer Science, IEEE Computer Society Press, pages 234–243, 1995.

[McM96] G. McCusker. Games and Full Abstraction for FPC. To appear in Proceedings of the 11th International Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

[DHR96] V. Danos, H. Herbelin and L. Regnier. Game Semantics and Abstract Machines. To appear in Proceedings of the 11th International Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

[Ong96] C.-H. L. Ong. A Semantic View of Classical Proofs: Type-Theoretic, Categorical and Denotational Characterizations. To appear in Proceedings of the 11th International Symposium on Logic in Computer Science, IEEE Computer Society Press, 1996.

[Cur94] P.-L. Curien. On the Symmetry of Sequentiality. In Proccedings of the International Workshop on Mathematical Foundations of Programming Language Semantics. Springer Lecture Notes in Computer Science 1994.

[Col94] L. Colson and T.Ehrhard. On strong stability and higher order sequentiality. IEEE proceedings of LICS’94, 1994.

[DGR92] P. Degano, R. Gorrieri, and G. Rosolini. A categorical view of process refinement. In J. de Bakker, G. Rozenberg, and J. Rutten, editors, Proc. REX Workshop on Semantics: Theory and Applications, volume 666 of Lecture Notes in Computer Science, pages 138–154. Springer-Verlag, 1992.

[CW] G-L. Cattani and G.Winskel. Presheaf models for concurrency. In preparation.

[JNW94] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Technical Report RS-94-7, May 1994. 42 pp. Journal version of LICS ’93 paper.

[Laf95] Y. Lafont, “Interaction Combinators”, submitted to publication, available by ftp anonymous on lmd.univ-mrs.fr in pub/lafont (file combinators.ps.Z)

[WN] G.Winskel and M.Nielsen. Models for Concurrency. Appears in the Handbook of Logic in Computer Science, vol.4, Oxford University Press, [NW] M.Nielsen and G.Winskel. Petri Nets and Bisimulations. January

1995. Appears in TCS. (ftp.daimi.aau.dk) (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/4/BRICS-RS-95-4.ps.gz)

[PW94] Gordon Plotkin and Glynn Winskel. Bistructures, bidomains and linear logic. Technical Report RS-94-9, May 1994. 16 pp. Appears in the proceedings of ICALP ’94, LNCS, 1994.

[Sol] S.Soloviev. Proof of a S.Mac Lane conjecture. Submitted to ”Annals of Pure and Applied Logic”, extended abstract published in the Proceedings of CTCS-6, Cambridge, 1995.

[Win94] Glynn Winskel. Stable bistructure models of PCF. Technical Report RS-94-13, May 1994. 26 pp. Preliminary draft. Invited lecture for MFCS ’94. To appear in the proceedings of MFCS ’94, LNCS, 1994.

[Win96] Glynn Winskel. Presheaf models for value passing. In preparation.

2.2 Topic B: duality in domain theory

The proposal for this project featured two areas in Classical Domain Theory which at the time seemed to warrant further attention, the problem of developing a duality theory for stable functions and the extension of domain theoretic concepts to continuous domains. It turned out that these were not the only worthwhile topics and indeed, Classical Domain Theory proved to be a rich source for deep and mathematically elegant results. While these are reported in detail below, we mention here also the completion of a major reference work on Domain Theory by Abramsky and Jung, [AJ94], published as a chapter in the Handbook of Logic in Computer Science. The project proposal also highlighted two distinct directions in which it seemed profitable to extend the ideas of Classical Domain Theory: Synthetic Domain Theory and Categorical Domain Theory. Both these areas developed in ways which would have been hard to predict.

2.2.1 Classical Domain Theory

2.2.1.1 Categories of domains

One substantial contribution of the project is represented by Andrea Schalk’s work on power domains, which is a further attack on the classical problem of nondeterminacy. The idea is to subject the standard power domain constructions to a fresh analysis by looking at them in different categories (dcpos, topological spaces, locales). The approach builds on earlier investigations in particular of Winskel [Win85] and Robinson [Rob88]. In [Sch93c] it is shown that the standard Hoare power domain goes through uniformly in all cases. However even the Smyth power domain leads to more than one generalisation (see [Sch93b] and [Sch93a]).

A second line of research in this area has been the study of linear categories of domains. Linear logic was identified as an important technical tool in the original proposal. In the context of traditional (Scott and stable) domain theory, it has been studied by Paul Taylor at Imperial, and this theme has been developed further. Huth [Hut95b] took as starting point the cartesian closed category of prime-algebraic domains [Win88], a proper full subcategory of Scott-domains. There is a simple monad on a symmetric monoidal closed category PRIME of distributive Scott-domains whose Kleisli category is a cartesian closed category of prime-algebraic domains. Further, PRIME is the greatest such category with distributive Scott-domains as objects [Hut95b]. Extensions of such results to all Scott domains present problems.

For example, the function space A_{2}−^{∘}A_{2} of the Scott-domain A_{2} in [Hut94] is not a Scott-domain (not even continuous!). However, Scott-domains are exactly those bounded complete domains where the identity is approximated by Scott-continuous projections with finite image. So we can call a domain linear [Hut94] if these functions can be chosen to preserve all existing (not only all directed) suprema. We thus obtain a symmetric monoidal closed category LIN which properly contains PRIME as a full subcategory; an object in PRIME is nothing but a distributive linear domain [Hut94]. Therefore, it is indeed possible to extend the linear types beyond the prime-algebraic setting such that it even encompasses all finite objects and that colimits of ω-chains of projection-embedding pairs exist.

We have been investigating the maximality of such denotational universes (cf. the corresponding maximality problems and results in the case of cartesian closed categories [Smy83, Jun89]). Previous techniques are no longer suitable; the reason being that one has a full reflective ∗-autonomous [Bar79] subcategory LL in LIN whose objects are all linear domains with a top. The self-duality of LL turned out to be the vital mechanism for arguing about the linear types in LIN and its inherent symmetry is a feature which is absent in the cartesian closed categories and, consequently, in the methods used in [Smy83, Jun89]. The study of LL culminated in the papers [HJK94b, HJK94a]. In fact, the entire theory could be extended to continuous lattices and resulted in the ∗-autonomous category LFS of linear FSlattices which combined the concept of finitely separated functions in [Jun90] with that of a linear lattice in [Hut94]. The category LL is just that of all algebraic linear FS-lattices.

A fascinating topological symmetry is the coincidence of the Lawson topologies λ(A) = λ(A^{⊥}) for all objects A in LFS; this gives rise to a duality between the lifted lower powerdomain of A and the lifted upper powerdomain of A^{⊥}; the latter being an isomorphic copy of ?(A), the DeMorgan dual of !(A). It is very pleasing to see that the mere imposition of a notion of approximation, i.e. continuity of the considered lattices, renders such a clearcut topological explanation of the modality ?(A) within the category LFS. Finally we can show that LFS is the greatest ∗-autonomous full subcategory of SUP (the usual category of sup lattices) such that every object is bicontinuous with a symmetric Lawson topology as above. In that sense it is the greatest possible semantic universe of Scott-domains if we insist on the extensional order and symmetry.

Together with Michael Mislove, Michael Huth has characterised linear FS-lattices and completely distributive lattices through their spaces of self-maps. The results are the following:

Theorem. A continuous lattice is a linear FS lattice (completely distributive lattice) if and only if its function space of sup-preserving self-maps is a Scottcontinuous (linear) projection of its function space of Scott-continuous self-maps.

This is remarkable because it gives a high-level description of these two concepts completely avoiding the the technicalities of the usual definitions. The result is contained in the technical report [HM94].

More recently, Michael Huth ([Hut95a]) was able to prove that the algebraicity of the space of sup-preserving self-maps already implies that the lattice is linear. A similar theorem was contained in [HJK94a] but there we needed to assume that the Lawson topology on the lattice was linked. This condition is rather hard to motivate from a computational point of view and it is major step that Huth was able to dispense with it. The proof uses completely new techniques and apparently works only for algebraic lattices rather than continuous ones. More research is needed to place this into context.

2.2.1.2 Stability and bidomains

The notion of strong stability was introduced by Bucciarelli and Ehrhard in their article [BE91b] as an alternative approach to sequentiality. In the models they build, programs (or proofs) are still interpreted by functions, as in the continuous or stable model in contrast with what happens with the models of sequential algorithms or games where the interpretations of programs contain a lot of information about their internal behaviour. The basic observation is that sequentiality of first order functions can be expressed as a preservation property based on a notion of linear coherence: f is sequential if and only if it sends linearly coherent sets to linearly coherent sets and preserves meets of linearly coherent sets. This approach extends to higher order functions and gives rise to a cartesian closed category of dI-domains with coherence. In order to compare this approach with the usual Scott model of PCF, Bucciarelli and Ehrhard constructed a further category where the (dI-)domains are embedded in a Scott domain. As with Berry’s notion of bidomain, some nonextensional behaviour is ruled out, and it turns out that the equational theory of this model equates more terms than the equational theory of the Scott’s model. This construction is presented in [BE91a] and [BE94].

Refining these ideas, Ehrhard has shown that a sufficiently large class of qualitative domains equipped with coherence can be described in terms of ‘hypercoherences’: a hypercoherence is a pair X = (|X|, ΓX), where |X| is a set and ΓX is a set of finite and non-empty subsets of |X| which contains all singletons (that is an unlabelled, unoriented and reflexive hypergraph). These new objects also give rise to a new model of linear logic, and are described in [Ehr93]. Bucciarelli has extended the hypercoherence approach to dI-domains with coherence using a notion of ‘hypercoherent event-structures’. This is a first step in the direction of a theory of “strongly stable domains”. This work is presented in [Buc93].

Finally, Ehrhard has compared the strongly stable model of PCF with the model of sequential algorithms. He used an “abstract” theory of sequential algorithms that he had previously set up with Bucciarelli ([BE]). In [Ehr] he has shown that any strongly stable function is the “extensional content” of a sequential algorithm; thus even at higher order, strong stability corresponds to a notion of sequentiality. We regard this result as telling evidence of the importance of the theory of strong stability.

Innovative work by Plotkin and Winskel has extended our understanding of an approach to domains in which both the extensional and a more intensional (computational) order are taken as basic. Bistructures are a generalization of event structures to represent spaces of functions at higher types. In place of the partial order of causal dependency, one has two orders, associated respectively with input and output behaviour. Bistructures give a representation of Berry’s bidomains. This representation can itself be considered the result of a linear decomposition. Bistructures give a categorical model of linear logic (a linear category plus suitably structured comonad). The corresponding Kleisli category is equivalent to a cartesian closed subcategory of Berry’s bidomains.

A main motivation for bidomains came from the full abstraction problem for the functional language PCF. However, although the bidomain model incorporates both the Berry stable and Scott extensional order, its PCF theory is incomparable with that induced by the Scott model. By incorporating the idea of a conflict relation, Winskel obtained a new model of PCF without this inadequacy. This research is described in [Win94].

In bistructures we intend to combine continuity and stability, so as to get a very tight correspondence between language and model. Surprisingly enough, by slightly changing the definition one gets a concept which encompasses both all dI-domains and all Scott-domains. Following up initial research by Lamarche, this has been fully carried out by Kegelmann [Keg95b, Keg95a].

2.2.1.3 Probabilistic computation

As proposed in the workplan we have worked on a setting for probabilistic power domains. Kirch’s thesis [Kir93], supervised within the project by Keimel, presents a simple ‘functional analytic’ framework, in which a version of the Riesz representation theorem plays a role. This was further refined in the thesis by Tix [Tix95]. Power domains are also involved in Sünderhauf’s work on quasi-uniform spaces [Sün95b] and [Sün95a] which builds on work of Smyth [Smy94].

In [Str95], Strüder approaches the probabilistic powerdomain from an algebraic angle. While it was well known that the construction yields a free algebra for a certain theory, it was not clear what the general principles for such free algebras are. Based on the results in [AJ94], she has proved a very general free algebra theorem for continuous domains. The main new feature is that in her setting the set of operations is also ordered. To our surprise, it turned out that the general theory is not directly applicable to the probablilistic powerdomain, but needs a particular extra step (a retraction). This makes it quite clear why the theory of this powerdomain construction is so much more difficult than that of the classical powerdomains. As a second application she shows how to construct free continuous prelocales.

Major progress was made in our programme to develop a “Domain Theory in Logical Form” for continuous domains which was one of our main objectives in the workplan. Achim Jung together with Philipp Sünderhauf [JS95a, JS95b] has set up a list of axioms which define a continuous analogue of Abramsky’s “prelocales”. The big surprise was that the axioms can be chosen to be completetly symmetric with respect to disjunction and conjunction even though the lattice of open sets will usually not satisfy these axioms. In order to define a prelocale from a coherent space one takes pairs of opens and compacts rather than just opens. The advantage of the symmetric approach is that one derives easily and uniformly space, lattice of opens and lattice of compacts from a prelocale. Free constructions (in the style of [AJ94]) also preserve the symmetry. These results confirm in a very convincing fashion our view that by studying the world of continuous domains one can get a deeper insight into the workings of domain theory.

2.2.1.4 Static datatypes

With static datatypes we mean ordered algebraic structures which derive from datatype definitions not involving the function space operator. The prime example is the datatype relational database. Jung and Puhlmann have been considering the snack powerdomain construction which provides a promising model. Their results are reported in [JP95, Puh95a, Puh95b].

When trying to apply the ordered theory of relational databases one would like to employ existing programs for the ordinary theory. To be able to do so we have studied ways to decompose domains into flat domains. This already arose in [BJO91], and was first addressed in [JLP91]. In [Haa93] Haack has thoroughly investigated lax limits in the (order enriched) category of domains, and has obtained a good decomposition result [Haa95]. A new rather small cartesian closed category of domains emerges from this work.

2.2.2 Synthetic and Generalised Domain Theory

Our main efforts in Synthetic Domain Theory (SDT) diverged from those envisaged in the project proposal. First we had expected to work on SDT in connexion with stable domain theory and sequentiality (Topic A). Though we did work on axioms and models for synthetic stable domain theory, this line was absorbed by a more general approach of providing models which connect SDT with Classical Domain Theory (Topic B-1). Secondly we had expected that Duality which plays an important part in our understanding of Classical Domain Theory would be the key to progress. However there was little progress on this front, and what there has been (some simple abstract observations by Hyland and a deeper approach by Taylor [Tay95]) remains unpublished.

The main goal of Synthetic Domain Theory is to bridge the gap between categories of domains, which provide adequate models for programming languages, and set-theoretic universes, where type-theory and logic are interpreted. In this way one would like to obtained a viable framework for the practice of Denotational Semantics and Program Logics. The preliminary ideas of project members in this area were discussed at the first Workshop on Evaluation Logic and Synthetic Domain Theory. The main problems were identified, and subsequent work has been closely related to that on the original Topic E. Hence, as mentioned in the First Year Report, the focus in SDT has been on providing a foundational background for applications.

Where it has not otherwise been published, our work on SDT has been publicised on the SDT bulletin board set up by Paul Taylor in the course of the first year of the project.

Characterising Categories of Domains In work predating the project Hyland [Hyl90] had presented the first set of properties for an object Σ of an elementary topos on the basis of which it was possible to develop (pre)domain theory as the theory of the replete objects: an object X is replete if, whenever Σ^{f} : Σ^{B} → Σ^{A} is iso, then X has the unique extension property with respect to f, i.e. for every α : A → X there is a unique β : B → X such that β ∘ f = α. Objects characterised by such orthogonality conditions automatically have good closure properties, and for this reason a characterisation of predomains as replete objects remains at the core of our approach. This characterisation was studied in depth in the project, and an account of a general fibrational setting is in [HM95].

Impact of Axiomatic Domain Theory Axiomatic Domain Theory is concerned with axiomatisations of traditional categories of domains. These axiomatisations should be consistent with known categories, and provide structural requirements for new semantic categories. A major step was taken by Peter Freyd (see [Fre90]), who discovered an appropriate abstract universal property of the solutions of domain equations. This discovery spurred research, in particular in Edinburgh, toward an axiomatic presentation of categories of domains (see [Sim92, Fio94, FP94]). In the project, Freyd’s axiomatic presentation was related to properties of Σ to give synthetic versions of the standard theory of domains (see [RS94, Ros95]). This work indicates that the full power of the infinitary side of domain theory can be captured in SDT by requiring simple properties of Σ sufficient to set up Freyd’s analysis. A detailed analysis of this point of view together with other fundamental material on the replete construction is given by Rosolini [Ros95]. It follows from this work that different versions of SDT should be distinguished by their finitary axioms.

Finitary axioms We have considered finitary axioms from two angles: to distinguish between different flavours of domain theory, and with a view to getting a smooth theory. Work of the first kind is closely related to work comparing SDT with Classical Domain Theory (see below). Our other work has focused on properties of the (Σ-epi, Σ-extremal mono) factorization system in the category of replete objects. For example, we considered the following statements:

A If m is regular mono then Σ^{m} is epi.

B If Σ^{e} is mono then Σ^{e} is Σ-extremal mono.

C All Σ-extremal monos are regular.

D The repletion has an algebraic description (cf discussion above).

E The functor Σ^{Σ^{(−)}} preserves regular monos (cf discussion above).

We know that (i) A entails C, (ii) C entails D, and (iii) A and B together entail E. We have many satisfactory models in which A holds. We have not been able to do much better with realisability models, but conjecture that we have better models in the case of Grothendieck toposes. Going further Paul Taylor [Tay95]identified additional axioms which ensure stronger properties of regular monos in categories of replete objects, for example (as required for a naive interpretation of Evaluation Logic see below) that Σ^{m} is a regular epi when m is a regular mono.

Comparison with Classical Domain Theory Our approach has been to construct toposes of sheaves in which some (fragment of a) category of domains embeds fully and faithfully. So there is a Scott topos which reflects much of the usual style of domain theory, and a variety of toposes reflecting versions of stable domain theory. These models provide conservative extension results, and make a good comparison with traditional approaches to domaintheory. In addition they give a hint as to how to axiomatise flavours of domain theory. (Unfortunately we are not able to characterise the replete objects in these models in a way which ties up with Classical Domain Theory.)

Evaluation Logic and SDT In the workshop on Evaluation Logic and Synthetic Domain Theory, we decided to investigate computational monads which seemed particularly problematic for interpreting Evaluation Logic (according to the semantics proposed in [Mog93b]) over particular models for SDT. A typical problem is that in the category of cpos both the monad of continuations Σ^{(Σ^{X})} and that of Plotkin’s powerdomain P_{p}(X_{⊥}) do not preserve regular monos (which correspond to inductive subsets, and so are the obvious candidate for interpreting a LCF-like logic). [Mog93a] tries to overcome these problems for Evaluation Logic, by replacing cpos with replete objects in the category of filter spaces. However, we have only established some partial results about this model, namely:

• SFP forms a full subcategory of the category of replete objects;

• a characterisation of the regular subobjects in replete objects of an SFP

• m : X̄ → Ȳ regular mono implies Σ^{m} regular epi, provided Ȳ is a topological space (cf discussion below).

2.2.3 Categorical Domain Theory

The aim of this area of our work was to move beyond the ‘topological’ or poset case and develop a theory of domains as categories (as opposed to spaces) of points. Here the points are to be thought of as the models of a suitably restricted kind of theory, and the passage from posets to categories amounts to the passage from propositional to predicate logic. We were originally motivated by the possible implications for specification languages, and the desire to provide clean semantics for them. Clear justification for this approach is now provided by the specific applications to building models for databases (via bag domains) envisaged by Vickers [Vic92].

The project succeeded in producing significant mathematical work providing foundations for the specific applications of topos theoretic models pioneered in [Vic92] for specific cases of the ‘bag domain’. It turns out to be a non-trivial exercise to establish proper foundations for a general theory of bag domains; such a theory involves a number of categorical subtleties. This more foundational work is described in Johnstone [Joh93]. In addition, following on from the papers of Vickers [Vic92] and Johnstone [Joh92], a number of potentially useful variations on the idea ‘domains of subcollections’ have been considered. A survey of work so far is given in Johnstone [Joh94]. There remains much to do; for example, it should be possible to consider the snack powerdomain from this point of view. These innovations were not predicted in the work plan, and testify to the fertility of the general idea of generalising Domain Theory.

On a wider front, we had intended to use topos theoretic analogues of domain theory as the basis for the semantics of a specification language. The main success of the project in this area was the use of categorical logic to internalize classifying categories of domains and their generalisations, and hence to establish the existence of a relatively cartesian closed category arising from ‘Scott Theories’. This line of work foundered after the first year, when the main researcher (Badenhorst) left Cambridge, and it proved impossible to find anyone with the relevent interests to take things further. Unfortunately the account of the research in the current version of Badenhorst’s Cambridge dissertation [Bad95] is flawed; a more satisfactory presenation is in preparation. On the positive side, the general approach of the project have been taken up by Lano (Imperial College) and Fiadeiro (Lisbon) in work on the semantics of specification languages.

[AJ94] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1994.

[Bad95] G. Badenhorst. Scott Toposes. Ph.D. Dissertation, University of Cambridge, submitted 1995.

[Bar79] M. Barr. ∗-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer Verlag, 1979.

[BE] A. Bucciarelli and T. Ehrhard. A theory of sequentiality. Theoretical Computer Science. To appear.

[BE91a] A. Bucciarelli and T. Ehrhard. Extensional embedding of a strongly stable model of pcf. In J. Leach Albert, B. Monien, and M. Rodriguez Artalejo, editors, Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science. Springer Verlag, 1991.

[BE91b] A. Bucciarelli and T. Ehrhard. Sequentiality and strong stability. In 6th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[BE94] A. Bucciarelli and T. Ehrhard. Sequentiality in an extensional framework. Information and Computation, 110(2):265–296, 1994.

[BJO91] P. Buneman, A. Jung, and A. Ohori. Using powerdomains to generalize relational databases. Theoretical Computer Science, 91:23–55, 1991.

[Buc93] A. Bucciarelli. Sequential models of PCF: some contributions to the domain-theoretic approach to full abstraction. PhD thesis, Universitá di Pisa, 1993.

[Ehr] T. Ehrhard. Projecting sequential algorithmes on strongly stable functions. Annals of Pure and Applied Logic. To appear.

[Ehr93] T. Ehrhard. Hypercoherences: A strongly stable model of linear logic. Mathematical Structures in Computer Science, 3:365–386, 1993.

[Fio94] M. Fiore. Axiomatic Domain Theory in categories of partial maps. Ph.D. Dissertation, University of Edinburgh, 1994.

[FP94] M. Fiore and G.D. Plotkin. An axiomatisation of Computationally Adequate Domain Theoretic Models of FPC. In S. Abramsky ed. 9th Symposium on Logic in Computer Science, Paris, July 1994, pages 92–102.

[Fre90] P. Freyd. Algebraically compact categories. In A. Carboni, M.C. Peddichio and G. Rosolini eds, Category Theory, volume 1488 of LNM, pages 95–104.

[Haa93] C. Haack. Die Hyperlimeskonstruktion, 1993. Technische Hochschule Darmstadt. Diploma thesis, 86 pp.

[Haa95] C. Haack. A decomposition theorem for domains. Accepted for publication in Information and Computation., 1995.

[HJK94a] M. Huth, A. Jung, and K. Keimel. Linear types and approximation. submitted to the Journal of MSCS, 1994.

[HJK94b] M. Huth, A. Jung, and K. Keimel. Linear types, approximation, and topology. In Logic in Computer Science, pages 110–114. IEEE Computer Society Press, 1994.

[HM94] M. Huth and M. Mislove. A Characterization of linear FS-lattices. Technical Report 1679, Technische Hochschule Darmstadt, September 1994.

[Hut94] M. Huth. Linear Domains and Linear Maps. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 438–453. Springer Verlag, 1994.

[Hut95a] M. Huth. The Greatest Symmetric Monoidal Closed Category of Scottdomains. Technical Report 1734, Technische Hochschule Darmstadt, May 1995.

[Hut95b] M. Huth. Zero Dimensional and Connected Domains. Semigroup Forum, 51:63–71, 1995.

[Hyl90] J.M.E. Hyland. First steps in Synthetic Domain Theory. In A. Carboni, M.C. Peddichio and G. Rosolini eds, Category Theory, volume 1488 of LNM, pages 131–156.

[HM95] J.M.E. Hyland and E. Moggi. The S-replete construction. In CTCS 1995, volume 953 of LNCS. Springer Verlag, pages 96–116.

[Joh92] P.T. Johnstone. Partial products, bagdomains and hyperlocal toposes. In Applications of Categories in Computer Science, L.M.S. Lecture Notes Series no. 177 (Cambridge University Press, 1992), 315–339.

[Joh93] P.T. Johnstone, Fibrations and partial products in a 2-category. Applied Categorical Structures, 1:141-179, 1993.

[Joh94] P.T. Johnstone. Variations on the Bagdomain Theme. Theoretical Computer Science 136: 3-20, 1994.

[JLP91] A. Jung, L. Libkin, and H. Puhlmann. Decomposition of domains. Technical Report 1416, Technische Hochschule Darmstadt, 1991.

[JP95] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. In M. Main and S. Brookes, editors, 11th Conference on Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V., 1995.

[JS95a] A. Jung and Ph. Sünderhauf. On the duality of compact vs. open. In B. Flagg and R. Kopperman, editors, Proceedings of the 11th Summer Conference on Topology and Applications. New York Academy of Sciences, 1995.

[JS95b] A. Jung and Ph. Sünderhauf. Uniform approximation of topological spaces. Manuscript, 1995. 20pp.

[Jun89] A. Jung. Cartesian Closed Categories of Domains, volume 66 of CWI Tracts. Centrum voor Wiskunde en Informatica, Amsterdam, 1989.

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

[Keg95a] M. Kegelmann. Factorisationsystems on domains. Extended Abstract, 1995.

[Keg95b] M. Kegelmann. Faktorisierungssysteme auf Bereichen. Master’s thesis, Technische Hochschule Darmstadt, September 1995. 63pp.

[Kir93] O. Kirch. Bereiche und Bewertungen. Master’s thesis, Technische Hochschule Darmstadt, June 1993. 77pp.

[Lon95] J.R. Longley. Realizability Toposes and Language Semantics. Ph.D. thesis, University of Edinburgh, 1995.

[Mog93a] E. Moggi. A note on sdt in filter spaces. Internal report available via FTP from theory.doc.ic.ac.uk, 1993.

[Mog93b] E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, to appear.

[Pho94] W.K.-S. Phoa. From term models to domains. Inf. Comp., 109:211–255, 1994.

[Puh95a] H. Puhlmann. Die Snack-Potenzkonstruktion: Grundlage einer Semantik genesteter Datenbanken. PhD thesis, Technische Hochschule Darmstadt, July 1995. 88pp.

[Puh95b] H. Puhlmann. Re-grouping information in a domain theoretic data model. Preprint, Technische Hochschule Darmstadt, October 1995. 27pp.

[Rob88] E. Robinson. Logical aspects of denotational semantics. In Summer Conference on Category Theory and Computer Science, Edinburgh, 7th– 9th September 1987, Lecture Notes in Computer Science. Springer Verlag, [RS94] B. Reus and T. Streicher. Naïve Synthetic Domain Theory. manuscript,

1994.

[Ros92] An exper model for Quest. In Mathematical Foundations of Programming Semantics (S. Brookes, M. Main, A. Melton, M. Mislove, D.Schmidt ed.), volume 598 of Lectures Notes in Computer Science, 1992, pag. 436–445. Springer-Verlag.

[Ros95] G. Rosolini. Notes on Synthetic Domain Theory. available by ftp from theory.doc.ic.ac.uk, 1995.

[Sch93a] A. Schalk. Algebras for Generalized Power Constructions. Doctoral thesis, Technische Hochschule Darmstadt, 1993. 174 pp.

[Sch93b] A. Schalk. Domains arising as algebras for powerspace constructions. Journal of Pure and Applied Algebra, 89:305–328, 1993.

[Sch93c] A. Schalk. The Hoare power construction for domains, topological spaces and locales. Technical Report 1549, Technische Hochschule Darmstadt, 1993. 33 pp.

[Sim92] A.K. Simpson. Recursive Types in Kleisli Categories. available by ftp from theory.doc.ic.ac.uk, 1992.

[Smy83] M. B. Smyth. The largest cartesian closed category of domains. Theoretical Computer Science, 27:109–119, 1983.

[Smy94] M. B. Smyth. Completeness of quasi-uniform and syntopological spaces. Journal of the London Mathematical Society, 49:385–400, 1994.

[Str95] C. Strüder. Stetige Operationen auf kontinuierlichen Bereichen. Master’s thesis, Technische Hochschule Darmstadt, April 1995. 38pp.

[Sün95a] Ph. Sünderhauf. Constructing a quasi-uniform function space. Topology and its Applications, 1995. To appear.

[Sün95b] Ph. Sünderhauf. Quasi-uniform completeness in terms of Cauchy nets. Acta Mathematica Hungarica, 69(1–2):47–54, 1995.

[Tay91] P. Taylor. The fixed point property in Synthetic Domain Theory. In G.Kahn editor, 6th Symposium on Logic in Computer Science, Amsterdam, July 1991, pages 152–160.

[Tay95] P. Taylor. An abstract Stone duality. available by ftp from

theory.doc.ic.ac.uk, 1995.

[Tix95] R. Tix. Stetige Bewertungen auf topologischen Räumen. Master’s thesis, Technische Hochschule Darmstadt, June 1995. 51pp.

[Vic92] S.J. Vickers. Geometric theories and databases. In Applications of Categories in Computer Science, L.M.S. Lecture Notes Series no. 177 (Cambridge University Press, 1992), 288–314.

[Win85] G. Winskel. A complete proof system for SCCS with modal assertions. In S. N. Maheshwari, editor, Foundations of Software technology and Theoretical Computer Science, volume 206 of Lecture Notes in Computer Science, pages 392–410. Springer Verlag, 1985.

[Win88] G. Winskel. An introduction to event structures. In J. W. de Bakker, editor, Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 364–399. Springer Verlag, 1988.

[Win94] G. Winskel. Stable bistructure models of PCF. Technical Report RS-94-13, BRICS, 1994.

2.3 Topic C: logic of inductive and recursive datatypes

2.3.1 Summary

The collaborating partners on this topic are Aarhus, Cambridge, Chalmers, Darmstadt, and Manchester.

2.3.2 Objectives

This topic was intended to contribute 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) were well established and we have sought to establish similar principles for wider classes of recursively defined types and also to integrate these priniciples into formal program logics.

The objectives can be divided into three subtopics:

1. Inductive types and the logic of total, well-founded objects, especially Martin-Löf Type Theory.

2. Coinductive types and the logic of infinite, non-wellfounded objects, especially non-standard extensions of Martin-Löf Type Theory.

3. Recursive types and the logic of general recursive functional programs, especially in the tradition of Scott’s Logic of Computable Functions (LCF).

A principal tool has been the categorical modelling of inductive types as initial algebras, of coinductive types as final coalgebras, and of recursive types as objects which are simultaneously initial algebras and final coalgebras. Topic C has therefore provided a natural continuation of the work in CLICS-I on categorical models of dependent type theories.

In the Work Plan we predicted that work on Topic C would be limited to the first two years of the project. However, the work on applications under the first subtopic (inductive types) developed into several new subtopics of independent interest: Internal Type Theory, reduction-free normalization, coherence problems for Type Theory, and formalization of Category Theory in Type theory. Moreover, the more abstract investigations of coinduction proposed in the Work Plan were followed by work which focussed on applications to programming. These new directions were actively pursued also during the third year of the project.

2.3.3 Results

2.3.3.1 Inductive Types

Simultaneous induction-recursion. A general schema for inductive definitions which included universes and other reflection principles were developed by Dybjer [Dyb94a]. The crucial idea was to generalize Martin-Löf’s universes à la Tarski to a general notion of simultaneous inductive-recursive definition. This schema gave a uniform explanation of several constructions, such as Griffor and Palmgren’s [Pal91] internal universe hierarchies and super universes and Martin-Löf’s computability predicates used for a normalization proof of Type Theory [ML72], and that it also provided a Type-Theoretic counterpart of Aczel’s Set-Theoretic construction of Frege Structures [Acz80].

Realizability models. Dybjer [Dyb94a] gave a realizability model for the theory of simultaneous inductive-recursive definition. Yuxi Fu extended Beeson’s realizability model for Type Theory to the case of inductive types [Fu92]. He also showed that the strictness conditions for inductive types can be dropped when modelling types in this way.

Internal Type Theory. One goal of the work on simultaneous induction-recursion was to define syntax and models of Type Theory in a suitable extension of itself. We hoped for example to formulate both a “standard” model and a model of normal forms in type theory itself. For this purpose we needed to develop several topics of independent interest: reduction-free normalization; categorical models of Type Theory and coherence problems; and the representation of Category Theory in Type Theory.

Reduction-free normalization. An elegant way to prove normalization of Type Theory in an extension of itself was provided by Martin-Löf [ML75a, ML75b] – “normalization by intuitionistic model construction”. T. Coquand and Dybjer [CD93] used these ideas to formalize inside Type Theory normalization for a combinatory formulation of Gödel System T with transfinite types. They also discussed algebraic aspects and pointed to the connection with the work of Lafont [Laf88] on glueing. C. Coquand [Coq93] developed a formalization of normalization in Simply Typed λ-Calculus via an interpretation into a Kripke model. An alternative categorical account in the same spirit can be found in Altenkirch, Hofmann, and Streicher [AHS95].

Categorical models of Type Theory and Coherence Problems. Hofmann [Hof95] used Cartmell’s categories with attributes for his setoid-model of Type Theory. This work provides a represention of Extensional Type Theory with quotient types in Intensional Type Theory. Hofmann and Streicher [HS94] constructed a groupoid model of Type Theory to show the failure of the uniqueness property for proofs of the equality proposition. Hofmann [Hof94] also applied a result by Benabou and showed how to construct a split model of Type Theory from a non-split one. This is an alternative approach to coherence in Type Theory to Curien’s work on substitution up to isomorphism. Dybjer [Dyb95] introduced categories with families. This is a variant of categories with attributes and are appropriate as a basis for Internal Type Theory.

Logical predicates and structural induction. Hermida [Her93] gave a categorical account of logical predicates for simply typed theories and of structural induction for inductive types in this setting.

2.3.3.2 Coinductive definitions

Infinite objects via guarded recursion. Coquand [Coq94] proposed a new way to extend Type Theory with infinite objects. This proposal can be contrasted to the final coalgebra approach to coinductive types and definition by destructors. Instead types of infinite objects are defined by constructors – like inductive types. Coquand introduced a notion of definition by guarded recursion, which ensures that functions are “productive”. Guarded recursion plays a somewhat dual role to definition by primitive recursion, which is used in standard Type Theory to ensure termination of functions.

Final coalgebras via ω-limits. In the Work Plan we expressed the intention to study the method for encoding coinductive types via ω-limits in Intensional Type Theory following the work of Hallnäs, Lindström, and Mendler. However, this study is still inconclusive. A short note to explicate Mendler’s work in more Type-Theoretic terms was written by Dybjer and Hofmann [DH94]. And Pitts observed that there is a very close connection between Hallnäs’ method and the earlier work on categorical powerdomains by Lehmann and Abramsky.

2.3.3.3 Recursive types in functional languages

Applications of algebraic compactness. Studying this notion of Freyd led Pitts [Pit] to prove that the partial order on a recursive predomain D is the greatest fixed point of a certain monotonic operator associated to D. This provided a principle of proof by coinduction for these recursive predomains: to show that one element of D approximates another, it suffices to find a binary relation containing the two elements that is a post-fixed point for the associated monotone operator. The statement of the proof principles is independent on the explicit method for constructing D.

Two specific instances of these principles occurred in earlier work by Abramsky [Abr91, Abr90] in the form of ‘internal full abstraction theorems’ for denotational semantics of SCCS and the lazy lambda calculus.

Mixed induction/coinduction. Freyd’s approach includes an approach to reflexive types, modelled as fixed-ponts of functors of mixed variance. Based on this Pitts [Pit93b] described a mixed induction/coinduction property for recursively defined domains. The utility of this property is demonstrated by deriving a family of proof principles from it. One example is the above-mentioned coinduction principle; another concerns induction for admissible subsets of general recursively defined domains extednding the principle of structural induction for inductively defined sets.

Proofs of correspondence between operational and denotational semantics. These proofs depend on the existence of certain relations specified as fixed points of nonmonotonic operators. Pitts [Pit93a] showed how to construct such relations withour having to delve into the detailed construction of the recursively defined domains themselves.

Applications to stream processing. Gordon [Gor95] and Pitts [Pit96] established properties of functional programs by using a coinductive characterization of contextual equivalence. They showed how to apply this technique to several stream processing examples.

2.3.3.4 Conclusions

The objectives on the topics of Inductive Types and on Recursive Types in Functional Languages were realized. These also led to several new developments not anticipated in the Work Plan.

The most interesting development on Coinductive Types was the work on guarded recursion by Coquand. This work was not anticipated in the Work Plan - in fact progress on the stated objective concerning the encoding of coinductive types in Intensional Type Theory was somewhat disappointing. A possible reason for this is that Intensional Type Theory is too low level for such an advanced task and that a good treatment of extensionality and quotienting [Hof95] is an essential prerquisite.

[Abr90] Samson Abramsky. The lazy lambda calculus. In David Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[Abr91] Samson Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[Acz80] Peter Aczel. Frege Structures and the Notions of Proposition, Truth, and Set, pages 31–59. North-Holland, 1980.

[Acz88] Peter Aczel. Non-Well-Founded Sets, volume 14 of CSLI Lecture Notes. Stanford University, 1988.

[AHS95] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David Pitt, David E. Rydeheard, and Peter Johnstone, editors, Springer LNCS 953, Category Theory and Computer Science, 6th International Conference, CTCS ’95, Cambridge, UK, August 1995.

[Bac88] Roland Backhouse. On the meaning and construction of the rules in Martin-Löf’s theory of types. In Proceedings of the Workshop on General Logic, Edinburgh, February 1987. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1988. ECS-LFCS-88-52.

[BCMS89] Roland Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory (part 1). Formal Aspects of Computing, pages 19–84, 1989.

[CD93] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen (accepted for publication in Mathematical Structures in Computer Science), 1993.

[Coq93] Catarina Coquand. From semantics to rules: a machine assisted analysis. In Egon Börger, Yuri Gurevich, and Karl Meinke, editors, Proceedings of CSL ’93, LNCS 832, 1993.

[Coq94] Thierry Coquand. Infinite object in type theory. In Types for Proofs and Programs, International Workshop TYPES’93, LNCS 806, 1994.

[CP90] Thierry Coquand and Christine Paulin. Inductively defined types, preliminary version. In LNCS 417, COLOG ’88, International Conference on Computer Logic. Springer-Verlag, 1990.

[DH94] Peter Dybjer and Martin Hofmann. On the interpretation of coinductive types in intuitionistic type theory. Manuscript, September 1994.

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

[Dyb91] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

[Dyb94a] Peter Dybjer. A general notion of simultaneous inductive-recursive definition in type theory. Draft paper, 1994.

[Dyb94b] Peter Dybjer. Inductive families. Formal Aspects of Computing, pages 440–465, 1994.

[Dyb95] Peter Dybjer. Internal type theory. In Proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, Göteborg, January [Fu92] Yuxi Fu. Topics in Type Theory. PhD thesis, University of Manchester,

1992.

[Gor95] Andrew D. Gordon. Bisimilarity as a theory of functional programming. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, 1995.

[Hal87] Lars Hallnäs. An intensional characterization of the largest bisimulation. Theoretical Computer Science, 53:335–343, 1987.

[Her93] Claudio Alberto Hermida. Fibrations, Logical Predicates and Indeterminates. PhD thesis, Department of Computer Science, University of Edinburgh, November 1993. Report DAIMI PB - 462, Computer Science Department, Aarhus University.

[Hof94] Martin Hofmann. Interpretation of type theory in locally cartesian closed categories. In Proceedings of CSL. 1994.

[Hof95] Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995.

[HS94] Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In LICS 1994, pages 208–212. IEEE Press, 1994.

[Laf88] Yves Lafont. Logique, Categories & Machines. Implantation de Langages de Programmation guidee par la Logique Categorique. PhD thesis, l’Universite Paris VII, January 1988.

[Lin89] Ingrid Lindström. A construction of non-well-founded sets with Martin-Löf’s type theory. Journal of Symbolic Logic, 54(1):57–64, 1989.

[Men91a] Nax-Paul Mendler. Σ is cocontinuous. Manuscript, Computer Science Department, Manchester University, March 1991.

[Men91b] Paul Francis Mendler. Predicative type universes and primitive recursion. In Proceedings Sixth Annual Synposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[ML71] Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 179–216. North-Holland, 1971.

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

[ML75a] Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In Proceedings of the 3rd Scandinavian Logic Symposium, pages 81–109, 1975.

[ML75b] Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium ‘73, pages 73–118. North-Holland, 1975.

[ML82] Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153– 175. North-Holland, 1982.

[Pal91] Erik Palmgren. On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf’s Type Theory. PhD thesis, Uppsala University, [Pit] Andrew M. Pitts. A co-induction principle for recursively defined do-

mains. Theoretical Computer Science. To appear.

[Pit93a] Andrew M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. Draft paper, 1993.

[Pit93b] Andrew M. Pitts. Relational properties of recursively defined domains. In Proc. 8th Annual Symposium on Logic in Computer Science, Montréal, pages 86–97. IEEE Computer Soc. Press, 1993.

[Pit96] Andrew M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 1996. To appear.

2.4 Topic D: subtypes and polymorphism in higher order languages

2.4.1 Summary

The collaborating partners on this topic are CAIMENS, Genova, Manchester, and Sussex. It has involved the collaboration of Curien, Hilken, Robinson, Rosolini, and Rydeheard. The publications which form the deliverables under this Topic are items [ACC93], [RR94], [HR94], and [HR93].

2.4.2 Objectives

The original intentions were to analyse the categorical structure of logical relations as in the recent works of Abramsky, Freyd, Mitchell, Reynolds, Scedrov and others, see e.g. [AJ91, BFSS90, Fre93, MR92, MS93]. The goals were to get a possibly simple, abstract understanding of the combination of recursive type constructors with a subtyping discipline for which models were known only with very technical presentations. In particular, a better understanding of the semantic significance of parametricity would be convenient to improve the use of categorical models. Some previous work of Rosolini and Robinson on categorical models of the calculus of constructions has shown that a kind of “parametric condition” can be embedded canonically in the construction of a model that makes its properties stable under equivalence, see [FRR92].

Moreover there has been further study under the heading of Topic D on the theories of classes and their proof structures and a new elementary notion of a structured category has been discovered which may be useful to study models of computations.

The workplan of the project listed research for this topic to span only two years of the project.

2.4.3 Results

2.4.3.1 Parametric polymorphisms

Study was carried out on parametricity in polymorphism from both the syntactic and the semantic side. It is important to keep them separate.

The syntactic approach to parametricity In [ACC93] Curien with Abadi and Cardelli of DEC consider a formal system which is an extension of system F which enables them to speak of the parametric properties in system F. And they can deduce various of the known results about parametricity (e.g. Reynolds’ abstraction theorem).

In [ACC93] an extension of system F, called R is introduced with relations between types which can be constructed and operated upon in a way which resembles formally the caluculs of logical relations. The basic judgements consists of three parts: one about the relation, and two relative to terms in the domain and the codomain of a relation which are in some sense connected by the stated relation, for instance:

\frac{E ⊢ \begin{matrix}b : A → B \\ S → T \\ b′ : A′ → B′ \end{matrix} E ⊢ \begin{matrix}a : A \\ S \\ a′ : A′ \end{matrix}}{E ⊢ \begin{matrix}b(a) : B \\ T \\ b′(a′) : B′ \end{matrix}}

The free theorems of [Wad89] and others can be stated in the formal system and proved as well as a syntactic form of the abstraction theorem. With this syntax it is possible to formulate results and conjectures that relate the intuitive definition of parametricity (that the behaviour of a polymorphic function does not depend on the instantiating type) with that of Reynolds.

The natural logic for reasoning about the structures which arise within the context of parametric polymorphism is that of Abadi and Plotkin. This seems to appear in the semantic construction to generate models for the system R of formal parametric polymorphism of Abadi, Cardelli and Curien. This is presented in a paper submitted for publication by Abadi, Bellucci, and Curien [ACC93]. The use of a very particular example (that of saturated PERs) for the general one helps to show that the actual problem for proposing a clean categorical interpretation of a logical system based on parametric polymorphism like system R requires the use of a fibration over another fibration: the power of a parametric system is immediately tested by introducing the relational graph of a term. The syntactic dependence forces another level of fibration. The paper shows that a semantic interpretation can be given in terms of environments, and suggest that also a categorical semantics can be given in the form of fibrations.

The semantic approach to parametricity One of the main intents is to follow the category-theoretic paradigm to study the problem of parametricity. In their fundamental paper [MR92], Ma and Reynolds gave a categorical description of the requirements for a parametric model of polymorphism. Many other approaches in the literature had tried to give a suitably abstract version of the calculus of relations in order to achieve parametric models (possibly not quite within the paradigm expressed in [MR92]).

In [FRR92] certain PL-categories (=models of polymorphism) were presented where interpretations of terms were invariant under isomorphisms. The notion of functorial parametricity introduced there shows that part of the “dinatural” behaviour can be seen from within the model, e.g. a cartesian closed category with some completeness properties, as in [Pit87]. What matters is that families be taken together with an action on isomorphisms.

In [Rob92] Robinson connects the notion of functorial parametricity to the notion of data abstraction. He introduces a polymorphic language extended with structure declarations (similar to that of [Rey83]), and he characterizes those interpretations of polymorphic terms which are invariant under isomorphism as those which are independent of the structure implementations.

In [RR94] Robinson and Rosolini present a general method to obtain a parametric model from a PL-category which satisfies suitable conditions (the same as in [MR92]). The construction is done mimicking those of [AJ91, OT93] and applies the concept of reflexive graph of categories. We believe it makes a clear step forward in the semantic analysis of parametricity. It is also significant that the structure at the base of the models mentioned in [Plo93] are particular instances of the construction performed.

Furthermore, there are transparent links to related works. The results in [BFSS90] about PER models follow from the main result of [RR94]. The structors of [Fre93] can be described as particular families among those considered, and the categories of structors are reflective subcategories of those considered (in a sense, one may say that it explains how the structure of categories intervenes in the definition of a structor). The relators considered in [MS93] are a more general construction than that given in [RR94] in the same way as homomorphisms of graphs are more general than homomorphisms of reflexive graphs. The construction in [FRR92] is a particular case of that considered. In a similar way, it is possible to look at (models of) subtyping as a special case of parametricity. (From a completely syntactic point of view an analogous idea was considered in [MR92].) The main difference with respect to all these cases is that the structure on the categories in the case now considered is very simple and explicit.

We have then developed a general machinery to produce categorical models of polymorphism which are parametric. In fact, what was probably the main issue here was to determine the precise meaning of the question asked. Ma and Reynolds [MR92] had shown that the structure to investigate was that of a reflexive graph of PL-categories. But the problem remained to produce some examples of these. The various attempts in the literature all consisted in specifying “some” structure on the category of logical relations of a given model (dinaturals, relators, structors). In fact, the categorical point of view suggested one candidate for a possible solution, and we found that the answer was to choose the structure of reflexive graph on categories.

The slogan may be that every model of polymorphism (which satisfies some suitable, quite general, hypotheses) can be refined to a parametric model. And this can actually sound rather intuitive. But the explicit statement which refers to categorical models explains precisely what one may get: given any PL-category A (which is suitable for polymorphism, see [MR92]), there are a reflexive graph of PL-categories and functors

B [figure] A_{p}

and an embedding of cartesian closed fibrations

A ^{⊂} A_{p}

such that the fibre over 1 of the reflexive graph is (equivalent to)

REL(A_{p}) [figure] A_{p}(1).

Moreover the embedding induces an equivalence on the fibres over 1 (the categories of “closed types”).

The construction explains why the various other categorical constructions encoded parts of the properties of “parametric” types, but always seemed to fail in some respect.

Some initial investigations show that the model of [Has91] provides a categorical model which is parametric, and the model of coherence spaces of [Gir89] is “almost” parametric. We tested the power of the model construction for parametric polymorphism on those models which can be obtained from an internal complete category. For instance, in the overused case of PERs, one obtains a model whose fibre of closed types is equivalent to that of saturated PERs as given in the paper on Functorial Polymorphism of Bainbridge, Freyd, Scedrov, and Scott. In the case of models obtained from algebraic classes of categories, or more generally, from fibrations of domains, it is not at all clear if a parametric completion can be obtained because these models do not have all limits (in particular pullbacks). This lack of definability prevents us from applying the results we had obtained even in the simplest of all: McCracken’s model of closure operators on a universal algebraic lattice.

Trying to overcome this obstruction, Claudio Hermida suggested to apply a different view: at the first-order level, the calculus of logical relations can be derived from a logic for reasoning about types. An example of this is the passage from logical predicates (=unary relations) to n-ary relations, obtained by formalizing the idea that an n-ary relation is a predicate on the product of the corresponding types. There is a general, mathematical scheme to do this which was presented at the recent MFPS conference in New Orleans. The next stage, which is under current consideration, is to extend the treatment to the second-order level. Preliminary indications are that the natural logic for reasoning about the structures which arise within this context is that of Abadi and Plotkin.

2.4.4 Models for subtyping

By means of a construction similar to the one above, it is possible to give models for languages with substypes. The structure involved is similar to the case of unary logical relations. So one obtains a retraction of categories rather than a reflexive graph. In this framework one can give models of subtypes like those advocated in [Pho92] which make no reference to (canonical choices of ) coercions. The properties of these are surprisingly similar to those for the parametric models. Also, one can model the logic of type coercions of [LMS94] which seems to be a very good candidate for a type system which allows the largest number of term equalities preserved udner type-erasure. This work needs to be extended.

2.4.5 Higher order theories of classes and categorical models of computations

Further input for the researches has come from the work of Hilken and Rydeheard on formalizing the syntactic power of comprehension principles in the line of the seminal work of Lawvere [Law70], see also [Pav93]. It is important to investigate how far we can take the structure discovered in models and if it possible to “simplify” the logical notation which has to be employed. In [HR92] they introduce theories of classes as a sort of set theory in natural deduction form with proofs which strongly normalize. (In this way, one avoids the standard paradoxes.) In [HR93] a different presentation is given which is more directed to the proof theory.

The proof structure and models of theories of classes was investigated in [HR93] where classes are ‘collections’ of entities. The theories are weaker than set theories and arise from a study of type classes in programming languages, as well as comprehension schemata in categories. Two languages of proofs are introduced: one is a simple type theory and the other has proof environments for storing and retrieving partial proofs. The relationship between these two languages is defined in terms of a normalisation result for proofs. The result leads naturally to the definition of a categorical semantics for classes for which we can establish coherence.

In a similar vein, [HR94] describes a precise notion of ‘category of generalised sets of computable elements’ in the same way that the description of an elementary topos makes precise a notion of ‘category of generalised sets’. This notion of category is denominated as compos. The axioms for a compos are based on a category of decidable partial equivalence relations. The preliminary investigations on the new notion of compos show that the theory should find applications in the description and implementation of formal systems.

2.4.6 Conclusions

The structure involved in parametric polymorphism is well understood, from a syntactic point of view as well as a semantic point of view. It is clear that it must now be applied to construct parametric models from old ones. Some models on domains (e.g. expers) should also help in developping subtyping further in this context.

Various open problems in models of polymorphism have been solved, and further research should be done in accomplishing a better, closer connection between the syntactic aspect and the semantic aspect. Use of category theory is crucial here.

The theory of compos has shown sufficient expressive power to be applied in the description and implementation of formal systems.

2.4.7 References and selected publications

[ACC93] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theo. Comp. Sci., 121:9–58, 1993.

[ACC93] M. Abadi, R. Bellucci, and P.-L. Curien. A model for formal parametric polymorphism: a per-interpretation for system R. submitted for publication, 1995.

[AJ91] S. Abramsky and T. Jensen. A relational approach to strictness analysis for higher-order polymorphic functions. In Proceedings of the 18th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 49–54, Orlando. ACM, 1991.

[BFSS90] S. Bainbridge, P. Freyd, A. Scedrov, and P. Scott. Functorial polymorphism. Theo. Comp. Sci., 70:35–64, 1990.

[Coq89] T. Coquand. Categories of embeddings. Theo. Comp. Sci., 68:221-237, 1989.

[CGW89] T. Coquand, C. Gunter and G. Winskel. Domain theoretic models of polymorphism. Inform. and Comput., 81:123–167, 1989.

[Fre92] P. Freyd. Remarks on algebraically compact categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory ’90, Lectures Notes in Mathematics vol. 1144, pages 131–140. Springer-Verlag, 1992.

[Fre93] P. Freyd. Structural Polymorphism. Theo. Comp. Sci., 1993.

[FRR92] P. Freyd, E. Robinson, and G. Rosolini. Functorial Parametricity. In A. Scedrov, editor, Proc. 7th Symposium in Logic in Computer Science, pages 444–452, Santa Cruz. I.E.E.E. Computer Society, 1992.

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

[Has91] R. Hasegawa. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. In T. Ito and A. Meyer, editors, Theoretical Aspects of Computer Software, Lectures Notes in Computer Science vol. 526, pages 495–521. Springer-Verlag, 1991.

[HR92] B.P. Hilken and D.E. Rydeheard. Towards a categorical semantics of type classes. Fund. Inf., 16:2, 1992.

[HR93] B.P. Hilken and D.E. Rydeheard. A theory of classes: proofs and models. submitted for publication, 1993.

[HR94] B.P. Hilken and D.E. Rydeheard. Categories with computable structure, 1994. submitted to Math. Struct. Comput. Sci.

[HP89] J.M.E. Hyland and A.M. Pitts. The theory of constructions: categorical semantics and topos-theoretic models”, In J.W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, Boulder June 1987, Contemp. Math. vol. 92, pages 137–199. A.M.S., 1989.

[Law70] F.W. Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In A. Scedrov, editor, Proc. Symposium in Pure Mathematics, pages 1–14. A.M.S., 1970.

[LMS94] G. Longo, K. Milsted, and S. Soloviev. A logic of type coercions, 1994. Draft.

[Ma92] Q. Ma. Parametricity as subtyping. In Proceedings of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 281–292, Albuquerque NM. ACM, 1992.

[MR92] Q.M. Ma and J.C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes, M. Main, A. Melton, M. Mislove, and D.Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 1–40. Springer-Verlag, 1992.

[MS93] J. Mitchell and A. Scedrov. Notes on sconing and relators. To appear.

[OT93] P. O’Hearn and R. Tennent. Relational parametricity and local variables. In Proc. 8th Symposium in Logic in Computer Science, Montreal. I.E.E.E. Computer Society, 1993.

[Pav93] D. Pavlović. On completeness and cocompleteness in and around small categories. To appear in Annals of Pure and Applied Logic, 1993.

[Pit87] A. Pitts. Polymorphism is set theoretic constructively. In D. Pitt, A. Poigné, and D. Rydeheard, editors, Category theory and Computer Science, Lectures Notes in Computer Science vol. 283, pages 12–39, Edinburgh. Springer-Verlag, 1987.

[Pho92] W. Phoa. Using fibrations to understand subtypes. In Fourman, Johnstone, and Pitts, eds. Procs. Symposium in Applications of Categories to Computer Science. Cambridge University Press, 1992, pages 239–257.

[Plo93] G. Plotkin. Second order type theory and recursion, 1993. Lecture at the Scott Fest.

[Rey83] J.C. Reynolds. Types abstraction, and parametric polymorphism. In R.E.A. Mason editor, Information Processing ’83, pages 513–523. North Holland Publishing Company, 1983.

[Rob92] E. Robinson. Parametricity as isomorphism. Report 5/92, University of Sussex, 1992.

[RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In S. Abramsky, editor, Proc. 9th Symposium in Logic in Computer Science, pages 364–371, Paris, 1994. I.E.E.E. Computer Society.

[Wad89] P. Wadler. Theorems for free! In Proc. 4th International symp. on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, London, 1989. Springer-Verlag.

2.5 Topics E and F: higher order modal program logics and monadic programming language semantics

2.5.1 Summary

The collaborating partners on these topics are Cambridge, Genova and Sussex. It has involved the collaboration of Moggi, Pitts, Robinson and Stark. The publications which form the deliverables under these Topics are items [CM93], [FMS95], [Mog94a], [Mog94b], [Mog95], [Mogar], [Pitar], [Pit96], [PS93], [RP95], [Rob94a], [Sta95].

2.5.2 Objectives

The overall objective was to develop the monadic approach to programming language semantics originated by one of the members of the consortium [Mog91]. This is already widely accepted as an important advance in structuring semantic descriptions and addresses the important issue of modularity in both programming language semantics and corresponding program logics. The following were the specific objectives.

1. To formalise the monadic approach in a general-purpose program logic in the LCF style (programs represented by lambda terms, correctness assertions by formulae, and reasoning about programs achieved by reasoning about the mathematical structures for program semantics). Previous work (undertaken in the first CLICS project) had produced a modal program logic based upon the monadic approach, called Evaluation Logic [Pit91, Mog91]. The intention was to extend Evaluation Logic to a higher order logic incorporating proof principles drawn from the work in Topic B on ‘synthetic’ domain theory and the work in Topic C on induction and co-induction principles for recursive datatypes. The aim of such a generalpurpose program logic is to provide a uniform framework for presenting various programming languages and program logics, and to support a modular approach to their description and properties.

2. To test the effectiveness of the monadic approach through some substantial case studies involving language features for which existing semantic methods do not provide a completely satisfactory analysis. Attention was focussed on locally declared state in higher-order procedural languages, with the aim of understanding better what are the fundamental principles underlying the observable behaviour of local state in both block-structured languages (like Algol) and ones with dynamically allocated state (like Standard ML).

2.5.3 Results

2.5.3.1 Higher Order Evaluation Logic

[Mog94a] presents a formalisation of Evaluation Logic as a definitional extension of higher order predicate logic with dependent types and computational types, whose semantics does not require any special properties of the strong monad interpreting computation types. In other words the evaluation modalities and evaluation predicate can be defined and axioms for them proved sound formally without referring to the categorical semantics. To model the logic, one needs to consider quasi-toposes equipped with a fibred monad (to interpret computational types). From the point of view of denotational semantics the main issue is how categories of predomains (such as the category of cpos) relate to an ambient category (such as a quasi-topos). This issue was investigated in the setting of Synthetic Domain Theory (see [Hyl91, Tay91]): the category of predomains must form a full reflective sub-fibration of the ambient category. A model which fits these requirements (and also those for interpreting polymorphic languages) is the quasi-topos of ω-sets with the full reflective sub-fibration of complete extensional PERs (see [FMRS90]). In this model fibred endofunctors have a simple alternative characterisation: they correspond to endofunctors realisable by a Turing machine.

The expressivity of Evaluation Logic was tested by constructing an interpretation in it of the ‘Variable Typed Logic of Effects’ (V T LoE) of Honsell et al [HMST95]. V T LoE is a program logic for reasoning about programs written in λ_{mk}, a call-by-value λ-calculus with references (basically the untyped counterpart of the fragment of ML studied in the project). It is the latest product of an ongoing research effort (especially by Mason and Talcott) in finding powerful reasoning principles for languages with destructive memory operations. [Mog94b] gives a simple way of representing the contextual assertions of V T LoE into Evaluation Logic. The basic idea is to translate a contextual assertion ϕ, say with one free variable, into a predicate ϕ^{∗} over T V, where V is the type of values for λ_{mk}. This representation validates all logical axioms of V T LoE and avoids the intensionality problem present in [HMST95], i.e. failure of the substitutivity rule

e ≅ e′ Φ(e)
\overline{(SUB)}
Φ(e′)

(this problem is also overcome by the localised version of the satisfaction relation given in [Tal93], which however is substantially more complicated). This representation result provides evidence of the expressiveness of Evaluation Logic, and the usability of contextual assertions for programming languages different from λ_{mk}.

We have looked at ways of representing other program logics in Evaluation Logic, by analogy with V T LoE. This seems feasible for Hoare logic and the modal μcalculus (where formulae are interpreted by sets of states in a labelled transition system). In the latter case, it seems that the only change to the translation of V T LoE needed for accommodating the necessity modalities [a]ϕ of the modal μ-calculus is to make more explicit the structure of computational types, e.g. by saying that T X is of the form T′(X + (A × T X)) for some simpler computational monad T′. On the other hand, it seems that the temporal μ-calculus (where formulae are interpreted by sets of runs) is unlikely to admit a simple representation into Evaluation Logic.

2.5.3.2 Metalanguages and Applications

[Mogar] considers typed metalanguages of increasing complexity, ranging from a naive one (with a set-theoretic semantics) to one incorporating ideas from Synthetic and Axiomatic Domain Theory and which is a proposal for the general-purpose program logic in Objective 1.

The monadic and incremental approaches are first formulated in the setting of a type-theoretic framework with dependent types and a naive set-theoretic semantics. The use of dependent types is particularly important here, since it allows a precise, concise and general description, based on LF-signatures as abstract representations for languages. Subsequently, the issue of recursive definitions is addressed, by incorporating ideas from Axiomatic and Synthetic Domain Theory. From SDT we take the idea that predomains should be part of a set-theoretic universe with an expressive logic. From ADT (in particular the work of Crole, Freyd, Pitts and Simpson) we take equational reasoning principles, which are valid in many categories used in Denotational Semantics, such as the category of cpos. Finally, computational types (and the monadic and incremental approaches) are revised in this richer setting.

The approach adopted has three novel aspects:

• it makes significant use of type theory as a tool for describing languages and calculi, while this is usually done via a set of formation or inference rules;

• it incorporates ideas from Axiomatic and Synthetic Domain Theory into metalanguages, while most metalanguages for denotational semantics are minor variants of LCF;

• it stresses the use of metalanguages to give semantics via translation (using the monadic and incremental approaches), but avoids a detailed analysis of the categories used in denotational semantics, since the metalanguages involved require richer categorical structures.

2.5.3.3 The Nu-Calculus

In pursuit of Objective 2, we applied the general methods for program semantics and program logics being developed in this project to study increasingly complicated fragments of Standard ML involving dynamically allocated local state (ML’s ‘reference types’). We began with an apparently very simple fragment, christened the nu-calculus, in an attempt to identify what, if any, are the difficulties created purely by locality of state, independent of other properties such as side-effects, exceptional termination and non-termination due to recursion.

The nu-calculus appears at first sight to be an extremely simple system for which one might expect to construct fully abstract models and complete proof systems for reasoning about observational equivalence. However [PS93] shows that this expectation is misplaced: nu-calculus expressions can exhibit very subtle behaviour with respect to an appropriate notion of observational equivalence. That paper introduces an operationally-based notion of ‘logical relation’ for the nu-calculus incorporating a version of representation independence for local names, drawing on denotationally-based work of O’Hearn and Tennent [OT93]. The logical relations is used to establish the termination properties of evaluation in the nu-calculus and to provide a useful notion of ‘applicative’ equivalence between nu-calculus expressions which implies observational equivalence. Although the two notions of equivalence differ at higher order types, they coincide for expressions of first order types and are decidable there. A compositional (on types) explanation of observational equivalence of nu-calculus expression at higher types is still lacking.

2.5.3.4 Dynamic Allocation Monads

[Staar] investigates monad-based denotational semantics for the nu-calculus. The use of categorical monads to enforce a distinction between denotations of values (expressions in canonical form) and denotations of computations (arbitrary expressions) is particularly helpful here, since it allows one to identify explicitly and simply what structure is needed in a model to give a static meaning for the key dynamic aspect of the nu-calculus, the action of computing a new name. Some simple structure on a category equipped with a strong monad is identified which is sufficient to guarantee that the nu-calculus can be modelled in the category in a computationally adequate way. An instance of this categorical structure can be obtained by adapting Moggi’s ‘dynamic allocation’ monad to O’Hearn and Tennent’s category of relationally parametric functors. This model is shown to be fully abstract at first order types, but not so at higher types. Other instances of the categorical structure are known and can be used to establish subtle, higher order observational equivalences. So far no fully abstract (concrete) model of the whole language is known.

2.5.3.5 Operationally-Based Models of Local State

The extension of the work on the nu-calculus to more complicated fragments of ML with dynamically allocated storage for higher order functions dramatically complicates the construction of suitable monads. One reason is because their construction involves solving complicated, mixed-variance domain equations. Here [Pit96] provides useful techniques for dealing with such domains, and particularly for constructing various logical relations on the domains needed for computational adequacy and arguments involving representation independence of local store. However there remains the problem that all but the simplest monads involve taking quotients by equivalence relations in their construction and such quotients in categories of domains are difficult to deal with (because they involve completion constructions). Pitts, de Paiva, Ritter and Stark side-stepped these difficulties by considering termmodels defined directly from the operational semantics of a suitable computational metalanguage, called the Monadic Store Calculus. To do this they generalised Abramsky’s co-inductively defined notion of ‘applicative bisimilarity’ from pure functional languages to ones with local state: the closed terms of the monadic store calculus quotiented by applicative bisimilarity comprise the model. One advantage of the monadic approach is seen in the fact that up to bisimilarity, product, function, and recursive types satisfy familiar equational and categorical properties properties (e.g. βη-conversion and surjective pairing hold). In other words the complications in the theory due to the presence of non-termination and side-effects are encapsulated in the computation types. There is a compositional (call-by-value) translation of the target fragment of ML into the model with the property that bisimilarity of translated programs implies observational equivalence between the programs. An account of this work is in preparation. A description of some of the methods appears in [RP95].

2.5.3.6 Monadic Semantics of CCS-like Languages

Moggi [FMS95] (in collaboration with Sangiorgi and Fiore) and Stark [Sta95] both investigated the denotational semantics of CCS-like calculi, including Milner’s πcalculus. The main technical result is a fully-abstract model in a suitable functor category of domains for π-calculus agents up to strong late bisimulation. An important methodological aspect of this work is that the technical tools needed had already been developed in the project independently from any considerations to do with the π-calculus:

• Functor categories had been proposed by Oles and Reynolds for modelling locality in Algol-like languages, and used by Pitts and Stark for modelling dynamic allocation of references (see section 2.5.3.4). Therefore, they should be used to model privacy of names in the π-calculus.

• The incremental approach to denotational semantics considered by Cenciarelli and Moggi (see section 2.5.3.2), in particular the monad transformer for adding resumptions, gives a uniform way of dealing with pure CCS and CCS with value passing, and suggests how to proceed in the case of the π-calculus.

2.5.4 Conclusions

The work completed on this Topic during the lifetime of the project has combined the development of general techniques and methodologies (such as the monad-based and incremental approach to semantics, and the use of co-inductively defined program equivalences) with their application to study specific programming language features (such as dynamically allocated local state). We believe that these techniques and methodologies may substantially aid the construction of good semantic models for new languages (such as the π-calculus—see section 2.5.3.6). Substantial effort during the last year of the project went into producing tutorial material on the techniques and methodologies developed under this Topic of the project: see [Mogar] and [Pitar].

2.5.5 References

[CM93] P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of the Conference on Category Theory and Computer Science, Amsterdam, Sept. 1993, 1993. CWI Tech. Report.

[DP9?] P. Dybjer and A. M. Pitts, editors. Semantics and Logics of Computation. Cambridge University Press, 199? Based on lectures given at the CLICS-II Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge UK, September 1995.

[FMRS90] P. Freyd, P. Mulry, G. Rosolini, and D. Scott. Extensional pers. In 5th LICS Conference. IEEE, 1990.

[FMS95] M.Fiore, E. Moggi and D Sangiorgi. A fully-abstract for the π-calculus. Submitted for publication, 1995.

[HMST95] F. Honsell, I.A. Mason, S.F. Smith, and C. Talcott. A variable typed logic of effects. Information and Computation, 119:55-90, 1995.

[Hyl91] J.M.E. Hyland. First steps in synthetic domain theory. In A. Carboni, C. Pedicchio, and G. Rosolini, editors, Conference on Category Theory ’90, volume 1488 of LNM. Springer Verlag, 1991.

[Mog91] E. Moggi. Notions of computations and monads. Information and Computation, 93:55–92, 1991.

[Mog94a] E. Moggi. A general semantics for evaluation logic. In 9th LICS Conference. IEEE, 1994.

[Mog94b] E. Moggi. Representing V T LoE in evaluation logic. Available via FTP from theory.doc.ic.ac.uk at /theory/papers/Moggi, 1994.

[Mog95] E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.

[Mogar] E. Moggi. Metalanguages and applications. In ??, volume ?? of CISM Lecture Notes. Springer Verlag, to appear. Lectures given at the Advanced School on Typed Lambda Calculus and Functional Programming (Udine, September 1994) and at the CLICS-II Summer School on Semantics and Logics of Computation (Newton Institute, Cambridge, September 1995). A revised and expanded version will appear in [DP9?].

[OT93] P.W. O’Hearn and R.D. Tennent. Relational parametricity and local variables. In 20th POPL. ACM, 1993.

[Pitar] A. M. Pitts. Operationally-based theories of program equivalence. To appear in [DP9?].

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

[Pit96] A. M. Pitts. Relational properties of domains. Information and Computation, ?:?–?, 1996. To appear.

[PS93] A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdańsk, 1993, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, Berlin, 1993.

[RP95] E. Ritter and A. M. Pitts. A fully abstract translation between a λcalculus with reference types and Standard ML. In 2nd Int. Conf. on Typed Lambda Calculus and Applications, Edinburgh, 1995, volume 902 of Lecture Notes in Computer Science, pages 397–413. Springer-Verlag, Berlin, 1995.

[Rob94a] E.P. Robinson. A note on the presentation of enriched monads. available by ftp from theory.doc.ic.ac.uk, August 1994.

[Sta95] I. D. B. Stark. A fully abstract domain model for the π-calculus. Submitted for publication, 1995.

[Staar] Ian Stark. Categorical models for local names. Lisp and Symbolic Computation. To appear.

[Tal93] C. Talcott. Localized semantics for VTLoE. Working Notes, 21 October, 1993.

[Tay91] P. Taylor. The fixed point property in synthetic domain theory. In 6th LICS Conference. IEEE, 1991.

2.6 Topic H: computational content of classical proofs

2.6.1 Objectives

The question that is adressed here was one of the main question of proof theory, as formulated by Hilbert [14]: can we interpret constructively non effective reasoning? Techniques from computer sciences bring new lights to this old problem. Hilbert was concerned mainly with consistency of non effective reasonings, and he noticed that this is equivalent to say that if an universal statement has been proved via non effective means, then it holds for any instances. We are here interested in the question: if an existential statement has been proved by non effective means, is it the case that this non effective reasoning contains implicitely an algorithm that computes a witness of this statement? This question is connected to the Curry-Howard analogy between constructive proofs and programs: is it possible to extend this analogy to non effective proofs?

The main tool used so far in the analysis of this program is essentially the technique of negative translation, which goes back to Kolmogorov, 1925 (and rediscovered later by Gödel, Gentzen and Bernays). This method has been refined in a spectacular way by H. Friedman, 1978, who used it to prove that for a large class of non effective systems, a proof of an existential statement can be transformed to an effective proof.

There are deep connections between this method and a technique developped independently in computer science: the use of continuation. The existence of such a connection is a further illustration of the Curry-Howard analogy.

It is important to notice however that this negative interpretation method is not a solution to the general problem of giving a constructive explanation to constructive proofs. Typically, a non effective reasoning that combines the Axiom of Choice with Excluded Middle don’t get an interpretation in this way.

The goal of topic H was to analyse two aspects of the question of extracting computational content from classical proofs:

• (i) even for simple examples, the use of double negation leads to algorithms that have not a simple structure. But there are alternative methods, like the sequent calculus, introduced by Gentzen and refined by Lorenzen, Tait. Do these methods lead to simpler algorithm? Are the extracted algorithm the same extensionally? Furthermore, in these methods, we have to make, contrary to the intuitionistic case, non canonical choices. Are these non canonical choices unavoidable?

• (ii) It seemed that in some cases, for Ramsey’s theorem and Higman’s lemma, the use of the theory of locales can be relevant. The question was then to precise the connection between the theory of locales and the extraction of algorithms from classical proofs. This is connected to the problem of extending the interpretation of classical proofs to formal system that uses the Axiom of Choice.

2.6.2 Results

The main contributions were made by Chalmers, Paris. There are also some works done by Thomas Streicher.

2.6.2.1 Sequent Calculus

The starting point was the analysis of a simple example, due to G. Stolzenberg, where the use of the double negation method was complicated and the algorithm extracted was clearly non optimal. The analysis in sequent calculus, as formulated by Gentzen in his first paper on consistency proof for arithmetic [10] showed:

• that the use of sequent calculus may be simpler in some cases. Furthermore, it admits a suggestive game theoretical interpretation.

• that the algorithm extracted in sequent calculus is the same as the one extracted by the negative interpretation.

The first work on this was to see if one can prove the cut-elimination theorem from the game-theoretical formulation, by analysing the form of the interaction between two strategies. This was done in [6]. This was also the starting point of the work of Hugo Herbelin, who passed his Ph.D. thesis in january 1995. He showed that the interaction between strategies can be seen as a weak head strategy for cutelimination (according to the terminology used for λ-calculus). The importance of this result with other work in CLICS is seen when comparing with the game semantics for PCF given by Martin Hyland and Luke Ong. There, “canonical forms” of PCF (roughly: Böhm trees with constants) are interpreted by strategies while composition is an interaction between these strategies, like in the interpretation of sequent calculus. Hugoe Herbelin has shown similarly that the operational semantics of the composition in Hyland & Ong’s model was, again, weak – linear – head reduction (i.e. the head reduction performed by environment machines such as Krivine’s abstract machine).

This work is used now in a general analysis of environment machines [13].

One other application of the interpretation of proofs as strategies has been the discovery of a realizability interpretation of the negative interpretation of the axiom of choice [2]. Until now, the only computational interpretation of the axiom of choice used the Dialectica interpretation.

2.6.2.2 Formal Topology

The arguments used in a constructive proof of an infinite version of Ramsey’s theorem [7], using some form of well-founded induction, were reminiscent of notions used in the theory of locales or formal topology [1]. The goal of this work was to analyse further this analogy. One was curious also to test applications of formal topology to constructive mathematics.

The main achievement have been a constructive analysis of the notion of non principal ultrafilters [8], and a new analysis of the topological proof of van der Waerden’s theorem on arithmetical progression. Furthermore, the analysis of non principal ultrafilters lead, unexpectedly, to a simple intuitionistic proof of the closed/open Ramsey’s theorem.

The general method is as follows. We start from an argument that uses the existence of a point of a space X, existence that is proved non effectively, typically by using Zorn’s lemma. This existence is used to prove a purely existential statement ϕ. We give then a formal description of X. This can be seen as a geometrical theory, which describes a “generic” point of the space X. In some cases, it is possible to build effectively a topological model of this theory. We then get that ϕ holds in a relativized sense, namely in this topological model. To conclude, one needs a transfert principle, that allows to conclude that ϕ holds if it holds in the topological sense.

What is interesting in this approach is that it extracts computational content in cases where other methods, like negative interpretation or sequent calculus, do not work, because it interprets some classical use of the axiom of choice. However, there are some uses of Zorn’s lemma, like in some proof of Hindman’s theorem [12], that don’t seem to be covered by this method, while this method applies to cases where classically the space X is without points, while being non trivial formally (for instance, the space of surjective functions from 2^{N} to N.),

The work on the space of ultrafilters is a first step to the analysis of non separable spaces. The problem is that these spaces are non absolute, and the method of generic points does not work so smoothly. Nice examples of use of non separable spaces are provided by the different proofs of Hindman’s theorems [12]. These proofs resist to the analysis we have so far.

On the other hand, we have recently been able to analyse the theorem of Hahn-Banach [5]. This was already proved by J. Vermeulen [15] in the framework of topos theory, but our proof can be done in type theory, and is closer in structure to the usual proof. We have also suggested a definition of the formal space of reals that use only finitary inductive definition [4].

2.6.3 Conclusions

The use of the game-theoretical interpretation of proofs provided an heuristic help for finding the realizability interpretation of the negative interpretation of the axiom of choice. This interpretation can be improved computationally, and here the work on game-semantics/PCF and CDS should play a role. Furthermore, this does not help in any way in the constructive understanding of the combination of the axiom of choice and classical logic. We have done some experimentation on analysing proofs on computers [9], but much more can be done, as indicated by the work of Berger and Schwichtenberg. It should be possible to use the technique of Goad [11] systematically here. We are hoping here that the notions developped about formal space will be fruitful. We think that the notion of site, which is a refinement of the notion of space, should allow to interpret some proofs that cannot be interpreted in topological models. However, this is only a conjecture yet. A good way to proceed now is probably to systematically rework the results of the theory of locales in the framework of formal spaces, with a complete formalisation, if possible mechanized, in Martin-Lof’s type theory. This work should be of interest for a systematic constructive development of the theory of locales.

2.6.4 References

[1] S. Abramsky. Domain Theory in Logical Form Annals of Pure and Applied Logic, 1987.

[2] S. Berardi, M. Bezem and Th. Coquand. On the Computational Content of the Axiom of Choice. TLCA Edimburgh, LNCS 902, 1995.

[3] U. Berger and H. Schwichtenber. Proofs and Programs. Proof and Computation, proceeding of the Marktoberdof Summer School 1993, NATO ASI Serie

[4] J. Cederquist and S. Negri. The Continuum as a Formal Space. Draft Paper, 1995.

[5] J. Cederquist, Th. Coquand and S. Negri. Helly-Hahn-Banach in Formal Topology. Draft Paper, 1996.

[6] Th. Coquand. A Semantics of Evidence for Classical Arithmetic. Journal of Symbolic Logic, Vol. 60, 1995, p. 325-337.

[7] Th. Coquand. An Analysis of Ramsey’s Theorem. Information and Computation, Vol. 110, 1994, p. 297-304.

[8] Th. Coquand. A Formal Space of Ultrafilters. Draft Paper, 1995.

[9] D. Fridlender. Ramsey’s Theorem in Type Theory. Lic. Thesis, Chalmers Univeristy, 1993.

[10] G. Gentzen. Collected Works. North-Holland, Szabo ed., 1969.

[11] Ch. Goad. Extraction of Programs from Proofs. Ph. D. thesis, Stanford, 1981.

[12] R. Graham, B. Rothschild, and J. Spencer. Ramsey Theory. John Wiley & Sons, New York, 1980.

[13] H. Herbelin. Séquent qu’on calcule. Ph.D. thesis, Paris VII, january 1995.

[14] D. Hilbert. Die logischen Grundlagen der Mathematik. Mathematische Annalen, 88, (1923), p. 151-165

[15] J. Vermeulen. Constructive Techniques in Functional Analysis. Ph. D. Thesis, Susseix, 1986.

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

2.7 Topic I: symbolic computation

2.7.1 Summary

This topic has been mainly developed in Marseilles, by Yves Lafont and his student Anne Massol. The publications corresponding to this topic are [Laf92], [Laf95a], [Laf95b], and [Mas95]. The main deliverable is a software written in CAML, by Anne Massol.

2.7.2 Objectives

Yves Lafont has started a new direction of research inspired by the work of Albert Burroni. Instead of making symbolic computation with terms, one uses planar diagrams (Penrose diagrams) which are more general and allow to decompose the operations of substitution into more primitive ones. With this new syntax, which is in fact the syntax of 2-categorical reasoning, it is still possible to work with terms, but also with various objects occurring in topology (knots), theoretical physics (quantum groups), and computer science (digital circuits). The main objectives were the following:

a) develop a general theory of rewriting for these diagrams;

b) implement a software for manipulating these diagrams in an interactive way;

c) experiment this software in one of its potential fields of applications, for instance the design of digital circuits;

d) write a book on the geometrical aspects of symbolic computation.

Another, more technical, objective has appeared during the work:

e) show that a certain presentation of the category of finite sets by 3 generators and 7 equations, which is the starting point of all this domain, is minimal.

2.7.3 Results

Objective (a) has only been partially achieved by Yves Lafont in [Laf92] and [Laf95a]. In fact, the theory is more complicated than it seemed. Objectives (b) and (e) have been achieved by Anne Massol. With Anne Massol’s software, it is possible to edit a diagram or an equation between diagrams. It is also possible to perform equational reasoning according to a given set of equations. The interface is purely graphical. For (e), see [Mas95]. Objective (c) has not yet been seriously considered, but we hope to benefit from fruitful interactions with the LIM (Laboratoire d’Informatique de Marseille). Objective (d) is under progress. The book will cover several topics, including the homological theory of Squier (see [Laf95b]).

2.7.4 References

[Laf92] Y. Lafont, “Penrose diagrams and 2-dimensional rewriting”, in “Applications of Categories in Computer Science”, London Mathematical Society Lecture Notes Series 177, pp 191–201, Cambridge University Press, 1992.

[Laf95a] Y. Lafont, “Equational reasoning with 2-dimensional diagrams”, in “Term Rewriting”, Lecture Notes in Computer Science 909, pp 170– 195, Springer-Verlag, 1995.

[Laf95b] Y. Lafont, “A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)”, Journal of Pure and Applied Algebra 98, pp 229-244, 1995.

[Mas95] A. Massol, “Minimality of the system of seven equations for the category of finite sets”, submitted to publication, available by ftp anonymous on lmd.univ-mrs.fr in pub/massol (french version : prétirage 95-37, Laboratoire de Mathématiques Discrètes, 163 avenue de Luminy, case 930, 13288 Marseille).

Conclusions and exploitation of results

Some promising new formalisms have already emerged from CLICS I, and a number of experimental implementations and case studies have been undertaken. 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). At this stage one can see that some of the work done in CLICS-I has already had an impact on more applied research.

• Various CLICS partners plan to continue the basic research effort of CLICS as part of a TMR network. The intension is to focus on three related and interacting areas by building directly on the achievements of CLICS:

– semantics of programming languages (will exploit Topic A, B and F);

– synthetic domain theory (will exploit Topic B and D);

– expressive type theories (will exploit Topic C, E and H).

• Aarhus anticipates continuing work and collaboration especially in the following areas:

The categorical presentation of models for concurrent computation as categories enabled the abstract formulation of bisimulation through open maps, and this in turn led to presheaf models. The extra power and flexibility they offer holds promise of a domain theory bringing together concurrency and independence models and usual domain theoretic techniques. There is already some success in extending presheaf models to higher-order processes. This work could be far reaching, as it is still true, as stated in the first CLICS proposal, that the study of concurrency is rather separate from traditional denotational semantics. On a smaller scale, the CLICS work on new names and semantics of the Pi-calculus is likely to extend to much broader classes of models.

Questions of adequacy and full abstraction of programming languages persist and demand further study building on the work in games semantics and strong stability. In particular there is ongoing work on bistructure models in collaboration with Curien and Plotkin.

• Cambridge expects to exploit the expertise gained in the CLICS projects in the following ways.

First, we expect to apply the experience gained in Topics C and F on recursive types, monadic semantics of higher order languages with state, and operationallybased methods to study verification techniques for object-based languages involving concurrent objects (ie multiple threads on one machine) and distributed objects (ie multiple threads on multiple machines). A proposal is being formulated for a UK EPSRC project in this area.

Secondly, we hope to build on our experience with game semantics acquired in relation to sequentiality (Topic A) to provide a compositional analysis at the intensional level of both programming languages and proof systems. In particular, a proposal, focusing on the computational content of classical proofs, will shortly be submitted for a UK EPSRC project.

Finally, experience gained in Linear Logic and in Synthetic Domain Theory forms the basis for further research plans in these foundational areas.

• Chalmers envisage the following exploitation of the expertise developed in the CLICS project.

The work on inductive and coinductive datatypes (Topic C) will influence the design of new versions of proof assistants for type theory. The work on reductionfree normalization and internal type theory could potentially also be applied in these proof assistants. Work on constructive category theory and reduction-free normalization is being continued both by the Darmstadt team and in collaboration with Phil Scott, University of Ottawa and Djordje Cubric, Cambridge. We are also making preliminary investigations of coherence problems from the point of view of constructive category theory.

• Genova envisages three possible exploitations of CLICS expertise.

The expertise on categorical model of polymorphism (Topic D) and that of the SHAPE project (University of Technology Sydney) will be exploited to aid the design of new languages for parallel architecture. The first step will consist in design an extension of SML incorporating ideas from shape theory, this should be done as part of a collaborative project (funded by the Australian Research Council) between UTS and University of Genova.

The expertise on evaluation logic (Topic E) could be used in designing a specification language for describing state changes, as part of a joint effort proposed by various sites of the COMPASS Working Group.

The expertise on monadic semantics (Topic F) will contribute to the EXPRESS HCM project, by providing denotational semantics to various process calculi.

• The work done at Imperial on game semantics and its applications will be continued by Abramsky and his group in Edinburgh. Significant extensions of game semantics beyond sequentiality in functional languages, to imperative features and concurrency, are already in hand. We will also consider connections with logic, and applications to typed concurrent object-oriented languages. This work will form part of an ongoing EPSRC-funded project, and may also form the basis for future proposals.

• Work done in Darmstadt on the semantics of databases will be carried further by Achim Jung in Birmingham. It has potential for guiding the design and implementation of database systems capable of dealing with partially specified data.

The work on continuous domains and the probabilistic powerdomain is being used by Abbas Edalat and his group in London as a foundation for new integration methods, which are of great practical use in a couple of applied fields, such as image compression and neural networks. Collaboration on these topics is now being funded by the British Council and the German Academic Exchange Service (DAAD) under the ARC scheme.

• Manchester is collaborating with Bangor University to set up a project to use extended type theories, including a notion of type classes (Topic D) as a basis for symbolic computation to implement mathematics.