CLICS II

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

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

1st Periodic Progress Report October 8th, 1993

DRAFT – DO NOT DISTRIBUTE

Contents

1 Executive summary 3 1.1 Milestones and Deliverables . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 External Contacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Resources . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Update on the worldwide state-of-the-art 6

3 Workpart Summaries 7 3.1 Progress on Deliverables . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 Emergent Themes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.3 Proposed deliverables for Milestone 2 . . . . . . . . . . . . . . . . . . . . 11 3.4 Site Management Report for Imperial . . . . . . . . . . . . . . . . . . . 13 3.5 Site Management Report for Aarhus . . . . . . . . . . . . . . . . . . . . 15 3.6 Site Management Report for CAIMENS . . . . . . . . . . . . . . . . . . 17 3.7 Site Management Report for Cambridge . . . . . . . . . . . . . . . . . . 18 3.8 Site Management Report for Chalmers . . . . . . . . . . . . . . . . . . . 20 3.9 Site Management Report for Genova . . . . . . . . . . . . . . . . . . . . 22 3.10 Site Management Report for Darmstadt . . . . . . . . . . . . . . . . . . 24 3.11 Site Management Report for Manchester . . . . . . . . . . . . . . . . . . 27

4 Deliverables Overview 33

5 Deliverables 35 5.1 Report on Topic A: Sequentiality and Stability . . . . . . . . . . . . . . 35 5.2 Report on Topic B: Duality and Domain Theory . . . . . . . . . . . . . 40 5.3 Report on Topic C: Logic of Inductive and Recursive Datatypes . . . . . 49 5.4 Report on Topic D: Subtypes and polymorphism in higher order languages 54 5.5 Report on Topic E: Higher Order Modal Program Logics . . . . . . . . . 59 5.6 Report on Topic F: Monadic Programming Language Semantics . . . . . 66 5.7 Report on Topic G: Applied Linear Logic and Concurrency . . . . . . . 72 5.8 Report on Topic H: Computational Content of Classical Proofs . . . . . 79 5.9 Report on Topic I: Symbolic Computation . . . . . . . . . . . . . . . . . 83 5.10 Appendix A: A Categorical Abstract Machine for the Calculus of Con-

structions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 5.11 Appendix B: Report on implementation of LiLac . . . . . . . . . . . . . 86 5.12 Report on Workshop on Evaluation Logic and Synthetic Domain Theory 88 5.13 Preliminary Programme of Workshop on Games, Logic and Processes . 90

Chapter 1

Executive summary

1.1 Milestones and Deliverables

The CLICS II project started on October 1st 1992. The first Milestone occurs after 12 months. The first Review meeting will take place in Marseille on October 8th 1993.

As set out in Chapter II of the Technical Annex, the Workplan is structured into nine research topics, A through I. The main deliverables, as specified in Section II-2.2 of the Technical Annex, comprise detailed accounts of progress on each of these topics, written by the “Topic Leader”. These are contained in Chapter 5 of this report. Each Topic progress report references the relevant papers produced within the project during the review period; a selection of these are included as an appendix to this report. The progress on the specific deliverables targeted for Milestone 1 (see pages 27–28 of the Technical Annex) is summarised in Section 3.1 of this report.

The overall picture is that there has been very considerable progress made on all the targeted deliverables, and indeed far more has been done than was anticipated in the Technical Annex. Some particularly striking results are highlighted in Section 3.1, and some major themes which have emerged in the course of the first year of the project are identified in Section 3.2. A provisional specification of deliverables for the second project Milestone is set out in Section 3.3; this will be revised in the light of our discussions at the project Business meeting, and of the reviewers’ comments, and the revisions will be incorporated in the final version of this report.

Our general assessment is that the first year of the project has been very successful; a great deal of high-quality research has been done, and some striking advances which have attracted considerable international attention have been made. An important ingredient in the success of the project has been the collaborative aspect. A number of intensive interactions and exchanges of personnel between sites have greatly accelerated progress. Details are given in the Management Summaries in Chapter 3.

1.2 External Contacts

The two main ESPRIT BRA projects with some overlap of personnel and content with CLICS II are Types and CONFER. Specifically, Coquand and Dybjer at Chalmers participate in Types, while Abramsky at Imperial and Curien at CAIMENS participate in CONFER. These contacts have been stimulating and valuable. So far there has been more cross-fertilisation between Types and CLICS II (both of which are continuations of projects from the first round of ESPRIT) than between CLICS and CONFER. However, Abramsky’s work on Interaction Categories, which forms his contribution to CONFER, is directly based on his previous work on Linear Logic done under the auspices of CLICS I, and we expect further interactions as the projects proceed.

There has been considerable activity by members of the project as regards information dissemination. Important monographs and advanced textbooks have been published within the last year or are forthcoming: the revised and expanded version of Curien’s Categorical combinators, sequential algorithms and functional programming, Winskel’s Formal Semantics of Programming Languages, Crole’s Categories and Types, Taylor’s Domains and Duality. There is also a major contribution by project members to the Handbook of Logic in Computer Science being published by Oxford University Press. Abramsky is one of the editors; and there are forthcoming chapters on Domain theory by Abramsky and Jung, Full Abstraction by Ong, and Categorical logic by Pitts. An invited tutorial lecture by Pitts on “Bisimulation and Coinduction” was given at LiCS 93 in Montreal. Project members have given invited lectures at a number of leading international meetings. Two of the three non-U.S. invited speakers at the forthcoming North American Jumelage meeting to be held at SRI on October 14-16 1993 are CLICS II participants (Abramsky and Moggi); Abramsky is the only European invited speaker at the TACS conference in Japan in April 1994.

1.3 Resources

We give aggregated information on resources in person months used and forecast. The forecast figures are based on the tables on pages 26 and 27 of the Technical Annex. The actual figures are based on the Site management reports contained in Chapter 3 of this document. Note that these figures include (and indeed are predominantly made up of) non CEC-funded labour.

Topic  A  B C  D  E F  G H  I
Imperial  10  3.5  10 1.5  25
Aarhus  10 6.5 3.5  8.5  28.5
Principal CAIMENS 12.5 3.5  1.25  4  4 25.25
sites  Cambridge  5 3.5 6  6 2.4 2.5  1.2  26.6
Genova  1.5  1.5 1.5  3 1.8  0.6  9.9
Chalmers  6  4 2.4  12.4
Darmstadt  9  6  15
Associate GMD  3.5  0.5  4
sites  Manchester  2.5 4  2  1.5 1.6  11.6
Sussex  3.5  1.5  1.4  6.4
Total man-months 41.5 35.5 21 6.25 12.5 5.6 25.5 7 9.8 165.65

Forecast use of person-months

Topic A B C D E F G H I
Imperial  12 9  3  9  2 35
Aarhus  7 7  3  15  32
Principal CAIMENS 10 6  3  4  4 27
sites  Cambridge 5 3 2  3 7 3  3 26
Genova  3 3 2 3  11
Chalmers  12  14 12 38
Darmstadt 4 17  21
Associate GMD
sites  Manchester  3 3 3  3 3 15
Sussex  4  4
Total man-months 38 45 17 16 9 9 48 15 12 209

Actual use of person-months

Update on the worldwide state-of-the-art

As mentioned in Section I-4 of the Technical Annex (page 9), the CLICS project comprises a considerable proportion of the worldwide state of the art over much of the range of topics it addresses. Our work on sequentiality, Synthetic Domain theory, game semantics, and the application of point-free topology to extracting computational content from classical proofs, seems clearly in advance of any comparable work we know of elsewhere. Our work on Linear Logic and its Computer Science applications, parametric polymorphism, inductive and recursive types, topological and categorical generalizations of Domain theory, and the semantics of local storage is fully abreast of current work worldwide, and we have excellent contacts with the leading workers in these fields, e.g. Girard, Reynolds, Freyd, Plotkin and Scott. We will continue to follow the state of the art closely, and to promulgate our own contributions to it, but at present we see no reason to modify the general course of the project in the light of developments elsewhere.

Workpart Summaries

Scientific Workpart Summary

In this summary, we will overview the progress made on the deliverables described in Section II-2.2 of the Technical Annex.

3.1 Progress on Deliverables

Significant progress has been made on all the items mentioned in the Deliverables for Milestone 1 in Section II-2.2 of the Technical Annex. In many cases, actual progress has significantly exceeded what was anticipated there.

Topic A

Connections between Linear Logic, games and sequential algorithms The work of Abramsky and Jagadeesan, Hyland and Ong, Lamarche and Curien has established a wealth of precise results, so that this area is now much better understood. Particularly striking results here are the Full Completeness Theorems of Abramsky and Jagadeesan and Hyland and Ong, and Lamarche’s use of games to give correctness criteria for proof-nets for additives and exponentials. Curien has made a detailed study of the connection between game semantics and the sequential algorithms model of Berry and Curien, and formulated an elegant notion of symmetric algorithm.

Full Abstraction Results for variations of PCF This area has seen some spectacular advances just over the last few months. The long-standing Full Abstraction Problem for PCF itself (which was highlighted as particularly challenging and fundamental in the Risk Assessment in Section II-1 of the Technical Annex) has been solved. The first major step towards this was taken, independently, by Abramsky, Jagadeesan and Malacaria and by Hyland and Ong, in constructing an intensionally fully abstract model in Abramsky’s terminology, which captured PCF definability. The further step to the purely semantic construction of the (order-extensional) fully abstract model of PCF was subsequently taken by Abramsky, Jagadeesan and Malacaria, using the notion of intrinsic preorder, which has also played an important rôle in Synthetic Domain Theory elsewhere in the project.

Topic B

Categorical Domain theory, bagdomains Vickers has continued to develop the view of topos theory as observational logic, and hence as a possible foundation for formal specifications, while Johnstone has made substantial contributions to the mathematical foundations, directly stimulated by Vickers’ work on bagdomains.

Duality theory for stable domains There have been substantial contributions by Malacaria on Stone duality for stable and strongly stable functions, by Erhard on hypercoherences as a model of Classical Linear Logic with the associated cartesian closed category based on strongly stable functions, by Bucciarelli on event structure representations of domains with coherence, and by Winskel on connections between dI-domains and Petri nets, and on a linear decomposition of bidomains.

Topic C

Proof principles for inductive and coinductive types There has been progress on type-theoretic foundations for inductive and coinductive types by Coquand and Dybjer. They have also made substantial use of such types, e.g. in developing constructive proofs in point-free topology. Pitts has formulated proof principles for mixed-variance recursive types in a domain-theoretic setting. These are closely related to Freyd’s ideas on algebraic compactness, and give the most general principles yet found for reasoning about recursive types. Moreover, these techniques have found significant application, e.g. in proofs of computational adequacy.

Topic D

Semantic criteria for parametric polymorphism Rosolini has developed a general approach to constructing parametric models from arbitrary categorical models of polymorphism. This unifies many previously known specific constructions, and should provide a good framework for a more systematic understanding of the semantics of parametricity. This construction should also apply to subtyping; indeed, it has become clear in recent work that subtyping can be seen as a special case of parametricity. Curien, in joint work with Abadi and Cardelli, has developed a formal calculus for reasoning about parametric polymorphism. This provides a useful vehicle for translating semantic insights into proof principles, much as with LCF vis-a-vis Domain theory.

Semantics for overloading and subtyping in object-oriented languages There has been little work done on this topic within the review period. We expect to build on the foundational work on subtyping mentioned above in order to address this topic at a later stage in the project.

Topic E

Evaluation logic for references There has been substantial progress by Moggi on the general theory of Evaluation logic, and on the specific problems arising from references and local state. There have been striking interactions with the work on Synthetic Domain theory, with major contributions by Moggi and Taylor.

Topic F

Monadic semantics for references Pitts and Stark have isolated the key problematic features of local dynamic allocation in the new-calculus, and studied this calculus intensively in both operational and monadic denotational semantic frameworks. They have developed a powerful proof principle for this calculus based on a suitable version of logical relations. However, the calculus has proved to be extremely subtle, showing the complexity of the computational concepts being analyzed, and a definitive semantic analysis has not yet emerged. Nevertheless, we believe that the crystallization of the issues involved in understanding dynamic allocation is of great value in its own right; and we anticipate substantial further progress on this topic in the remainder of the project.

Topic G

Game semantics for Linear Logic, full completeness results Abramsky and Jagadeesan introduced the notion of full completeness: a categorical model for a logic, such that each morphism in the category is the denotation of a unique cut-free proof. They developed a history-free game semantics for Classical Linear Logic, and proved Full Completeness theorems for Multiplicative Linear Logic with the MIX rule, and for (intuitionistic) simple types. Hyland and Ong refined the Abramsky-Jagadeesan model for the multiplicatives to obtain a Full Completeness theorem for Multiplicative Linear Logic without MIX.

Connections with type theory and concurrency Winskel and Engberg have proved a completeness theorem for Linear Logic with respect to an interpretation in Petri Nets they had previously introduced. Linear Logic provides a very expressive formalism for describing properties of nets under this interpretation.

Topic H

Game semantics for Classical logic Coquand has given a game semantics for classical arithmetic which gives a process interpretation of cut-elimination, and a new perspective on how computational content can be extracted from classical proofs. There is also a link with Linear Logic via a connection with Blass’ game semantics.

Computational content of classical proofs Coquand and his students have continued Coquand’s extensive work on extracting computational content from classical proofs using mathematical tools from point-free topology, and logical tools from inductive definitions in type theory. Connections are also beginning to emerge between this work and the game semantics.

Topic I

Implementation of a CAM for CoC This has been done by Eike Ritter, and will be available for demonstration at the review.

Implementation of a functional language based on Linear Logic This has been done by Ian Mackie, and will be available for demonstration at the review.

It should be emphasized that the work mentioned above is only that which is most directly related to the deliverables for Milestone 1 as specified in the Technical Annex. A great deal of additional work has been done under the aegis of CLICS II, including many important contributions to the overall aims of the project. A full account will be found in the Topic Reports in Chapter 5.

3.2 Emergent Themes

It is to be expected in a project at the foundational level of CLICS II that new themes and topics may emerge or become more prominent during the course of the project. (See the dicussion in the first paragraph under Risk Assessment on page 17 of the Technical Annex.) It is important to keep such developments under review, since they clearly can, and should, influence the evolution of the Workplan. We see particular opportunities for rapid advance, and for interactions between different strands of the project, arising in the following areas:

1. Game semantics. This cuts across topics A, G, H, and has potential interactions with most of the other topics. The first year of the project has seen striking advances in Full Completeness theorems for various logics (topic G), full abstraction results for PCF (topic A), and the computational interpretation of Classical logic (topic H). A first task for the next review period is to relate the first two of these strands (whose inter-relationship is already well understood) to the third. In addition, we see considerable potential for game semantics of polymorphic and recursive types (topics C and D), and of dynamic allocation (topic F). In the light of the progress on applications of games to sequentiality, we also plan to investigate a notion of “sequential realizability” based on games; this should provide the right setting for an analysis of the “logic of sequentiality”, and may also provide a very attractive setting for Synthetic Domain theory (topic B).

Thus games offer considerable promise, both as a unifying theme for the project as a whole, and as a vehicle for some specific key technical advances.

2. Synthetic Domain Theory and Evaluation Logic. There have been very lively interactions between these two strands of the project. Although definitive results have not emerged yet, it seems some exciting progress could be made.

3. Semantics and Logic of dynamic allocation. The work already done within the project has reached the stage where the key problems and issues have been isolated and crystallized, to the point where a definitive solution seems at least possible. The significance of this would be to open up the world of state-based imperative programming, combined with all the structural facilities of functional programming, to logical and semantical analysis of a quality comparable to that which currently exists for purely functional languages.

3.3 Proposed deliverables for Milestone 2

As stipulated in the Technical Annex page 28, we set out proposed deliverables for Milestone 2 in this report. The deliverables set out below are provisional; they will be revised in the light of our discussions at the Business meeting, and of the reviewers’ comments at the first review; the revisions will be incorporated into the final version of this report.

Topic A Full abstraction results for extensions of PCF, e.g. with ML-style polymorphism. Connections between strongly stable function models and game semantics. Sequential realizability and the logic of sequentiality.

Topic B Development of Synthetic Domain Theory as a setting for Evaluation Logic. Extension of the semantic approach to strong normalization arguments.

Topic C Applications of mixed inductive-recursive definitions to the internalization of normalization arguments in type theory. Categorical analysis of constructive infinite objects and non-well-founded sets.

Topic D Develop the general theory of parametric models of polymorphism. Study models of subtyping within the same framework, and consider applications to the semantics of object-oriented languages.

Topic E Find sound and complete axiomatizations for the semantics of necessity in Evaluation Logic. Incorporate proof principles for inductive and coinductive types developed by Pitts into Evaluation Logic. Experiment with interpreting other program logics in Evaluation Logic.

Topic F Develop a monadic semantics for the Store calculus, and prove computational adequacy (possibly using the new techniques developed by Pitts in his work on Topic C). Develop a game semantics for dynamic allocation, and also for “Idealized Algol”.

Topic G Full completeness theorems for larger fragments of Linear Logic, and for fragments of Intuitionistic and Classical Logic via translations into Linear Logic. Further investigation of categorical models of bisimulation and refinement.

Topic H Develop game semantics for classical analysis, and investigate applications to the extraction of computational content from classical proofs. Study the connection between game semantics for Classical logic and for Linear Logic and PCF.

Topic I Further development of higher dimensional rewriting.

Management Workpart Summary

3.4 Site Management Report for Imperial

People working on the project

Permanent members of staff : Samson Abramsky has contributed about 6 man-months. Steve Vickers (Lecturer) has contributed about 3 man-months. Abramsky’s time was made available by funding from CLICS II.

SERC-funded Research Fellows: Paul Taylor (6 man-months), Roy Crole (3 manmonths).

DFG-funded Visiting Research Fellow: Michael Huth (3 man-months).

SERC-funded Research Assistants: Radha Jagadeesan (6 man-months), Pasquale Malacaria (6 man-months).

SERC-funded Research student: Ian Mackie (2 man-months).

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Abramsky.

These people made contributions to the following Topics in the project Workplan: Topic A: Abramsky, Jagadeesan, Malacaria. Topic B: Taylor, Vickers, Huth. Topic E: Crole. Topic G: Abramsky, Jagadeesan, Lamarche. Topic I: Mackie.

Interaction with other sites

Imperial has had important interactions with four other project sites during the review period:

1. Cambridge. The Cambridge and Imperial sites organized a joint seminar on Game Semantics which met about every two weeks, alternating between the two sites. This is continuing into the next review period.

2. CAIMENS. Lamarche and Malacaria both took up positions at Imperial, having previously worked at ENS. This has been very helpful in maintaining the flow of ideas and contacts. Also, Curien’s work on games and sequential algorithms refers strongly to the work of Abramsky and Jagadeesan and Lamarche. We have also begun to make connections between the work at Imperial on game semantics, and the work by Bucciarelli and Erhard on strongly stable functions. We intend to pursue this link further during the next review period.

3. Genova. We had visits from Moggi and Rosolini, and Taylor visited Genova. Together with the project workshop on Synthetic Domain theory and Evaluation Logic at Cambridge, this sparked some very lively interactions between the work on SDT and Evaluation Logic. Taylor set up an electronic mailing list as a forum for the ensuing discussions, and this has proved very effective.

4. Darmstadt. Abbas Edalat and Paul Taylor visited Darmstadt from Imperial during the review period. Michael Huth has now taken up a five-year research position at Darmstadt. Abramsky and Jung are writing a chapter on Domain theory together for the Handbook of Logic in Computer Science.

In addition, Abramsky and Coquand at Chalmers had some preliminary discussions about connections between their work on game semantics. We intend to explore this link more intensively during the next review period.

Conferences attended

The following conferences and workshops contained presentations of work done on the project at the Imperial site.

Foundations of Software technology and Theoretical Computer Science, New Delhi, India, December 1992.

51st Peripatetic Seminar on Sheaves and Logic, Valenciennes France, February 1993. Mathematical Foundations of Programming Semantics IX, New Orleans, April 1993. Linear Logic Workshop, Cornell, June 1993. Workshop on Interactions between Category Theory and Computer Science, Schloss

Dagstuhl Germany, July 1993.

Category Theory and Computer Science, Amsterdam, September 1993.

Publications

S. Abramsky and R. Jagadeesan, Games and Full Completeness for Multiplicative Linear Logic. Extended abstract appeared in Proceeding of FSTTCS 92, Springer LNCS vol. 652. Full version to appear in Journal of Symbolic Logic. Roy Crole, Categories and Types, Cambridge University Press, 1993. Michael Huth, Linear Lattices, Proceeding of MFPS 93, Springer LNCS. To appear. Francois Lamarche, On Additive-Multiplicative Linear Logic, submitted to Proceedings of 1993 Linear Logic Workshop. Ian Mackie, LiLac: a functional programming language based on Linear Logic, to appear in Journal of Functional Programming. Steve Vickers, Geometric logic in Computer Science, in Proceedings of Theory and Formal Methods 1993, Springer Workshops in Computing, 1993.

Problems

The only problem encountered concerned employment of labour for the project. Since the CEC has only guaranteed funding for the first 15 months of the project, any research assistant could only have been employed on an unsatisfactorily short term contract of 12 months (given the delays by CEC in issuing the contracts). Such short term contracts make retention of high quality research workers almost impossible. We therefore decided that the maximum benefit from the project funds would be obtained by using them to release Abramsky’s time to work on the project.

3.5 Site Management Report for Aarhus

Staff and students Sergei Soloviev a lecturer from the University of St Petersburg has been employed by CLICS II as a researcher from January 1993 (publications [21, 22]). Claudio Hermida has just joined the project from September 1 1993, staying for a year if funding continues. Jaap Van Oosten is to join the group from January 1 1994, employed by the new Danish-funded research centre BRICS, of which Winskel is to be Director. The PhD work of Torben Brauner, Bettina Sörensen and Gianluca Cattani is within the areas of CLICS II. Winskel’s MSc student Henrik Enström is completing a thesis on synthetic domain theory. Two MSc students Hans Jacob Pedersen and Poul Christensen have completed an MSc, under Winskel’s supervision, on a categorical reformulation of Lamport’s Temporal Logic of Actions. At Aarhus Anders Kock has been bolstering our knowledge of topos theory in a course based on MacLane and Moerdijk’s recent book on sheaves, geometry and logic.

Visits Bettina Sørensen’s work using ideas from category theory to include time in domains was boosted by Winskel’s visit to Paris to discuss with Pierre-Louis Curien and Thomas Ehrhard—the former has a semantics for linear logic in concrete domains. Another PhD student, Torben Brauner visited Cambridge for two weeks in the Spring to consult with Martin Hyland, Valeria de Paiva, Gavin Bierman and others on categorical models for Linear Logic. Gianluca Cattani, previously a student of Pino Rosolini, has become a PhD student at Aarhus, with Winskel as supervisor. Vladimiro Sassone (Pisa), Thiagajan (Madras) and Pino Rosolini (Genoa) have visited categorical models for concurrency and refinement. Winskel’s lectures at Banff, Canada, have led to fruitful (subsequently email) collaboration with André Joyal (see [16]). There have been a number of publications at international conferences (notably MFCS and LICS). MSc student Henrik Enström is completing a thesis on synthetic domain theory.

Aarhus publications in CLICSII Bibliography

[1] Cattani, G., Modelli categoriali per la logica lineare. Tesi di laurea, Dipartimento di Matematica, Università di Parma, December 1992.

[2] Christensen, P., and Jacobsen, H-J., A reformulation of Lamport’s Temporal Logic of Actions. MSc project DAIMI, 1993.

[3] Degano,P-P., Gorrieri, R., and Rosolini, P., A categorical view of process refinement. In Procs. of the REX Workshop on Semantics: Theory and Applications (J. de Bakker, W.-P. de Roever, G. Rozenberg ed.), volume 666 Lectures Notes in Computer Science, 1992, pag. 138–154. Springer-Verlag.

[4] Engberg,U., and Winskel, G., Completeness results for linear logic on Petri nets. Extended abstract in proceedings of MFCS 93, Poland (1993).

[5] Engberg,U., and Winskel, G., Completeness results for linear logic on Petri nets. Full version of above, submitted to Annals of Pure and Applied Logic. Available as DAIMI PB 435, April 1993.

[6] Joyal, A., Nielsen, M., and Winskel, G., Bisimulation and open maps. Extended abstract in LICS 93 proceedings. A full version is being written for a LICS 93 special issue of Information and Computation.

[7] Sassone, V., Nielsen, M., and Winskel, G., A classification of models for concurrency. Submitted to CONCUR 93.

[8] Sassone, V., Nielsen, M., and Winskel, G., Deterministic behavioural models for concurrency.To appear in proceedings of MFCS 93, Poland (1993).

[9] Nielsen, M., and Winskel, G., Trace structures and other models for concurrency. Invited chapter for the “Trace Book”, editors Diekert, V., and Rozenberg, G.

[10] Soloviev, S., Reductions in Intuitionistic Linear Logic (extended abstract). In CTCS (Category Theory and Computer Science) Proceedings, Amsterdam, 7-10 September 1993.

[11] Soloviev, S., A Complete Axiom System for Isomorphism of Types in Closed Categories. In proc of LPAR-93 S.Petersburg, Published in LNAI (Lect.Notes in Art.Int.) v.698, 1993.

[12] Winskel, G. and Nielsen, M., Models for concurrency. To appear as a chapter in the Handbook of Logic and the Foundations of Computer Science, Oxford University Press, 1994.

3.6 Site Management Report for CAIMENS

People working on the project

1. Pierre-Louis Curien, Laboratoire d’Informatique de l’Ecole Normale Supérieure, Paris. Games, symmetric sequential algorithms and linear logic. Full abstraction for observably sequential languages, with Felleisen.

2. Yves Lafont, Laboratoire de Mathématiques Discrètes, Marseille. Interaction nets, geometry of symbolic computation.

3. Antonio Bucciarelli, Laboratoire d’Informatique de l’Ecole Normale Supérieure, Paris. Strong stability, event structures for dI-domains with coherence.

4. Pasquale Malacaria, now at Imperial College, London. Stone duality for stable and strongly stable functions, games semantics of linear logic and PCF (at London).

5. Thomas Ehrhard, Institut Gaspard Monge, Noisy-le-Grand and L.I.T.P., Unversité Paris 7. Strong stability, hypercoherences.

Interaction with other sites Pierre-Louis Curien has visited Cambridge in february 93 and has had a lot of e-mail interactions with Cambridge and Imperial College about sequentiality and games.

Thomas Ehrhard has attended the workshop on Synthetic Domain Theory and Evaluation Logic held at Cambridge on January 93.

Conferences attended The following conferences and workshops contained presentations of work done on the poject at the CAIMENS site:

• Peripatetic Seminar on Sheaves and Logic, Cambridge, November 1992.

• Mathematical Foundations of Programming Semantics IX, New Orleans, U.S.A., April 1993.

• Linear Logic Workshop, Cornell, U.S.A., June 1993.

• Interactions between Category Theory and Computer Science, Schloss Dagsthul, Germany, July 1993.

Publications

• A. Bucciarelli, T. Ehrhard, Sequentiality in an extensional

framework, to appear in Information and Computation.

• A. Bucciarelli, Another approach to sequentiality: Kleene’s unimonotone functions, to appear in Proc. MFPS IX.

• R. Cartwright, P.-L. Curien and M. Felleisen, Fully abstract models of observably sequential languages, to appear in Information and

Computation.

• T. Ehrhard, Hypercoherences: a strongly stable model of linear logic, to appear in Mathematical Structures in Computer Science.

• T. Ehrhard, Projecting sequential algorithms on strongly stable functions, to appear in Annals of Pure and Applied Logic.

3.7 Site Management Report for Cambridge

People working on the project Permanent members of staff : Andrew Pitts and Martin Hyland have each contributed about 4 man months. Peter Johnstone has contributed 1 man month.

Contract research workers: Eike Ritter has been employed as a Research Associate by the project since January 1993, and so has contributed 9 man-months so far. Luke Ong (Research Fellow) has contributed about 3 man months. Valeria de Paiva is employed full time on a SERC-funded research project whose results have also contributed to this project.

Research students: Nick Benton, Gavin Bierman, Monica Nesi, Joshua Ross and Ian Stark have each contributed about 1 man month.

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Eike Ritter.

These people made contributions to the following Topics in the project Workplan: Topic A: Hyland, Ong.

Topic B: Hyland, Johnstone. Topic C: Pitts. Topic E: de Paiva, Pitts, Stark. Topic F: Pitts, Ritter, Stark. Topic G: Hyland, Benton, Bierman, de Paiva, Ross, Stark. Topic I: Nesi, Ritter.

Interaction with other sites The Cambridge site hosted a project workshop on Synthetic Domain Theory and Evaluation Logic held on 9,10 January 1993.

The Cambridge and Imperial sites organized a joint seminar on Game Semantics which met about every two weeks, alternating between the two sites.

The following short visits were made:

28,29/11/93: visit of Pino Rosolini (Genova) to Cambridge. 4–10/1/93: visit of Eugenio Moggi (Genova) to Cambridge. 5/3/93: visit of Alan Stoughton (Sussex) to Cambridge. 21–24/3/93: visit of Andrew Pitts to Chalmers. 22-26/3/93: visit of Ian Stark to Genova. 30/4/93: visit of Matthew Hennessy (Sussex) to Cambridge. 10–16/5/93: visit of Eike Ritter to Chalmers. 7–13/6/93: visit of Eugenio Moggi (Genova) to Cambridge. 10–16/6/93: visit of Jan Ekman (Chalmers) to Cambridge. 2–14/8/93: visit of Joshua Ross to Aarhus. 29/9–4/10/93: visit of Martin Hyland to Genova.

Conferences attended The following conferences and workshops contained presentations of work done on the project at the Cambridge site. (Project funds were not used to cover attendance at items marked with a ∗.)

Logic at Work, Amsterdam, December 1993.

51st Peripatetic Seminar on Sheaves and Logic, Valenciennes France, February 1993. Typed Lambda Calculi and Applications, Utrecht, March 1993. ∗Mathematical Foundations of Programming Semantics IX, New Orleans, April

1993.

ACM Workshop on State in Programming Languages, Copenhagen, June 1993. ∗8th Annual IEEE Symposium on Logic in Computer Science, Montréal, June 1993. Workshop on Interactions between Category Theory and Computer Science, Schloss

Dagstuhl Germany, July 1993.

∗18th International Symposium on Mathematical Foundations of Computer Science, Gdańsk Poland, August 1993.

Category Theory and Computer Science, Amsterdam, September 1993.

Computer Science Logic, Swansea UK, September 1993.

Publications P. N. Benton, Strong Normalisation for the linear term calculus, University of Cambridge Computer Laboratory Technical Report No. 305, May 1993.

P. N. Benton, G. Bierman, V. C. V. de Paiva and J. M. E. Hyland, A Term Calculus for Intuitionistic Linear Logic, In M. Bezem, J. F. Groote (Eds), Typed Lambda Calculi and Applications, LNCS 664 (Springer-Verlag, 1993), pp 75–90.

G. M. Bierman, C. Meré and V. C. V. de Paiva, Intuitionistic Necessity Revisited. Proceedings of the Logic at Work Conference, University of Amsterdam. To appear as Chapter 13 of: Plos, Masuch and Marx (eds), Arrow Logics and Multimodal Logics (OUP, 199?).

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), pp 179-194.

J. M. E. Hyland and C.-H. L. Ong, Fair Games and Full Completeness for Multiplicative Linear Logic without the MIX-rule, preprint, 29pp.

P.T. Johnstone, Fibrations and partial products in a 2-category, Applied Categorical Structures, to appear.

A. M. Pitts, A Co-induction Principle for Recursively Defined Domains, Theoretical Computer Science (Fundamental Studies), to appear. (Available as Univ. Cambridge Computer Laboratory Tech. Rept. No. 252.)

A. M. Pitts, Relational Properties of Recursively Defined Domains. In Proc. 8th Annual Symp. on Logic in Computer Science (IEEE Computer Soc. Press, Washington, 1993), pp 86–97.

A. M. Pitts and I. D. B. Stark, On the Observable Properties of Higher Order Functions that Dynamically Create Local Names. (Preliminary Report.). In Proc. ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, 1993. Yale Univ. Dept. Computer Science technical report YALEU/DCS/RR-968, pp 31–45.

A. M. Pitts and I. D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or: What’s new?. In Proc. 18th Int. Symp. on Math. Foundations of Computer Science, Gdańsk, 1993, Lecture Notes in Computer Science Vol. 711 (Springer-Verlag, Berlin, 1993), pp 122–141.

E. Ritter, Categorical Abstract Machines for Higher-Order Typed Lambda Calculi. Ph. D. Thesis, University of Cambridge. Available as University of Cambridge Computer Laboratory Technical Report No. 297, April 1993.

Problems The only problem encountered concerned employment of labour for the project. Although the official project start date was 1 October 1992, delays in completion and signing of the contract with the CEC meant that the Research Associate working on the project (Eike Ritter) could only be employed commencing 1 January 1993. Since the CEC has only guarenteed funding for the first 15 months of the project, Ritter is employed on an unsatisfactorily short term contract of 12 months. Such short term contracts make retention of high quality research workers almost impossible: we are very likely to loose Ritter’s services to another employer before continued funding of the project is decided.

3.8 Site Management Report for Chalmers

People working on the project

1. Thorsten Altenkirch, 1 man-month; proofs of strong normalization, models of type theory, inductive types.

2. Carolyn Brown, 11 man-months; linear logic, categorical approaches to relational calculus and hardware verification; specification of concurrent systems using Petri

nets.

3. Catarina Coquand, 3 man-months; lambda calculus with explicit substitution and explicit names, Kripke models.

4. Thierry Coquand, 6 man-months; analysis of Van der Waerden’s theorem, normalization proofs, game-theoretical analysis of classical proofs.

5. Peter Dybjer, 6 man-months; inductive definitions and reflection principles, models of type theory, normalization proofs, categorical models of infinite objects.

6. Daniel Fridlender, 3 man-months; analysis of computational content of classical proofs.

7. Lars Hallnäs, 3 man-months; models of infinite objects.

8. Graham Hutton, 3 man-months; categorical approches to relational calculus and hardware verification;

9. Hugo Herbelin (ENS Lyon, INRIA-Rocquencvourt, adjoint member), 3 manmonths; connections between game-theoretical semantics and cut-elimination in sequent calculus.

Publications

1. C. Brown and D. Gurr, “Relations and Non-commutative Linear Logic”, to appear in the Journal of Pure and Applied Algebra

2. C. Brown and G. Hutton, “The Geometry of Relational Programs” draft paper (joint work with Graham Hutton of Chalmers).

3. C. Brown and G. Hutton, and “Allegories for Circuit Design”.

4. C. Brown, D. Gurr, and V. C. V. de Paiva “A Linear Specification Language for Petri nets”, to appear in Mathematical Structures in Computer Science.

5. C. Brown, D. Gurr, “Relations and Non-commutative Linear Logic”, to appear in JPAA.

6. Th. Coquand, “A proof of Higman’s lemma by structural induction” invited paper presented at the Takeuti’s conference, Luminy, July 1993.

7. Th. Coquand, “A constructive topological proof of Van der Waerden’s theorem”, draft paper.

8. Th. Coquand, “Another Proof of the intuitionistic Ramsey Theorem”, Theoretical Computer Science 115, (1993), 63-75.

9. Th. Coquand, “A Semantics of Evidence for Classical Arithmetic”, to appear in the Journal of Symbolic Logic.

10. P. Dybjer, “A general notion of simultaneous inductive-recursive definition in type theory”. Draft paper, 1993.

11. D. Fridlender, “Intuitionistic Ramsey Theorem, Formalizations and Programs”, Dissertation for the Licentiate Degree in Computer Science, autumn 1993.

12. H. Herbelin “Weak reduction in sequent calculus”, to appear as a Tech. Report, University of Lyon.

Interaction with other sites Andy Pitts and Eike Ritter from Cambridge visited Chalmers in March and May respectively.

Carolyn Brown, Peter Dybjer, and Lars Hallnäs visited the SDT-EL Workshop in Cambridge in January.

Carolyn Brown and Valeria de Paiva from Cambridge are preparing a joint paper on the classification of some substructural logic. Carolyn Brown has also written a joint paper with Doug Gurr and Valeria de Paiva entitled “A Linear Specification Language for Petri nets”.

Changes of plan Carolyn Brown was employed on the project and has participated in topic G (Applied Linear Logic) together with Graham Hutton. This participation was not planned in the initial proposal.

3.9 Site Management Report for Genova

People working on the project.

• Eugenio Moggi has been working mainly on Topic E and F, he has devoted about 5 man-months on the project and has produced the following publications and reports available via FTP: [2], [9], [10], [20].

• Giuseppe Rosolini has obtained some results in Topic D and G, has devoted about 6 man-months on the project and has produced the following publications : [10], [2], [6].

Interactions and travels. Interactions directly related to CLICS-II:

27/11-04/12/92 Rosolini visits Cambridge, Imperial College, and Aarhus
04-10/01/93 Moggi visits Cambridge
09-10/01/93 SDT-ELT Workshop in Cambridge
22-26/03/93 Stark visits Genova
01-30/04/93 Taylor visits Genova (CNR funding)
07-11/06/93 Moggi visits Cambridge and Imperial
29/09-04/10/93 Hyland, Streicher and Reus visit Genova

Attendance to conferences and workshops:

28-29/11/92 Rosolini at Peripatetic Seminar on Sheaves and Logic, Cambridge
19-23/07/93 Workshop on Interactions between Cat. Th. and Comp. Sci., Dagstuhl
07-10/09/93 Conference on Cat. Th. and Comp. Sci., Amsterdam
14-16/10/93 Moggi at North American Jumelage, SRI Menlo Park

Other relevant interactions^{1}:

28/12/92-02/01/93 Moggi visits Edinburgh
01-12/02/93 Cenciarelli visits Genova
04-13/02/93 Rosolini visits Utrecht
10-11/05/93 Rosolini visits Pisa
17-18/05/93 Rosolini visits Pisa
14-15/06/93 Meeting in Edinburgh
14-17/06/93 Moggi visits Edinburgh
16-17/09/93 Rosolini visits Pisa

1This include interaction with related project EC SCIENCE twinning ERBSC1*CT920795 on “Programming Language Semantics and Program Logics” and with EEC project MASK SC1 – CT92 – 00776.

Bibliography

[1] Pietro Cenciarelli and Eugenio Moggi. A Syntactic Approach to Modularity in Denotational Semantics. In: Proc. Conference on Category Theory and Computer Science, Amsterdam, 1993. CWI internal report.

(available as /theory/papers/Moggi/mod-sem.dvi from theory.doc.ic.ac.uk)

[2] P. Degano, R. Gorrieri and G. Rosolini. A categorical view of process refinement. In Procs. of the REX Workshop on Semantics: Theory and Applications (J. de Bakker, W.-P. de Roever, G. Rozenberg ed.), volume 666 di Lectures Notes in Computer Science, 1992, pag. 138–154. Springer-Verlag.

[3] 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.

(available via FTP from theory.doc.ic.ac.uk)

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

(available as /theory/papers/Moggi/elt.dvi from theory.doc.ic.ac.uk)

[5] E. Moggi. A general semantics for evaluation logic, 1993.

(available as /theory/papers/Moggi/elt2.dvi from theory.doc.ic.ac.uk)

[6] E. Moggi. A note on SDT in filter spaces, 1993.

(available as /theory/papers/Moggi/filter2.dvi from theory.doc.ic.ac.uk)

[7] G. Rosolini. Reflexive graphs and parametric polymorphism. To appear.

(available via FTP from theory.doc.ic.ac.uk)

3.10 Site Management Report for Darmstadt

3.10.1 People involved in CLICS II

Klaus Keimel, Professor Effort: 4 man-month

Project management at Darmstadt. Supervision of the thesis work by Schalk, Sünderhauf, Puhlmann, Kirch, Haack.

Achim Jung, Assistent Effort: 9 man-month Supervision of the thesis work done by Schalk, Sünderhauf, Puhlmann, Haack. Research on Topic A: The full abstraction problem for PCF. The lambda-definability

problem.

Research on Topic B: A comprehensive text on domain theory.

Publications: [JS92, JS93, JT92, JT93, AJ]

Andrea Schalk, Doctoral Student Effort: 12 man-month Research on Topic B: Generalised power constructions. Publication: [Sch93b, Sch93a]

Philipp Sünderhauf, Doctoral Student Effort: 12 man-month Research on Topic B: Quasi-uniform spaces in denotational semantics. Publications: [Sün92, Sün93]

Hermann Puhlmann, Doctoral Student Effort: 6 man-month Research on Topic B: Domain theoretic models of relational databases. Publications: [Puh93]

Christian Haack, Diploma Student Effort: 6 man-month

Research on Topic B: Diploma thesis on the hyperlimit construction in categories of domains.

Publication: [Haa93]

Olaf Kirch, Diploma Student Effort: 6 man-month Research on Topic B: Diploma thesis on the probabilistic powerdomain construction. Publication: [Kir93]

3.10.2 Activities

Conferences Cambridge Workshop on Synthetic Domain Theory: Andrea Schalk. Mathematical foundations of Programming Semantics, Tulane: Klaus Keimel. Typed Lambda Calculi and Applications, Utrecht: Achim Jung. Second Workshop of Science Project MASK, Amsterdam: Philipp Sünderhauf. Interactions of Category Theory and Computer Science, Dagstuhl: Achim Jung, Klaus Keimel. Mathematical Foundations of Computer Science, Gdansk: Hermann Puhlmann.

3.10.3 Visitors at Darmstadt

Kurt Sieber, Saarbrücken, Jon Riecke, Bell Labs, Pierre-Louis Curien, ENS Paris, Abbas Edalat, London, Paul Taylor, London.

[AJ] 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 ??, page 132 pp. Oxford University Press, ?? Draft.

[Haa93] C. Haack. Die hyperlimeskonstruktion. Master’s thesis, Technische Hochschule Darmstadt, 1993. Diploma thesis, 86 pp.

[JS92] A. Jung and A. Stoughton. Studying the fully abstract model of pcf within its continuous function model. Technical Report 7/92, University of Sussex, 1992.

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

[JT92] A. Jung and J. Tiuryn. A new characterization of lambda definability. Technical Report 1498, Technische Hochschule Darmstadt, 1992.

[JT93] A. Jung and J. Tiuryn. A new characterization of lambda definability. In M. Bezem J. F. Groote, editor, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 245–257. Springer Verlag, 1993.

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

[Puh93] H. Puhlmann. The snack powerdomain. In Mathematical Foundations of Computer Science, 1993. to appear.

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

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

[Sün92] Ph. Sünderhauf. Quasi-uniform completeness in terms of cauchy nets. Technical Report 1529, Technische Hochschule Darmstadt, 1992. 8 pp.

[Sün93] Ph. Sünderhauf. Constructing a quasi-uniform function space. Technical Report 1541, Technische Hochschule Darmstadt, 1993. 26 pp.

3.11 Site Management Report for Manchester

3.11.1 The Team

• Peter Aczel

• Gilles Barthe

• Yuxi Fu

• Barney Hilken

• David Rydeheard

• Harold Simmons

3.11.2 General

Yuxi Fu has returned to China. He obtained his Ph.D. here under David Rydeheard and has been working as an RA on CLICS-II. Much of his work is relevent to the Types project. Gilles Barthe has had his Ph.D. accepted and has been working as an RA on the Types project for eight months in the last year. He is now funded on the CLICS-II project. Barney Hilken has been working as an RA on an SERC project, with David Rydeheard. He is leaving to take up a post-doc position in Cambridge.

Reports and Abstracts

Acz93b Peter Aczel. ‘Schematic Consequence’. To appear in the book ‘What is a logical System’, edited by Dov Gabbay, Oxford University Press.

Abstract: The aim of this note is first to set up some general theory for discussing different aspects of the notion of a logic and then to draw attention to the schematic aspects of logic and suggest a way of capturing this aspect without making any committment to the kind of syntax a logic should have.

Sim93a Harold Simmons. ‘A Density Property of the Primitive Recursive Degrees’. Tech report UMCS-93-1-1 (33 pages) Submitted to TCS.

Abstract: The standard Ackerman function which is produced by diagonalisation to lie outside the class of primitive recursive functions is shown to be far from an optimal example of such a function. By slowing down the diagonalisation I producea whole continuum of functions which, in complexity, lie above the primitive recursive functions and below the Ackerman function. There is a dense set of these functions which have a rudimentary graph.

Sim93b Harold Simmons. ‘How to eliminate predicate variables’. Tech report UMCS-93-1-2 A slightly revised version of this will appear in J Logic and Computation under the title ”The monotonous elimination of predicate variables” (45 pages).

Abstract: I describe an algorithm which when given a sentence Γ involving universally quantified predicate variables, first reduces this sentence to a normal form Γ^{∗} and then, if Γ^{∗} satisfies certain extra restrictions, eliminates the predicate variables of Γ^{∗} to produce a predicate-free equivalent of Γ. This process may involve the introduction of skolem functions but in many cases does not (and so produces a more elementary version of Γ).

The algorithm eliminates the predicate variables by witnessing them with certain definable predicates. The choice of these predicates is guided by the shape of the normal form Γ^{∗}.

The algorithm was initially designed to deal with modal correspondence problems. In this respect it is an extension of Sahlqvist’s algorithm which produces first order equivalents of a wide class of modal formulas. The algorithm is illustrated by several examples from modal logic.

Sim93c Harold Simmons. ‘The glueing construction and lax limits’. To appear in Mathematical Structures in Computer Science (40 pages).

Abstract: Starting life as a way of reconstructing a topological space from a pair of complementary subspaces, the glueing construction has found employment in a wide range of different roles from the construction of free distributive lattices to a supporting part in the 2-categorical analysis of types theories. In this latter role the construction appears to be a fundamental factor in the behaviour of higher order proof theory. What is going on here? Before that can be answered we need at least a less ad hoc description of the construction.

In this paper I set down what is, I believe, the beginnings of a coherent account of the algebraic version of glueing. As well as the abstract theory I give a good selection of different examples to illustrate the diverse nature of the uses of the construction.

Sim93d Harold Simmons. ‘Logic and computation: Taking the Curry-Howard correspondence seriously’. A (preliminary version of a) set of lectures notes. Available on ftp from pub/applied_logic/logic-and-comp.ps (134 pages).

Contents:

Chapter 1 The basic proof systems of constructive propositional logic Chapter 2 Untyped combinator and lambda calculus Chapter 3 The Curry-Howard correspondence Chapter 4 Gödel’s T Chapter 5 The second order λ-calculus Appendix Some solutions (to the exercises)

Fu92 Yuxi Fu. ‘Topics in Type Theory’. Ph.D. thesis, Technical Report Series UMCS-92-11-1, Manchester University

Abstract: The thesis is mainly about semantics of type theory. We carry out an investigation into the semantics of logical frameworks using internal category theory. We argue that the treatment of object-variables as meta-variables adopted in most logical frameworks means semantically that the interpretations of an encoded object language constitute internal full subcategories of the models of the framework itself. This model theoretic result also suggests how one should code object langauges. The second part of the thesisis concerned with semantics of inductive types. A recursive model is given to the generalised inductive types. The interpretation uses some basic recursion theory and theory of inductive definitions. Then we define a different clas of (co)inductive types. A semantic investigation of these types is also carried out. Finally we show how to justify semantically the introduction of the generalised inductive types to the Calculus of Constructions. A model is constructed by ‘effectivising’ the classical set theoretical model. Finally, we give an account of what we think of type theory.

Fu93a Yuxi Fu. ‘Encodings in Polymorphism revisited’. Technical Report, University of Manchester, Dept of Computer Science, UMCS-93-6-4.

Abstract: We consider encodings in polymorphism with finite product types. These encodings are given in terms of I-algebras. They have the property that all canonical terms (ground terms) are normal terms. We transplant the proof of a well-known result to our setting abd show why weak recursion is admissible. We also show how to carry out the dual encodings using the existential quantifier.

Fu93b Yuxi Fu. ‘Understanding Inductive Types in Constructions’

Abstract: In this paper we extend the Calculus of Constructions with generalized inductive types. The extension is justified by showing that the usual set theoretical model can be effectivized. It is also pointed out that the model given in a published paper for a collection of inductive types in a different style is wrong.

Fu93d Yuxi Fu. ‘Categorical Properties of logical Frameworks’

Abstract: In this paper we give a new presentation of ELF which is well suited for semantic analysis. We introduce the notions of internal codability, internal definability, internal typed calculi and frame languages. These notions are central to our perspective of logical frameworks. We will argue that a logical framework is a typed calculus which formalises the relationship betwen internal typed languages and frame languages. In the second part of the paper we demonstrate the advantages of our logical framework by showing some categorical prperties of it and encodings in it. By doing so we hope to indicate a sensible model theory of encodings.

Fu93e Yuxi Fu. ‘CZF in Martin-Lof’s Type Theory without Identity Types’. Draft paper.

Abstract: Aczel’s interpretation of the constructive set theory CZF in Martin-Lof’s type theory uses the extensional indentity types. It is generally believed that these “types” do not belong to a type theory. In this short paper we show that Aczel’s interpretation goes through with the intensional identity types. Furthermore we show that the interpretation works even without identity types. On the way we will give a faithful understanding of CZF in a logical type theory, although in this case there is a question of the axiom of choice.

Fu93f Yuxi Fu. ‘A Note on Weak Fibrations’. Draft paper.

Abstract: In this note we record two technical results on weak fibrations. Firstly, it is demonstrated that a factorization system for weak fibrations does exist as long as we do not require the distinguished morphisms to form a category. Secondly, the indexed categorical counterpart of split weak fibrations are given. the weak indexed categories are lax functors satisfying compatibility and compositionality conditions.

Fu93g Yuxi Fu. ‘Recursive Models of General Inductive Types’. Technical Report, University of Manchester, Dept of Computer Science, UMCS-93-6-6.

Abstract: We give an interpretation of Martin-Lof’s type theory (with universes) extended with generalized inductive types. The model is an extension of the recursive model given by Beeson. By restricting our attention to PER model, we show that the strictness of positivity condition in the definition of generalized inductive types can be dropped. It therefore gives an interpretation of general inductive types in Martin-Lof’s type theory.

HR93a Barney P. Hilken and David E. Rydeheard. ‘A Theory of Classes: Proofs and Models’. Draft paper.

Abstract: We investigate the proof structure and semantics of theories of classes, 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. We establish normalisation results for proofs and use these results establish coherence of a categorical semantics for classes.

HR93a Barney P. Hilken and David E. Rydeheard ‘Logical Frameworks and Their Implementation: An Axiomatic Account’. Draft paper.

Abstract: We describe an approach to logical frameworks based on a categorical treatment of logic rather than on encoding logics in an appropriate type theory. This has several advantages including emphasizing the use of multiple logics and relationships between logics. Unlike the type theoretic approaches of ELF, ALF and Coq, it is not clear what it means to implement a logic in this categorical framework. To this end we have axiomatized a notion of ‘computable’ which covers the kinds of computation that are required to encode logics in a logical framework. We describe models of the axioms and show how to implement this framework as programs in the functional language Gofer.

Peter Aczel and Gilles Barthe have been developing some abstract algebra in the proofdevelopment system Lego. The process of creating readable machine-checked requires the use of new kinds of abstractions not used explicitly in informal mathematics. One such abstraction is the notion of class with subclasses, methods and methods inheritance, which capture elegantly overloading. Peter Aczel and Gilles Barthe have implemented a simulation of classes and methods in Lego; they have used this simulation to formalise some basic notions of abstract algebra; their package distinguishes between three levels of abstractions: the first level is the level of mathematical structures, such as sets, groups … The second level is the level of small categories, such as the category of sets. The third level is the level of the category of small categories.

In parallel an initial attempt to develop the theory of classes in type theory has been made: Peter Aczel has been using the formalism of Pure Type Systems to describe axiomatically the notion of class. Gilles Barthe will experiment further with the package and implement some further basic concepts: in particular, an adequate handling of substructures is required. The theory of classes will also been investigated further. Relevant papers are listed below.

Bar93a Gilles Barthe. ‘Developing Algebra in LEGO’. Draft report for the Turin workshop, January, 1993.

Abstract: This note discusses the formalisation of algebra in a proof-development system and particularly the formalisation of the unsolvability of the symmetric group over a discrete set of more than four elements. We give an outline of the proof we use (as it differs from the proof in textbooks) and provide a brief documentation of the lego files.

Acz93a Peter Aczel. ‘Galois: A Theory Development Project’.

Abstract: This very briefly outlines the Galois proposal, to implement Galois theory in Lego. It contains an appendix that consists of an edited Lego file that first defines the category of sets and then the group of permutations on a set.

Bar93b Gilles Barthe. ‘Presentations of order-sorted specifications’, Ph.D. thesis, Manchester, 1993.

Abstract: Equational logic has been used in computer science to specify data types; it has been generalised so as to allow terms to have sorts; however, strong typing appears to be too inexpressive to specify data types such as natstack; an elegant approach that avoids many of the shortcomings of many-sorted logic has been developed by Goguen and Meseguer and the OBJ group, is based on ordersorted logic. The computational properties of order-sorted logic have been thoroughly studied; however, nobody has tried, to our knowledge, to establish the equivalence between the categorical presentations of specifications (categories of models, monads, algebraic theories). It is one of the purposes of this paper to establish such an equivalence. Moreover, we introduce set-theoretical structures which can be used as presentations of order-sorted specifications: generalised composita. They have been introduced by Aczel, and provide an axiomatic approach to substitution. Building upon Aczel’s work, we develop further the theory of generalised composita and study some of their applications. In particular, we use generalised composita to tie up the different approaches to substitution undertaken by linguists, computer scientists and logicians.

Bar93c Gilles Barthe. ‘Formalising Galois theory’. Draft

Abstract: This preliminary report introduces the Galois project, its motivations and its ambitions. It presents a possible approach to Galois theory and an analysis of the structure of the theory. In particular, we underline a possible modular decomposition of the theory.

Bar93d Gilles Barthe. ‘Foundations for the formalisation of algebra’. (Draft)

Abstract: This draft report is intended as a guide to the algebra file we have been developing in lego. Firstly, we find useful to justify some mathematical choices we have made in the course of formalising algebra. Secondly, we attempt to justify and illustrate the use of inheritance in formalising mathematics; we also introduce a method to capture inheritance in type theory: classes, as they are used in object-oriented languages. Thirdly, we document the file which we have produced, from sets to fields and vector spaces.

Deliverables Overview

The deliverables for Milestone 1 comprise the following:

1. Reports on each of the Topics A through I, each compiled by the Topic Leader. In the case of Topic A, the report was compiled by Thomas Ehrhard and Samson Abramsky, deputising for Pierre-Louis Curien, who is spending the academic year 1993-94 as a Visiting Professor at the University of Beijing. Also, the responsibility for Topics E and F, which are closely linked, was interchanged between Eugenio Moggi and Andrew Pitts.

Thus the list of reports and authors is as follows:

Report on Topic A: Sequentiality and Stability  Ehrhard/Abramsky
Report on Topic B: Duality and Domain Theory  Martin Hyland
Report on Topic C: Inductive and Recursive Types  Peter Dybjer
Report on Topic D: Subtypes and Polymorphism  Giuseppe Rosolini
Report on Topic E: Evaluation Logic  Eugenio Moggi
Report on Topic F: Monadic Semantics  Andrew Pitts
Report on Topic G: Applied Linear Logic  Glynn Winskel
Report on Topic H: Computational Content of Classical Proofs Thierry Coquand
Report on Topic I: Symbolic Computation  Yves Lafont

2. Two experimental implementations, by Eike Ritter of a categorical abstract machine for the Calculus of Constructions, and by Ian Mackie of a functional programming language based on Linear Logic, form part of the deliverables. These implementations will be available for demonstration at the Review meeting. Descriptions of these implementations by Ritter and Mackie are included as Appendices to the Report on Topic I.

3. A report on the first project Workshop on Synthetic Domain Theory and Evaluation Logic, which was held in Cambridge in January 1993. This was compiled by Martin Hyland.

4. A provisional programme for the second project Workshop, on Games, Logic and Processes, which will be held in Marseilles on October 4-7, immediately preceding the Review meeting.

In addition, a selection of the papers written within the project during the review period will be included as an Appendix to this Report in the material sent to the Reviewers.

Deliverables

5.1 Report on Topic A: Sequentiality and Stability

5.1.1 Strong stability

This notion has been introduced by Bucciarelli and Ehrhard in their article [4] as an alternative approach to sequentiality. In the models they build, programs (or proofs) are still interpreted by functions, like in the continuous or stable model. The situation here is very different from what happens with the models of sequential algorithms or games where the interpretations of programs contain a lot of informations about their internal behaviour.

The basic observation of Bucciarelli and Ehrhard is that sequentiality (of first order functions) can be expressed as a preservation property as follows. Consider the case of a monotone function N^{k} → N^{l}, where N is the usual flat domain of integers. Then let us say that a subset A of N^{k} is “linearly coherent” if it is non-empty and has the following property: for all i ∈ {1, …, k}, if all the elements of A have their i-th component defined (that is different from ⊥), then all these i-th components are equal. For instance, any non-empty and bounded subset of N^{k} is linearly coherent. But also (for k = 3), the set {(⊥, 1, 2), (2, ⊥, 1), (1, 2, ⊥)} is linearly coherent and unbounded. They have first proved (in a more general framework, not restricted to domains of the shape N^{k}) that f is sequential if and only if it sends linearly coherent sets on linearly coherent sets and commutes to the glb’s of linearly coherent sets.

They have then extended this kind of approach to higher order, considering domains (actually, dI-domains or qualitative domains) equipped with a notion of coherence. Such an object is a pair (X, CX) where X is a domain and CX is a set of finite and nonempty subsets (which are called the “coherent subsets”) of X satisfying some closure properties. A morphism between two such objects is then a continuous function between the underlying domains which sends coherent sets to coherent sets and commutes to the glb’s of coherent sets. They proved that the category defined this way is cartesian closed, which means that this new approach to sequentaility can be extended to higher order.

In order to compare this model with the usual Scott model of PCF, they have built a category of dI-domains equipped with coherence where each object is embedded in a Scott domain. This was necessary in order to reject certain “pathological” strongly stable functionals which have a non extensional behaviour. This notion of “extensionally embedded dI-domains with coherence” is similar to Berry’s notion of bidomains, but it is more restrictive on morphisms, and for this reason it has been possible to prove that the equational theory of this model equates more terms than the equational theory of the Scott’s model. This construction is presented in [5] and [7].

Trying to simplify the notion of “qualitative domain equipped with coherence”, Ehrhard observed then that a sufficiently large subclass of these objects could be described in a concise way by very simple structures that he called “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 has to contain all singletons. So a hypercoherence is simply an “unlabelled, unoriented and reflexive hypergraph”. Out of such a hypercoherence X one can define a domain and a coherence on the top of this domains, and all the constructions defined in [4], when performed on hypercoherences, give rise to hypercoherences. Furthermore, Ehrhard observed also that hypercoherences give a new model of linear logic (which is, only formally, similar to Girard’s model of coherence spaces). These objects are presented in [8].

Next, Ehrhard tried to connect the strongly stable model of PCF with its model of sequential algorithms. For this, he used an “abstract” theory of sequential algorithms that he had previously set up with Bucciarelli ([6]). With this tool, he could prove in [9] that any strongly stable function is the “extensional content” of a sequential algorithm, which means that, also at higher order, strong stability is sequentiality.

Simultaneously, Bucciarelli has extended the “hypercoherence” approach to dIdomains with coherence. More precisely, he has defined a notion of “hypercoherent event-structures” which behave wrt “dI-domains with coherence” (of a certain kind) exactly like standard event structures wrt dI-domains. It is a first step in the direction of a theory of “strongly stable domains”. This work is not yet published and is presented in [3].

5.1.2 Stone duality

Previous works of Abramsky have proved that Stone duality is relevant in the semantics of programming languages. This duality gives rise to an approach where “properties” are more important than “values”. However, Abramsky’s work was limited to the standard Scott semantics of functional languages. So a reasonable question was whether such an approach could be carried out for the stable semantics as well. Actually G.Q. Zhang had already in his thesis some results in this direction. However, an abstract notion of “locale” for stable functions was still lacking when Ehrhard and Malacaria addressed this problem. In [10] they proposed such a notion and proved that it satisfies the required conditions. The idea is to consider a meet-semilattice where some joins are allowed (essentially, the directed meets and the disjoint meets), and which is distributive for these joins (let us recall that a locale is a similar structure but where all joins are allowed). More details, as well as an extension to strong stability, can be found in his thesis [19].

5.1.3 Curien’s work on Games and Sequentiality

We offer a symmetric account of sequentiality, by means of symmetric algorithms, which are pairs of sequential functions, mapping data to data, and output exploration trees to input exploration trees, respectively. We use the framework of sequential data structures, a reformulation of a class of Kahn-PlotkinUs concrete data structures. In sequential data structures, data are constructed by alternating questions and answers. Sequential data structures and symmetric algorithms are the objects and morphisms of a symmetric monoidal closed category, which is also cartesian, and is such that the unit is terminal. Our category is a full subcategory of categories of games considered by Lamarche, and by Abramsky-Jagadeesan, respectively.

Following Lamarche, we construct a comonad corresponding to contraction. We define this comonad via an adjunction between the category of symmetric algorithms and the old cartesian closed category of sequential algorithms, defined in the late seventies by the author and Gerard Berry. Thus sequential algorithms model not only typed λ-calculus, but also intuitionistic affine logic. This work, while finding its roots in the study of sequentiality, presents striking correspondences with game-theoretic concepts, introduced by Blass in the early seventies in a very different context.

The aim of the present work is to offer a systematic connection between sequentiality and games. Also, the notion of symmetric algorithm appears to be new.

5.1.4 Games and Full Abstraction for PCF

The most spectacular advance in this area has been the solution of the long-standing Full Abstraction Problem for PCF: that is, to give a purely semantic account, independent of the syntax of PCF, of the fully abstract model for PCF. This happened in two stages. Firstly, Abramsky, Jagadeesan and Malacaria, and independently Hyland and Ong, introduced categories of games giving rise to intensionally fully abstract models of PCF, in Abramsky’s terminology; that is, models in which all compact elements are definable. However, these models are not extensional. Nevertheless, this should be seen as the key step towards the solution of the Full Abstraction problem. The definability result is actually in a direct line of descent from the Full Completeness concept introduced by Abramsky and Jagadeesan, and proved by them for Multiplicative Linear Logic with MIX and for Intuitionistic simple types with respect to their category of games; and which was subsequently refined by Hyland and Ong to yield a Full Completeness Theorem for MLL without MIX. See the Report on Topic G for further details. One additional ingredient was required to be added to the Abramsky-Jagadeesan category in order to yield the definability result for PCF: a classification of moves in a game as questions (requests for data) or answers (data values), orthogonal to the classification of moves as positive (by Player) or negative (by Opponent); and a well-bracketing constraint on strategies defined in terms of this new classification. This well-bracketing discipline excludes strategies corresponding to Cartwright and Felleisen’s catch and other non-local control constructs. Then the history-free constraint of Abramsky and Jagadeesan (which is expressed in alternative but apparently equivalent terms in Hyland and Ong’s model) ensures that the only information available to a functional about the behaviour of its argument is the value it returns. This excludes those strategies which violate extensionality; this is the key point which transcends the limitations of previous intensional models, in particular the sequential algorithms model of Berry and Curien.

The further step, to the explicit semantic construction of a cartesian closed category giving rise to the fully abstract model, was subsequently taken by Abramsky, Jagadeesan and Malacaria. A key rôle here was played by the notion of intrinsic preorder; a striking property of the AJM category is that this preorder coincides with the pointwise order on function spaces and products, without any additional assumptions. The proof of this makes full use of the underlying structure of (Classical) Linear types, even though the application is to Intuitionistic types.

The techniques and concepts giving rise to these results seem ripe for extensive further applications to richer sequential languages. In particular, it should be possible to combine Abramsky and Jagadeesan’s Full Completeness theorem for simple types (see the Report on Topic G) with the PCF results to get a fully abstract model for PCF extended with ML-style polymorphism. This would be of particular interest, since O’Hearn and Riecke have recently given a “fully abstract translation” of Reynolds’ Idealized Algol into this polymorphic PCF. Thus such extensions would also be of direct relevance to work on Topics D and F.

[Cur] P.-L. Curien, On the symmetry of sequentiality. Preprint, 1993.

[AJM1] S. Abramsky, R. Jagadeesan and P. Malacaria, Games and Full Abstraction for PCF: preliminary announcement, July 1993.

[AJM2] S. Abramsky, R. Jagadeesan and P. Malacaria, Games and Full Abstraction for PCF II: second preliminary announcement, September 1993.

[HO] M. Hyland and C.-H. L. Ong, Dialogue Games and Innocent Strategies: an approach to (Intensional) Full Abstraction for PCF, July 1993.

[B] A. Bucciarelli. Sequential models of PCF: some contributions to the domaintheoretic approach to full abstraction. PHD thesis, Università di Pisa, 1993.

[BE1] A. Bucciarelli, T. Ehrhard. Sequentiality and strong stability. LICS 91.

[BE2] A. Bucciarelli, T. Ehrhard. Extensional embedding of a strongly table model of PCF. ICALP 91.

[BE3] A. Bucciarelli, T. Ehrhard. A theory of sequentiality. To appear in TCS.

[BE4] A. Bucciarelli, T. Ehrhard. Sequentiality in an extensional framework. Submitted to Information and Computation.

[E1] T. Ehrhard. Hypercoherences: a strongly stable model of linear logic. To appear in Mathematical Structures in Computer Science.

[E2] T. Ehrhard. Projecting sequential algorithms on strongly stable function. To appear in Annals of Pure and Applied Logic.

[EM] T.Ehrhard and P. Malacaria. Stone duality for stable functions. CTCS 91.

[M] P. Malacaria. Deux contributions de la Dualité de Stone à l’informatique théorique. PHD thesis, Université de Paris VII, 1993.

5.2 Report on Topic B: Duality and Domain Theory

This report describes the work which has been done on Topic B of the Workplan in the first year of the project: this contributes to the project objectives in the area of Domain Theory. As anticipated, at this first milestone we report progress on Categorical Domain Theory and on Duality Theory for Stable Functions. In addition, considerable effort has been devoted to duality in the context of Synthetic Domain Theory (mentioned under Topic A in the proposal but appropriately reported here).

5.2.1 Categorical Domain Theory

As explained in the project proposal, we have reason to develop a variety of generalizations of domain theory. On the one hand we need more general order theoretic models (for example continuous as opposed to algebraic cpos); on the other we are motivated to move beyond the ‘topological’ case and develop a theory for the case of categories (as opposed to spaces) of points by the possible implications for specification languages, and the specific applications to building models for databases (via bag domains) envisaged by Vickers [30]. We report considerable and varied developments in the first of these areas in 5.2.1.1. Progress in the second of these areas has been adversely affected by the departure of project members; the progress we have made, and the difficulties we face are described in 5.2.1.2.

5.2.1.1 Categorical topology and Domain Theory

One substantial contribution of the project is represented by Schalk’s work on power domains, which is a further attack on the classical problem of non-determinacy. 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 [33] and Robinson [23]. In [25] 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 generalization (see [24] and [26]). (There is an interesting parallel with investigations of Johnstone [16] reported below.) Other power domains have also received attention. As proposed in the workplan we have worked on a setting for probabilistic power domains. Kirch’s thesis [18], supervised within the project by Keimel, presents a simple ‘functional analytic’ framework, in which a version of the Riesz representation theorem plays a role. Power domains are also involved in Sünderhauf’s recent work on quasi-uniform spaces [28] and [29] which builds on work of Smyth [27]. We expect further advances in all these areas by the 2nd milestone.

The question of the unique decomposability of domains into flat domains arose in [2], and was first addressed in [17]. In a thesis [11] supervised within the project by Jung, Haack has thoroughly investigated lax limits in the (order enriched) category of domains, and has obtained a good decomposition result. A new rather small cartesian closed category of domains emerges from this work.

Finally we should mention Abramsky and Jung’s substantial text [1] on Domain Theory which is being written under the aegis of the project. It gives an up-to-date account of the subject, and contains new results (notably a characterization of continuous domains in terms of bases).

5.2.1.2 Topos-theoretic generalizations

We have succeeded in producing significant work in connexion with those very specific applications of topos theoretic models pioneered in [30]. 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 (of a kind which we do not expect end users to need to appreciate). This more foundational work is described in Johnstone [15]. In addition, following on from the papers of Vickers [30] and Johnstone [14], a number of potentially useful variations on the idea have been considered. A survey of work so far is given in Johnstone [16]. These innovations were not predicted in the work plan, but we may hope for further developments in the remainder of the project.

On a wider front, Vickers has continued to develop a view of geometric topos theory as observational logic, as a basis for the semantics of a formal specification language. An expository paper setting out his point of view is [31]. He has also investigated the use of topos theory to internalize categories of domains in his work on topical categories [32].

5.2.2 Stable Functions and Duality

Work of Abramsky in particular established the importance of Stone duality to the semantics of programming languages; in this approach “properties” are more important than “values”. However, Abramsky’s work was limited to the standard Scott semantics of functional languages. So in the workplan we proposed considering a similar approach to stable semantics as well. In [10] Ehrhard and Malacaria proposed an abstract notion of ‘locale’ for stable functions as a meet-semilattice which is distributive for certain prescribed joins. While this addresses the original problem, project members became convinced that a theory of duality for a more subtle notion of stability would be of greater value. This notion of ‘strong stability’ has lead to tight connexions between Topics A and B, and is one of the major unforeseen recent developments in the project. It is described at greater length in 5.2.2.1. Inevitably much of the work has not been directly concerned with duality, but the duality theory has been extended to the case of strong stability, and details can be found in [19]. The importance of this general area is indicated by applications of the ideas of duality for stable functions to concurrency as described in 5.2.2.2.

5.2.2.1 Strong stability

The notion of strong stability was introduced by Bucciarelli and Ehrhard in their article [4] 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 (see Topic A) 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 non-extensional 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 [5] and [7].

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 (cf Topics A, G and H), and are described in [8]. 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 not yet published and is presented in [3].

Finally and dramatically, 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 ([6]). In [9] 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

5.2.2.2 dI-domains and concurrency

For an example of possible applications of duality for stable domains, we refer to the handbook chapter of Winskel and Nielsen [23]. This shows how a great many models for parallel computation are related by adjunctions. As a corollary, it shows how dIdomains can be identified with certain kinds of Petri nets; a subcategory of dI-domains with linear morphisms, those which, in addition to being stable and join-preserving, also preserve covering intervals, embeds fully and faithfully in a category of Petri nets. Conditions can be viewed as neighhbourhoods of nets and share many features of open sets of a topology. In particular, conditions are reflected by morphisms in the category of nets and a recent addition to the chapter shows that the notion of connected condition is central to the coreflection from dI-domains to safe Petri nets. This cast new light on an old construction (that of Nielsen,Plotkin and Winskel’s construction of a net from an event structure) and reveals new facts about the “logical” structure of conditions (for example, that conditions which are subcomponents of a condition of a dI-domain form a boolean algebra).

5.2.3 Duality in Synthetic Domain Theory

Our main efforts in Synthetic Domain Theory (SDT) differ from those rather tentatively envisaged in the project proposal (though some work in connexion with Topic A continues) and hence are reported under Topic B. The preliminary ideas of project members in this area were discussed at the first Workshop on Evaluation Logic and Synthetic Domain Theory, and subsequent work has been closely related to that on Topic E reported elsewhere.

The idea of synthetic domain theory is that domains can be treated as (certain kinds of) constructive sets. The aim is to provide an abstract and more flexible substitute for traditional denotational semantics. In the theory as currently envisaged, the replete objects play the role of predomains. We have developed a duality theory making sense of the repletion an object X as the points of Σ^{X} with respect to the limit theory of Σ (unpublished notes of Hyland). But this general result is rather uninformative. Hence we have been investigating ‘good’ cases where a simpler description of repletion is possible. Conceptually this is the case when the infinitary algebraic theory of Σ suffices, so that repletion has an algebraic description. We have made progress in specifying relevent axioms, and in finding models in which this is so. It turned out that this work was related to the question, which arose out of the first workshop, of providing good models for evaluation logic by using SDT.

5.2.3.1 Evaluation Logic, SDT and filter spaces

In the workshop on Evaluation Logic and Synthetic Domain Theory, it was decided to investigate first over the category of cpos and more generally over categories of replete objects, some computational monads which seemed particularly problematic for interpreting Evaluation Logic (according to the semantics proposed in [21]).

Unfortunately, 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). [20] tries to overcome these problems for Evaluation Logic, by replacing cpos with replete objects in the category of filter spaces (see [12]). 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).

5.2.3.2 Axioms and Models

Most of our work on axioms has focused on properties of the (Σ-epi, Σ-extremal mono) factorization system in the category of replete objects. As examples, consider 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. Going beyond this, Paul Taylor in particular has tried to identify 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) that Σ^{m} is a regular epi when m is a regular mono. This is stronger than A and entails that the replete objects are equivalent to the opposite of the category of Σ^{Σ^{(−)}}-algebras (algebras for the continuation monad). Models in which this holds are actively being sought.

Our work in this area has not yet reached publishable state, though definitions, ideas and results have been publicised on the SDT bulletin board set up by Paul Taylor in the course of the first year of the project. We hope to report more fully on these and related matters at the 2nd milestone.

5.2.3.3 Strong normalization proofs

One striking biproduct of work on models of SDT has been a fresh approach to strong normalization results. In [13] Hyland and Ong showed that given an arbitrary conditionally partial combinatory algebra (C-PCA), there is a systematic way to construct a Kreisel-style modified realizability topos which has (more than) sufficient completeness properties to provide a categorical semantics for higher type theories. Based on the topos generated from the C-PCA of an appropriate quotient of the strongly normalising untyped lambda-terms, they obtained a “generic” strong normalization (s.n.) argument. This argument reduces the s.n. property of a class of higher type to the validity of two “stripping arguments” which are reasonably easy to verify in the case of F_{ω}. In [22] Ong and Ritter report work which carries the same programme a step forward; they illustrate the general applicability, and the simplicity of the argument by bringing it to bear on the demanding test case of Coquand and Huets’ Calculus of Constructions.

5.2.4 Work completed or in progress within the project

Of the papers listed below, the following represent research done at least in substantial part in connexion with the CLICS II project: [1], [3], [6], [7], [8], [9], [11], [13], [15], [16], [18], [19], [20], [21], [22], [24], [25], [26], [27], [29], [23].

[1] S. Abramsky and A. Jung. Domain Theory. To appear in S. Abramsky and D. M. Gabbay and T. S. E. Maibaum (Eds) Handbook of Logic in Computer Science, Oxford University Press.

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

[3] A. Bucciarelli. Sequential models of PCF: some contributions to the domaintheoretic approach to full abstraction. PHD thesis, Università di Pisa, 1993.

[4] A. Bucciarelli, T. Ehrhard. Sequentiality and strong stability. In LICS 91.

[5] A. Bucciarelli, T. Ehrhard. Extensional embedding of a strongly stable model of PCF. In ICALP 91.

[6] A. Bucciarelli, T. Ehrhard. A theory of sequentiality. To appear in TCS.

[7] A. Bucciarelli, T. Ehrhard. Sequentiality in an extensional framework. Submitted to Information and Computation.

[8] T. Ehrhard. Hypercoherences: a strongly stable model of linear logic. To appear in Mathematical Structures in Computer Science.

[9] T. Ehrhard. Projecting sequential algorithms on strongly stable function. To appear in Annals of Pure and Applied Logic.

[10] T. Ehrhard and P. Malacaria. Stone duality for stable functions. In CTCS 91.

[11] C. Haack. Die Hyperlimeskonstruktion. Diploma Thesis, Technische Hochschule Darmstadt, 1993.

[12] J.M.E. Hyland. Filter spaces and continuous functionals. Annals of Mathematical Logic, 16, 1979.

[13] 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.

[14] 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.

[15] P.T. Johnstone, Fibrations and partial products in a 2-category. Applied Categorical Structures, to appear.

[16] P.T. Johnstone. Variations on the Bagdomain Theme. In preparation.

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

[18] O. Kirch. Bereiche und Bewertungen. Diploma Thesis, Technische Hochschule Darmstadt, 1993.

[19] P. Malacaria. Deux contributions de la Dualité de Stone à l’informatique théorique. PHD thesis, Université de Paris VII, 1993.

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

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

[22] C.-H. L. Ong and E. Ritter. A Generic Strong Normalization Argument: Application to the Calculus of Constructions. Paper presented at the 1993 Annual Conference of the European Association for Computer Science Logic.

[23] E. Robinson. Logical aspects of denotational semantics. In Summer Conference on Category Theory and Computer Science, Edinburgh, 7th–9th September 1987, volume 83 of Lecture Notes in Computer Science, pages 238–253. Springer Verlag, 1988.

[24] A. Schalk. Domains arising as algebras for power space constructions. Journal of Pure and Applied Algebra, 1993. To appear.

[25] A. Schalk. The Hoare Power Construction for Domains, Topological Spaces and Locales. Technical Report 1549, Technische Hochschule Darmstadt,1993.

[26] A. Schalk. Algebras for Generalized Power Constructions. Doctoral Thesis, Technische Hochschule Darmstadt,1993.

[27] M. B. Smyth. Completeness of quasi-uniform and syntopological spaces. Journal of the London Mathematical Society, 1993, to appear.

[28] Ph. Sünderhauf. Quasi-Uniform Completeness in Terms of Cauchy Nets. Technical Report 1529, Technische Hochschule Darmstadt, 1992.

[29] Ph. Sünderhauf. Constructing a Quasi-Uniform Function Space. Technical Report 1541, Technische Hochschule Darmstadt, 1993.

[30] 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.

[31] S. J. Vickers. Geometric logic in computer science. In Theory and Formal Methods 1993, ed. G. L. Burn, S. J. Gay and M. D. Ryan, Springer Workshops in Computing, 1993, 37–54.

[32] S. J. Vickers. Topical categories of domains. Technical Report DAIMI PB-397-I, 1992.

[33] G. Winskel. On power domains and modality. Theoretical Computer Science, 36:127–137, 1985.

[34] G. Winskel and M. Nielsen. Models for concurrency. To appear as a chapter in the Handbook of Logic and the Foundations of Computer Science, Oxford University Press, 1994.

5.3 Report on Topic C: Logic of Inductive and Recursive Datatypes

5.3.1 Summary

This report describes work done during Year 1 on Topic C (Logic of Inductive and Recursive Datatypes). This topic contributes to the project objectives in the areas of “Type Theory” and “Semantics and Logics of Programming Languages”. The collaborating partners are: Aarhus, Cambridge, Chalmers, Genova, Manchester. The deliverable planned for milestone 1 was a collection of proof principles for inductive and recursive datatypes. We intended to contribute to (i) the logic of well-founded datatypes (ii) the logic of non-wellfounded datatypes (the logic of infinite objects) (iii) the logic of recursive types in higher order functional programming languages.

We have made progress in all three areas. New proof principles have been established. Models of the resulting theories have been constructed. The principles have been put to use for particular examples.

5.3.2 Work completed

5.3.2.1 Logic of well-founded datatypes

The logic of well-founded datatypes in intuitionistic type theory was already welldeveloped and has been put to extensive use for formalizing proofs in programming, theoretical computer science, and mathematics. There were formulations of a theory of generalized inductive definitions in type theory both in natural deduction [4, 5, 6] and in categorical logic [4].

One thing that was missing in these formulations was an account of universes, and other reflection principles which are needed for formalizing certain metamathematical proofs such as normalization proofs. We have remedied this deficiency and extended type theory with a general notion of simultaneous inductive-recursive definition in Dybjer [7]. (The initial inspiration for this extension came from Mendler’s categorical semantics of type-theoretic universes [11].) This notion subsumes various universe constructions including internal universe-hierarchies and super universes described by Griffor and Palmgren. It also enables a construction of Frege structures inside type theory, making explicit use of proof-objects.

This extension of type theory has been proved consistent by constructing a realizability model [7].

Work on models of inductive types has also been done by Yuxi Fu [8]. He has extended Beeson’s recursive realizability models for type theory to inductive types. In particular he has shown that the strictness of positivity condition can be dropped when modelling inductive types in this way. Yuxi Fu has also worked on an ω-set model [8].

5.3.2.2 Logic of infinite objects

There has been much recent interest in modelling infinite objects in type theory as objects of coinductive types. Proof principles for such types arise from their categorical analysis as final coalgebras over categories of types. From this point of view types of infinite objects are dual to inductive types and hence defined by their destructors rather than their constructors.

Thierry Coquand has proposed alternative proof principles for such types of infinite objects. Firstly, as for well-founded objects, types are defined by their introduction rules. But then rather than defining functions by primitive recursion we can define functions by guarded recursion. In this way we can ensure that all objects defined are productive. This alternative relies on the existence of explicit proof objects in type theory.

This work was reported as part of the deliverable for ESPRIT-BRA TYPES [3], but it was conceived during conversations with Eike Ritter when he visited Chalmers. Since it also fits well into the general development of ideas under this topic of CLICS-II we mention it here.

5.3.2.3 Logic of recursive types in functional languages

Freyd has studied abstract conditions on categories that suffice for modelling recursive types with strong properties. These conditions involve the existence of object that are simultaneously initial algebras and final coalgebras for functorial type constructors.

Studying such algebraically compact categories, led Pitts [12] 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 provides 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 [2, 1] in the form of ‘internal full abstraction theorems’ for denotational semantics of SCCS and the lazy lambda calculus.

Freyd’s approach includes an approach to reflexive types, modelled as fixed-ponts of functors of mixed variance. Based on this Pitts [14] 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.

A concrete application of these ideas concerns proofs of correspondence between operational and denotational semantics. These proofs depend on the existence of certain relations specified as fixed points of non-monotonic operators. Pitts [13] shows how to construct such relations withour having to delve into the detailed construction of the recursively defined domains themselves.

An accessible account of the traditional concrete approach to these proofs can be found in a recent textbook by Glynn Winskel[15], where he uses information systems and well-founded induction on the structure of tokens for correspondence proofs for eager and lazy functional languages.

5.3.3 Future plans

We plan to further study simultaneous inductive-recursive definitions. In particular their importance for representing the semantics of type theory internally, and for normalization proofs. We expect that we will use ideas from the categorical semantics of type theory.

Work is in progress on investigating a categorical account initiated by Mendler of Hallnäs’ method [9] for constructing bisimulations without needing to iterate transfinitely. Categorically, this comes out as a special case of a general construction of final coalgebras for ω-continuous functors. This construction can be done in a category of constructive sets (in Martin-Löf’s sense). The goal of this work is to show that coinductive types are constructive in the sense that they can be interpreted in (standard) Martin-Löf’s type theory. A particular point is that this constructivity does not depend on the use of impredicative quantification as when coinductive types are represented in system F and the Calculus of Constructions following Wraith [16].

5.3.4 References and selected publications

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

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

[3] T. Coquand. Infinite objects in type theory. In Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen, 1993.

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

[5] P. Dybjer. Inductive Families. Formal Aspects of Computing. To appear.

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

[7] P. Dybjer. A general notion of simultaneous inductive-recursive definition in type theory. Draft paper, 1993.

[8] Y. Fu. Topics in Type Theory. PhD thesis, University of Manchester, 1992.

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

[10] B. Jacobs. Inductively defined types in dependent type theory. Draft version, 1993.

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

[12] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science. To appear.

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

[14] A. 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.

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

[16] G. C. Wraith. A note on categorical datatypes. In Category Theory and Computer Science, Proceedings, 1989. LNCS 389.

Interactions. Dybjer visits Cambridge 09-10/01/93; Pitts visits Chalmers 21-24/03/93; Ritter visits Chalmers 10-16/05/93.

Interaction with related research projects. Topic C is highly relevant for BRA-TYPES. Chalmers is also a site of that action. Proof principles for inductive and recursive datatypes form the foundation of the proof assistants developed in TYPES, where they have been put to extensive use. In almost all cases of developments of these proof principles there has been a strong interaction between categorical and prooftheoretic ideas. It is thus a topic in the junction between TYPES and CLICS-II with very strong interactions with other CLICS-II topics as well as with theoretical and practical developments in TYPES.

Coquand, Curien, Dybjer, and Ritter participated in the annual BRA-TYPES workshop in Nijmegen 24-28/05/93.

Work complete. Proof principles for simultaneous inductive-recursive definitions in type theory. Model constructions of inductive definitions in type theory. Proof principles for recursively defined types in functional languages. Abstract proof of adequacy of denotational semantics.

Difficulties encountered. There was an intended contribution from the Genoa site concerning the development of models for higher order languages (aka the theory of constructions) with subtypes and solutions for domain equations. This work has however stagnated and Genoa has instead presented progress under Topic D “subtypes and polymorphism in higher order languages” on the related topic of parametric models of polymorphism.

5.4 Report on Topic D: Subtypes and polymorphism in higher order languages

5.4.1 Summary

The topic contributes to the project objectives in the areas of Type Theory and Semantics of Programming Languages. The collaborating partners are CAIMENS, Genova, Manchester, and Sussex. The preliminary 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. [8, 9, 13, 18, 19]. 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 [2].

The workplan of the project listed research for this topic to span only six months of the period under review.

5.4.2 Completed work

It is important to separate the syntactic aspects from the semantic aspects of parametricity. In [1] 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’ abstrction theorem).

One of the main intents is to follow the category-theoretical paradigm to study the problem of parametricity. In their fundamental paper [18], 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 [18]).

In [2] there were presented PL-categories (=models of polymorphism) 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 [22]. What matters is that families be taken together with an action on isomorphisms.

In [5] 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 [24]), and he characterizes those interpretations of polymorphic terms which are invariant under isomorphism as those which are independent of the structure implementations.

In [6] Rosolini presents a general method to obtain a parametric model from a PLcategory which satisfies suitable conditions (the same as in [18]). The construction is done mimicking those of [8, 20] 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 [23] are particular instances of the construction performed.

Furthermore, there are transparent links to related works. The results in [9] about PER models follow from the main result of [6]. The structors of [13] 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 [19] are a more general construction than that given in [6] in the same way as homomorphisms of graphs are more general than homomorphisms of reflexive graphs. The construction in [2] 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 [17].) 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.

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 [16], see also [21]. 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 [3] 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 [4] a different presentation is given which is more directed to the proof theory.

5.4.3 Plans for future developments

The results obtained in the first part of the project suggest how to develop the subject toward the solutions of the problems considered in the presentation of the project, and possibly some new developments:

1. We intend to test the new construction in [6] by computing what kind of parametric models arise from the various known PL-categories, and we want to see if some of these are parametric completion. In particular we shall consider those described in [10, 9, 15]. It would be nice to find a cartesian closed category which does not extend to a PL-category, but whose parametric completion does. (In a sense this would go back to Reynolds’ first motivation for introducing parametricity.)

2. There is an obvious idea for which a parametric model can be extended to a fibration of “relations” as to give rise to a structure which should model the logic introduced in [7]. This must be confirmed.

3. The parametric models of [14] must be fitted into the framework: although this may seem straightforward, there are problems related to absolute lack of semantic presentatioins of syntactic models.

4. A subcategory of coercion maps on a given cartesian closed category gives rise to a reflective subcategory of the category of relations and the reflector preserves products. Hence the subcategory is also sub-cartesian closed. We want to investigate if this can help in introducing a new kind of models for polymorphism and subtypes which would avoid possible diversions to explicit coercions.

5. Considering the canonical structure of a reflexive graph on a category together with its category of relations, it is clear how the contra/covariant behaviour of type constructors is treated. It may be that this may take care also of the similar problem for the definition of recursive types. In a first attempt we shall try to see if there is any substance to this, attempting to develop a calculus of fixpoints, as in [12], using the framework of reflexive graphs on categories of embeddings.

In the following list of references, the first six entries are the papers which were produced within the project in the last year and are relevant to the topic.

[1] M. Abadi, L. Cardelli and P.-L. Curien. Formal parametric polymorphism. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 1993.

[2] 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.

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

[4] B.P. Hilken and D.E. Rydeheard. A theory of classes: proofs and models. To appear in the special issue of Math.Str.Comp.sci. for CTCS-5.

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

[6] G. Rosolini. Reflexive graphs and parametric polymorphism. To appear.

[7] M. Abadi, L. Cardelli and G.D. Plotkin. A logic for parametric polymorphism. To appear.

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

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

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

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

[12] 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.

[13] P. Freyd. Structural Polymorphism. Theo. Comp. Sci., 1993. To appear.

[14] 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.

[15] 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.

[16] 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.

[17] 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.

[18] Q. Ma and J. 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, Lectures Notes in Computer Science vol. 598, pages 1–40. Springer-Verlag, 1992.

[19] J. Mitchell and A. Scedrov. Notes on sconing and relators, 1993. To appear.

[20] 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.

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

[22] 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, [23] G. Plotkin. Second order type theory and recursion, 1993. Lecture at the Scott

Fest.

[24] 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.

5.5 Report on Topic E: Higher Order Modal Program Logics

5.5.1 Summary

This report describes work done during Year 1 on Topic E (higher order modal program logics). This topic contributes to the project objectives in the areas of “Semantics and Logics of Programming Languages” and “Domain Theory”. The work done address the key issue of “Unification of Formalisms”. It has involved the collaboration of Moggi in Genova, Pitts and some of his research associates and students in Cambridge, and Taylor at Imperial. The results reported here will appear in a special issue of Fundamenta Informaticae, or were presented at the following international workshops: Workshop on Interactions between Category Theory and Computer Science, Schloss Dagstuhl, July 1993; Fourth North American Jumelage, SRI Menlo Park, October 1993.

The general objective is to develop a program logic along the LCF approach, which provides a uniform framework for presenting programming languages and program logics, and supports a modular approach to their description. The intention was to build on previous work (undertaken in CLICS) by extending Evaluation Logic (see [12, 8]) to higher order logic, and by integrating it with Synthetic Domain Theory (see [5, 20]). The deliverable planned for this milestone was an Evaluation Logic for a subset of the Standard ML programming language containing reference types. This has not yet been achieved, progress towards this goal and the difficulties encountered are explained in subsection 5.5.2.1. To overcome the difficulties we have explored two independent approaches to evaluation logic described in subsection 5.5.2.3 and 5.5.2.4. However, axiom systems for Evaluation Logic have been identified, which are sound and complete w.r.t. natural classes of models (see subsection 5.5.2.2), substantial progress has been made in integrating Evaluation Logic with Synthetic Domain Theory (see subsection 5.5.2.3), and a proof-theoretic and categorical analysis of necessity in S4 has been carried out (see subsection 5.5.2.4). Moreover, the effort towards integration has sparked further work on axioms and models for Synthetic Domain Theory, and is reported under Topic B. The publications which form the deliverables under this Topic are items [1], [9], [10] and [15].

Workshop on synthetic domain theory and evaluation logic. The two days meeting 9-10/01/93 was devoted to discuss problems, issues, and strategies. (A more detailed account of the meeting is given in a separate report, here we recall only the main issues regarding evaluation logic.) Pitts reported on the problems of intensionality in connection with dynamic allocation. It was decided to check whether the approach in [9] was able to overcome the problems. Another test case for [9] was to look at some problematic monads on the categories of replete objects (in some suitable models of Synthetic Domain Theory), namely continuations Σ^{(Σ^{X})} and Plotkin’s powerdomain. In a discussion on “extensionality versus intensionality” it was agreed that an extensional logic would be more desirable, but this issue could not be resolved without further testing. Only later (after various attempts to get a positive result) we showed that the problematic test cases do not fit in the framework of [9].

5.5.2 Work completed

5.5.2.1 Evaluation logic for local state

The objectives under this heading are intimately tied up with corresponding ones under Topic F, described in subsection 3 (Semantics of local state) of the report on that topic. Our general approach to giving formal semantics and program logics requires the construction of a computational metalanguage ML_{T} (Σ) over a signature Σ tailored to the target programming language P L to be translated into ML_{T} (Σ). A logic must be given over ML_{T} (Σ) which permits the operationally defined observations in P L to be translated into judgements in the logic. A minimal requirement is that these translations preserve and reflect validity of observations in the programming language. This ensures that the metalanguage and logic are adequate for reasoning about the observable behaviour of programs.

When formulating the project proposal, it was envisaged that in order to meet this minimal requirement the logic over the computational metalanguage would need to incorporate the evaluation modalities introduced in [12] (and correspondingly work on Topic F shows a dependency on Topic E in the Workplan). This has turned out not to be the case. For both dynamic allocation of local names [14] and more generally for local mutable state [17] we have found that a predicate logic with equality (over a suitably rich computational metalanguage) is sufficient to establish adequacy. In fact, this option was forced on us by certain problems with intensionality for the rules in [12] (described next) and difficulties in fitting the new models for dynamic allocation in the framework of [9] (see subsection 5.5.2.3). To overcome these difficulties we have investigated two independent approaches to evaluation logic: one generalises the semantics in [9] (see subsection 5.5.2.3), the other exploits a proof-theoretic analysis of modal logic S4 (see subsection 5.5.2.4).

Problems of intensionality The programs logics we are constructing are based upon predicate logic with equality. In particular they must satisfy the fundamental principle of equality that equal can be substituted for equal in any logical assertion. In other words the substitution rule

x = x′ : A Φ(x)
\overline{(SUB).}
Φ(x′)

should be valid. This is in contrast, for example, with recent work of Mason and Talcott [4] on an operationally based logic for local state. Their logic of ‘contextual assertions’ can make intensional distinctions between equal (‘contextually equivalent’) expressions: in other words the rule (SUB) is not valid in their logic. We regard this as a defect restricting the usefulness of their logic which we wish to avoid. Mason and Talcott give an example of a typical failure of (SUB): see [4, Sect. 5(A)]. The analogue in evaluation logic of their example would be the invalidity of the following specialisation of (SUB):

e = e′ : T A [x⇐e]Φ(x)
\overline{([]-SUB).}
[x⇐e′]Φ(x)

Pitts has shown that in the presence of the rules introduced in [12], the rule ([]-SUB) permits one to derive a contradiction from a certain equation E = F (see below) valid in a (computationally adequate) model for dynamic allocation. For example, the following two ML expressions of type unitref->bool are observationally equivalent:

                e  =^{def} let val x=ref() in fn y => x=y end
                f  =^{def} fn (y:unit ref) => false.

Under translation into ML_{T} (Σ) these become the following terms of type T (ν → T o):

E =^{def} let x⇐new in [λx ∈ ν.[x = y]]
F =^{def} [λx ∈ ν.false].

(Here we are assuming the signature Σ contains, amongst other things, types ν and o of names and booleans and a constant new : T (ν) for the computation of a new name; see [14].) However, one derive a contradiction from E = F and the axiom ⟨x⇐new⟩true (asserting that the evaluation of new terminates). Both approaches described in subsection 5.5.2.2 and 5.5.2.4 weaken the axioms for necessity

Φ(a) ⇔ [x⇐[a]]Φ(x)  (5.1)
[x⇐e][y⇐f(x)]Ψ(y) ⇔ [y⇐(let x⇐e in f(x))]Ψ(y)  (5.2)

considered in [12], but [9] invalidates the ⇐ direction, while [1] invalidates the other direction.

Representation independence for local state The work in this project on semantics and logics for local state is focused on the kind of dynamically allocated local state that occurs in Standard ML. However, recent progress on the semantics of blockstructured local state in Algol-like languages by O’Hearn and Tennent has influenced our work. In particular Pitts and Stark [14] have adapted the use in [11] of ‘relationally parametric’ functors to produce a modification of Moggi’s dynamic allocation monads, giving a more ‘fully abstract’ model of dynamic creation of local names. [15] gives a notion of logical relation incorporating this form of relational parametricity and a form of Reynolds’ notion of ‘representation independence’ for local names. They show how this kind of logical relation may be used to establish instances of observational equivalence in a programming language involving local names (the ‘nu-calculus’). See the report on Topic F for a fuller discussion.

From the point of view of work done under Topic E, what is lacking is the incorporation of the proof technique inherent in this use of relationally parametric logical relations for local names into the programming metalogic being developed. What we have in mind here is analogous to Plotkin and Abadi’s logical treatment of relationally parametric polymorphism [16]. To do this we seem to need to go beyond evaluation modalities: the necessity modality is a form of action of the monad T on unary relations, whereas an action on binary relations may be needed (with properties yet to be determined).

5.5.2.2 Sound and complete axiom systems for evaluation logic

The objective here was to find axiom systems for various versions of EL (Evaluation Logic), which are sound and complete w.r.t. natural classes of models. Pitts’ models for EL (see [12]) were rather general structures, based upon Lawvere’s hyperdoctrines for modelling predicate logic, and the interpretation of the modalities was constrained by the choice of monad, but not uniquely determined by it.

[9] takes a more standard approach to modelling EL, based upon the requirement that the monad preserves (distinguished) subobjects and their inverse images. In these models there is an obvious interpretation of the necessity modality. [9] identifies sound and complete axiom systems for this kind of models. This is done both for first order and higher order versions of EL (involving only the necessity modality). In the higher order version, there is an impredicative encoding of the evaluation predicate and the possibility modality in terms of the necessity modality. In order to obtain the completeness results, [9] uses the Grothendieck (see [3]) and the Tripos construction (see [12, 6]), and extends in an interesting way the work of Hyland-Johnstone-Pitts on constructing toposes from hyperdoctrine models of higher order logic.

5.5.2.3 General semantics for evaluation logic

Preservation of (distinguished) subobjects by monads is a fairly natural requirement (see the many examples in [9]), and allows a simple interpretation of necessity. However, there are computational monads, which may not satisfy this requirement. These include some monads for continuations and dynamic allocation, and several kinds of powerdomain. The objective here is to extend the interpretation of necessity, so that it is not based upon additional requirements on strong monads, and to find sound and complete axiom systems for this wider class of models.

[10] extends the interpretation of necessity proposed in [9] by dropping all requirement on strong monads, at the expense of stronger assumptions on the underlying category and the class of distinguished subobjects. These assumptions are consistent with Synthetic Domain Theory, but are too strong for classical Domain Theory: they are satisfied by any small complete quasitopos (when the distinguished subobjects are either all subobjects or only regular ones), but are not satisfied by the category of cpos and the class of inductive subobjects. Without the additional requirement on strong monads, the interpretation of necessity is far more complicated and there are several alternatives (which yield different semantics). [10] considers seven of these alternative interpretations (they all agree with the interpretation proposed in [9], when this is defined), and gives evidence that only one of them is suitable for interpreting necessity. Despite important differences in the logical setting, we have also looked at Reyes’ topos-theoretic semantics of modal logics (see [18]) and related it to the semantics in [9].

5.5.2.4 Evaluation logic and proof-theory

Based on our experience with Linear Logic, some of the work in Program Logics in Cambridge has taken the direction of Categorical Proof-Theory. We decided to produce a constructive S4-variant of Evaluation Logic and the work for that has been divided in three stages:

• The first stage was to understand proof-theoretically the Computational Lambda-Calculus, where the strong monad T plays the role of a (non-canonical) possibility operator.

• The second stage is to concentrate on a constructive version of S4. Here the difficulty lies in deciding which properties such a system should satisfy. The answer is clear enough if the underlying logic is classical, but over an intuitionistic basis some choices have to be made. There are several proposals in the literature, including very recent ones by Nerode and Wijesekera on ”Constructive Concurrent Dynamic Logic” and by A. Simpson on constructive (but weaker than S4) modal logics. The idea here is that the modalities in Evaluation Logic could be taken to reflect the minimal properties associated with constructive S4-modalities.

• The third stage of the work is to add quantifiers to the amalgamation of the systems above. This ought to give us (with a suitable choice of recursive operators) an S4-variant of Evaluation Logic. This seems to solve at least one of problems raised by ML-style references, as one of the Pitts and Stark counter-intuitive examples disappears. This is work in progress.

5.5.3 References and selected publications

[1] Gavin Bierman, Claudia Meré and Valeria de Paiva. Intuitionistic Necessity Revisited. Chapter 13 of: Plos, Masuch and MarxPlos, Masuch and Marx (eds), Arrow Logics and Multimodal Logics (OUP, 199?), to appear.

(available as /theory/papers/dePaiva/inr.dvi from theory.doc.ic.ac.uk)

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

[3] J.W. Gray. Fibred and cofibred categories. In S. Eilenberg et al., editors, Proc. Conf. Categorical Algebra (La Jolla 1965). Springer Verlag, 1966.

[4] F. Honsell, I.A. Mason, S.F. Smith, and C. Talcott. A variable typed logic of effects. In Proceedings 1992 Annual Conference of the European Association for Computer Science Logic CSL92, San Miniato, volume to appear of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[5] 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 Lecture Notes in Mathematics. Springer Verlag, 1991.

[6] J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88, 1980.

[7] Ian Mason and Carolyn Talcott. References, local variables and operational reasoning. In Proc. 7th Annual Symp. on Logic in Computer Science, Santa Cruz, 1992 (IEEE Computer Society Press, Washington, 1992) pp 186–197.

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

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

(available as /theory/papers/Moggi/elt.dvi from theory.doc.ic.ac.uk)

[10] E. Moggi. A general semantics for evaluation logic, 1993.

(available as /theory/papers/Moggi/elt2.dvi from theory.doc.ic.ac.uk)

[11] P. W. O’Hearn and R. D. Tennent. Relational Parametricity and Local Variables. In Conf. Record 20th Symp. on Principles of Programming Languages, Charleston, 1993 (ACM, New York, 1993) pp 171–184.

[12] A.M. Pitts. The Theory of Triposes. PhD thesis, University of Cambridge, 1981.

[13] Andrew Pitts. Evaluation Logic. In G. Birtwistle (ed.), IVth Higher Order Workshop, Banff, 1990, Workshops in Computing (Springer-Verlag, Berlin, 1991), pp 162–189.

[14] A.M. Pitts. Relational properties of recursively defined datatypes. In 8th LICS Conf. IEEE, 1993.

[15] Andrew Pitts and Ian Stark. On the Observable Properties of Higher Order Functions that Dynamically Create Local Names. (Preliminary Report. In Proc. ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, 1993.

(available as /theory/papers/Pitts/silp.dvi from theory.doc.ic.ac.uk)

[16] Andrew Pitts and Ian Stark. Observable Properties of Higher Order Functions that Dynamically Create Local Names, or: What’s new?. In Proc. 18th Int. Symp. on Math. Foundations of Computer Science, Gdańsk, 1993, Lecture Notes in Computer Science Vol. ? (Springer-Verlag, Berlin, 1993).

[17] Gordon Plotkin and Martin Abadi. A Logic for Parametric Polymorphism. In Proceedings of the Conference on Typed Lambda Calculus and its Applications, Utrecht, 1993, Lecture Notes in Computer Science Vol. 664 (Springer-Verlag, Berlin, 1993) pp 361-375.

[18] G.E. Reyes and H. Zolfaghari. Topos-theoretic approaches to modalities. In A. Carboni, C. Pedicchio, and G. Rosolini, editors, Conference on Category Theory ’90, volume 1488 of Lecture Notes in Mathematics. Springer Verlag, 1991.

[19] Ian Stark. A calculus for dynamic allocation of store. Working paper, Univ. Cambridge Computer Laboratory, January 1993.

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

5.6 Report on Topic F: Monadic Programming Language Semantics

This report describes the progress which has been made during the first year of the project on Topic F of the Workplan. The work contributes to the project objectives in the area of Semantics and Logics of Programming Languages. It has involved the collaboration of Moggi in Genova, Pitts in Cambridge and Stoughton in Sussex, together with some of their research associates and research students. Conference presentations of the results reported here were given at the following international conferences and workshops: ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, June 1993; Workshop on Interactions between Category Theory and Computer Science, Schloss Dagstuhl, July 1993; 18th International Symposium on Mathematical Foundations of Computer Science, Gdańsk, August 1993; Conference on Category Theory and Computer Science, Amsterdam, September 1993.

Section 5.6.1 briefly recalls the monadic approach to denotational semantics developed by the CLICS project. The subsequent sections describe the work that has been done so far in the CLICS-II project towards extending and applying this approach. The publications which form part of the deliverables under this Topic are items [2], [14],

[15] and [17].

5.6.1 Monadic programming language semantics

Moggi [9] introduced the use of categorical monads as a tool for structuring denotational semantics. Using techniques of categorical logic, this can be formalized via metalanguages ML_{T} extending LCF-like computational metalanguages with a so-called ‘computation type’ constructor T (which is modelled by the monad). ¿From this point of view the process of giving a denotational semantics to a programming language P L, equipped with a (structured) operational semantics, splits into the following steps. (See [12] for an illustration of the technique, based on a small fragment of Standard ML with global references.)

A Identification of a suitable signature Σ over the metalanguage and definition of a compositional translation [[−]] of P L into ML_{T} (Σ).

B Definition of a logical theory over ML_{T} (Σ) together with an interpretation of the (operationally defined) observations in P L as judgements in the logic. A fundamental requirement (called computational adequacy) is that an observation hold of a P L expression E if and only if the corresponding judgment about [[E]] is provable in the logic. So long as equality is part of the logic over ML_{T} (Σ), this condition (together with compositionality of the translation [[−]]) guarantees that observational equivalence of P L expressions may be established via provable equality of their translations in ML_{T} (Σ). Establishing adequacy normally involves carrying out step C.

C Construction of (adequate) models of the logical theory defined in B (which in turn involves finding suitable categories and monads). The ideal (often very difficult to obtain) is a ‘fully abstract’ model, in which equality of denotations coincides with observational equivalence. In practice specific models, even if not fully abstract, can suggest sound extensions to the logic in step B which enhance its usefulness as a tool for reasoning about observational equivalence in P L.

5.6.2 Syntactic approach to modularity in denotational semantics

For applications of denotational semantics (whether monadic or not) to be feasible for large-scale examples, the key issue of modularity of denotational descriptions has to be addressed. Work carried out in the first CLICS project [7, 8] proposed a way of tackling the problem of modularizing the monadic semantic specification of programming languages based on the use of monad transformers to build up new monads from old when carrying out the step C of subsection 5.6.1. One barrier to the usability of this approach is the level of expertise and mathematical sophistication required. This issue of simplicity of such denotational techniques has been addressed in the current project. In the translation of P L into ML_{T} (Σ) the details of how one should interpret the computational monad T are hidden (much as an interface hides implementation details of an abstract datatype). So it is in the last step C that most of the complexities lie. Simplicity is achieved through a syntactic reformulation of the original monad-transformer approach which deals directly with the metalanguages ML_{T} (Σ) constructed in step B.

[7, 8] proposed an incremental approach to constructing models of ML_{T} (Σ) analogous to the stepwise refinement method of program development. This approach is reformulated in a simpler, syntactical way in [2] using a duality between model constructions and translations (often called ‘relative interpretations’) between theories. Thus, a model of some basic metalanguage ML_{T} (Σ_{0}), is refined towards a model of the target metalanguage by composing it with a sequence of translations

ML_{T} (Σ_{n}) →^{I_{n}} ML_{T} (Σ_{n−1}) →^{I_{n−1}} ⋯ →^{I_{0}} ML_{T} (Σ_{0})

that are built up step by step. To demonstrate the simplicity and usability of this syntactic reformulation of the monadic approach, [2] gives sample theories and translations which can be used to give semantics to concurrent languages without the ad hoc treatment still present in the original approach. We are beginning to investigate implementing this modular approach in Pollack’s LEGO proof assistant [3].

The notion of translation between metalanguages used in this work is general enough to describe the traditional techniques of denotational semantics [Mos90], but is not applicable to constructions involving ‘change of category’. For example the work on monadic semantics of local state described in the next subsection involves monads on functor categories valued in some suitable category of domains. It is unclear whether monad transformers may help in structuring this more complex denotational semantics.

5.6.3 Semantics of local state

Programming languages combining higher order features with the manipulation of local state present severe problems for existing techniques of programming language semantics and logics of programs. For denotational semantics, the problems manifest themselves as a lack of abstraction in existing semantic models: some expressions that are observationally equivalent (i.e. that can be interchanged in any program without affecting its behaviour when executed) are assigned different denotations in the model. For operational semantics, the problems manifest themselves in the fact that simple techniques for analyzing observational equivalence in the case of purely functional languages (such as Milner’s ‘Context Lemma’ [5], or more generally, notions of applicative bisimulation [1]) break down in the presence of state-based features. Furthermore, operationally based approaches to properties of programs are often inconveniently intensional, e.g. the familiar congruence properties of equational logic fail to hold. (See [4, Sect. 5(A)], for example.) These problems have been intensively studied by a number of workers for the case of local variables in block-structured, Algol-like languages, but the case of languages involving the dynamic creation of mutable locations, such as Standard ML[6], has been much less studied.

The project work under this heading (and related work under Topics C and E of the Workplan) aims to apply categorical logic, and in particular the monadic approach to denotational semantics, to develop better techniques than currently exist for reasoning about the evaluation behaviour of higher order functions in Standard ML which may be recursively defined, and involve recursive datatypes and (monomorphic) reference types. This is rather an ambitious aim, and so far it has only partly been achieved. The strategy adopted is to build up to the full combination of features by studying judiciously chosen combinations of them in isolation for which there is some hope of obtaining definitive results (such as fully abstract models, or complete proof systems). The results of these studies are outlined below.

The nu-calculus The motivation for this part of the work was to try 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. Following initial work of Stoughton in Sussex, Pitts and Stark in Cambridge studied higher order functions that can dynamically create fresh names of things, but which ignore completely what kind of thing (references, exceptions, etc.) is being named. Names are created with local scope, can be tested for equality, and are passed around via function application, but that is all. As the vehicle for this study [14] formulates an extension of the call-by-value, simply typed lambda calculus, called the nu-calculus. In terms of Standard ML, it contains higher order functions over ground types bool and unitref—the latter being the type of dynamically created references to the unique element of type unit. This acts as a type of ‘names’ because only one thing can be (and is) stored in such a reference, so that its only characteristic is its name.

Recursion is purposely excluded from the nu-calculus and as a result any closed expression evaluates to an essentially unique canonical form. Indeed, 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 [15] shows that this expectation is misplaced: nucalculus expressions can exhibit very subtle behaviour with respect to an appropriate notion of observational equivalence. [15] introduces a notion of ‘logical relation’ for the nu-calculus incorporating a version of representation independence for local names. The technique is a syntactic version of the relationally parametric semantics of O’Hearn and Tennent [11]. There are also interesting similarities with Plotkin and Abadi’s parametricity schema for existential types [16, Theorem 7]. This version of logical relations is used to establish the termination properties of 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.

The programme outlined in subsection 5.6.1 has been carried out 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. [14] identifies some simple structure on a category equipped with a strong monad 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 [7] ‘dynamic allocation’ monad to O’Hearn and Tennent’s category of relationally parametric functors [11]. This model is shown to be fully abstract at first order types, but not so at higher types. So far no fully abstract (concrete) model of the whole language is known.

The store calculus Stark [17] considers an extension of the call-by-value typed lambda calculus allowing dynamic creation of references to values of higher type. Combining the results in [12] with the work on the nu-calculus, steps A and B of the programme of subsection 5.6.1 are carried out. It remains to carry out step C, i.e. to construct adequate models of the metalanguage and logic introduced in [17]. To do this using our existing knowledge of monads constructions requires the combination of dynamic allocation monads (on functor categories) and side-effect monads involving a non-constant state functor. Initial studies have been carried out by Moggi.

A serious complication has to do with modelling recursion in the programming language. (Stark’s store calculus contains recursion implicitly since it permits references to values of higher type; and the target fragment of Standard ML mentioned at the beginning of subsection 5.6.3 contains recursion explicitly.) To cope with this, we are looking for monads on cpo-enriched categories. However, all but the least abstract of the dynamic allocation monads involve quotient constructions, and these are known to be complicated in the category of cpo’s. It may be possible to circumvent these complications by moving to a category of cpo-PER’s, in which quotients have been formally adjoined. A related complication is that the definition of the monad for the store calculus involves recursively defined domains of mixed variance. Here we expect the work in [13] (see the report on Topic C) to be of help in establishing adequacy of the model.

The programming language considered in [17] only differs from the fragment of Standard ML which is the target for this part of the Project in that it lacks recursive datatypes. We feel that the essential difficulties lie in completing step C for the store calculus, since in particular this step already involves the use of recursively defined domains. If this can be done, the extension of the monadic denotational semantics to encompass recursive datatypes should be relatively straightforward.

[1] Samson Abramsky. The Lazy Lambda Calculus. In D. Turner (ed.), Research Topics in Functional Programming (Addison-Wesley, 1990), pp 65–116.

[2] Pietro Cenciarelli and Eugenio Moggi. A Syntactic Approach to Modularity in Denotational Semantics. In: Proc. Conference on Category Theory and Computer Science, Amsterdam, 1993. Lecture Notes in Computer Science Vol. ? (Springer-Verlag, Berlin, 1993).

[3] Z. Luo and R. Pollack. LEGO Proof Development System: User’s Manual. University of Edinburgh LFCS Technical Report ECS-LFCS-92-211, 1992.

[4] Ian Mason and Carolyn Talcott. References, local variables and operational reasoning. In Proc. 7th Annual Symp. on Logic in Computer Science, Santa Cruz, 1992 (IEEE Computer Society Press, Washington, 1992) pp 186–197.

[5] Robin Milner. Fully abstract models of typed λ-calculi. Theoretical Computer Science 4(1977) 1–22.

[6] Robin Milner, Mads Tofte and Robert Harper. The Definition of Standard ML (MIT Press, 1990).

[7] Eugenio Moggi. An abstract view of programming languages. University of Edinburgh LFCS Technical Report ECS-LFCS-90-113, 1989.

[8] Eugenio Moggi. A modular approach to denotational semantics. Invited talk, Conference on Category Theory and Computer Science, Paris, 1991.

[9] Eugenio Moggi. Notions of computation and monads. Information and Computation 93(1991) 55–92.

[10] Peter Mosses. Denotational semantics. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science (North-Holland, Amsterdam, 1990).

[11] Peter O’Hearn and Robert Tennent. Relational Parametricity and Local Variables. In Conf. Record 20th Symp. on Principles of Programming Languages, Charleston, 1993 (ACM, New York, 1993) pp 171–184.

[12] Andrew Pitts. Evaluation Logic. In G. Birtwistle (ed.), IVth Higher Order Workshop, Banff, 1990, Workshops in Computing (Springer-Verlag, Berlin, 1991), pp 162–189.

[13] Andrew Pitts. Computational Adequacy via ‘Mixed’ Inductive Definitions. Submitted for Proc. Mathematical Foundations of Programming Semantics IX, New Orleans 1993, Lecture Notes in Computer Science (Springer-Verlag, Berlin).

[14] Andrew Pitts and Ian Stark. On the Observable Properties of Higher Order Functions that Dynamically Create Local Names. (Preliminary Report. In Proc. ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, 1993. Yale Univ. Dept. Computer Science technical report YALEU/DCS/RR-968, pp 31–45.

[15] Andrew Pitts and Ian Stark. Observable Properties of Higher Order Functions that Dynamically Create Local Names, or: What’s new?. In Proc. 18th Int. Symp. on Math. Foundations of Computer Science, Gdańsk, 1993, Lecture Notes in Computer Science Vol. 711 (Springer-Verlag, Berlin, 1993), pp 122–141.

[16] Gordon Plotkin and Martin Abadi. A Logic for Parametric Polymorphism. In Proceedings of the Conference on Typed Lambda Calculus and its Applications, Utrecht, 1993, Lecture Notes in Computer Science Vol. 664 (Springer-Verlag, Berlin, 1993) pp 361-375.

[17] Ian Stark. A calculus for dynamic allocation of store. Working paper, Univ. Cambridge Computer Laboratory, January 1993.

5.7 Report on Topic G: Applied Linear Logic and Concurrency

Largely unforeseen at the time of writing the proposal was the influential role that game semantics of linear logic was to play. Through categories of games full completeness has been achieved for classical linear logic (see “Work on Games”below). This strengthens the Curry-Howard isomorphism by establishing a perfect match between a category built from game-theoretic intuitions and the category obtained from the proof system of classical linear logic. The modelling of linear logic by categories of games is already proving a powerful tool. The games are based on two kinds of moves, those of Opponent and those of Player, related by a form of accessibility (or enabling) relation. In fact they carry the structure of special forms of Petri net, which can in turn be identified with (filiform) concrete data structures, a representation of those domains which support a definition of sequential function and algorithm. This goes some way to explaining the role games have played in the refined analysis of sequential computation, leading to intensionally fully abstract models of PCF (see topic A on “Sequentiality and Stability”). It also links to more traditional work, not just in sequentiality, but to models for concurrency. The dust has not yet settled, and the relations between the different categories of games and models for computation (including the two categories yielding intensionally fully abstract models of PCF) is not yet clear.

There have been considerable advances in more expected areas forecast in the Workplan. Progress has been made in the use of both categories of Petri nets and in individual Petri nets as models for linear logic; in particular, there are new completeness results (see below for details). Collaboration with André Joyal has led to a convincing abstract way of defining bisimulations in a range of different (categories of) models. This work also contributes to the understanding of process refinement, and stands with several other contributions to models for parallel computation, including the connection with operational semantics (see “Concurrency” below). Significant contributions have been made to linear functional programming languages, including categorical combinators for them (see “LL and Functional Programming” below). This builds on foundational work on the nature of categorical models for linear logic.

Work on Games

Abramsky and Jagadeesan introduced a category of games as a model for Linear Logic. This built on pioneering work by Blass, but improved it in several crucial respects—for example, Blass’ definitions did not lead to a category. Also, Abramsky and Jagadeesan introduced the important notion of full completeness: a categorical model of a logic such that every morphism (at a denotable type) is the denotation of a unique cut-free proof. They also introduced the apparently very restrictive notion of a history-free strategy, whose response depends only on the immediately preceding move of the Opponent. This incorporates a strong constraint of locality of information, which has proved to be very powerful and fruitful. They showed that the category of games and history-free strategies has a rich enough structure to provide a model of Multiplicative Linear Logic, and moreover is closely related to Girard’s Geometry of Interaction; and they proved a Full Completeness theorem for this category with respect to Multiplicative Linear Logic plus the MIX rule.

Next, they extended the history-free semantics to (second-order) Multiplicative Exponential Logic. This proved to be a very subtle and challenging task; indeed, it involved overcoming the technical problems afflicting Girard’s Geometry of Interaction interpretation of the exponentials. The solution involved a partial equivalence relation on strategies induced by the action of automorphism groups on the underlying games. On this basis, they were then able to prove a Full Completeness Theorem for “ML-types”, i.e. for the universal second-order closures of simple types built from type variables. This should be compared with the best previously known result along these lines, for PER models, which applies only to “algebraic” types, i.e. first-order types in the functional sense, as opposed to arbitrary simple types.

Hyland and Ong subsequently refined the Abramsky-Jagadeesan model of the multiplicatives by considering a category of finite, fair games, and used it to prove a Full Completeness Theorem for Multiplicative Linear Logic without the MIX rule. It remains to be seen if their model can be extended beyond the multiplicatives.

Lamarche introduced a proof-net criterion for Multiplicative-Additive Linear logic. His work combines syntactic and semantic ingredients, with connections to game semantics.

Linear Logic and Functional Programming

In the area of intuitionistic linear logic directly applied to Functional Programming, the main achievements have been a better notion of a Natural Deduction formulation of Intuitionistic Linear Logic in parallel with a more precise notion of a categorical model of Intuitionistic Linear Logic. This work is preliminarily described in [3] as well as two refereed papers that grew up from this technical report, namely [4, 5]. This work builds on [14] describing Full Intuitionistic Linear Logic, its categorical semantics and a non-trivial cut-elimination theorem for it.

A full and detailed study of the complete intuitionistic fragment of linear logic (intuitionistic linear logic) is presented in Gavin Bierman’s forthcoming Ph D. thesis. There intuitionistic linear logic is studied from logical, term calculus and categorical viewpoints. In addition some implementation issues for this fragment are suggested.

There has been work at Cambridge on Categorical Combinators for Linear Logic. The two-fold idea here is to develop the category theory and the machinery necessary for a linear categorical abstract machine along the lines of Curien’s CAML. The first more theoretical part of the work has been achieved for intuitionistic linear logic. Building on Ritter’s previous work on categorical combinators for the calculus of constructions, the notion of a syntactic multicategory emerges as the appropriate concept to deal, not only with intuitionistic linear logic, the main goal, but also with some other weaker substructural logics. Syntactic multicategories are defined and shown equivalent to the traditional notion of a Lambek multicategory and then a system of categorical combinators that correspond to them is described. The main idea in both the syntactic multicategories as well as in the combinators is that substitution is dealt with explicitly and the role of contexts as modelling tensor products is separated from their role as modelling substitutions. This idea has two important consequences. First, it makes the construction of a categorical abstract machine much easier. Second the syntactic multicategories can be defined in terms of universal properties. Hence relatively simple combinators are obtained and the problem with Lambek’s original definition is avoided. His definition of composition in a multicategory does not indicate which variable is substituted for. This work is described in the abstract [11].

The second part of the work applies term-rewriting techniques to the system of combinators and developing a semi-automatic rewriting tool for manipulating and reasoning about combinators for intuitionistic linear logic. Work is still in progress on dealing with the operator “!” from the rewriting point of view. This work is described in the abstract [17].

Some preliminary work was done on connecting Full Intuitionistic Linear Logic and the theory of concurrent processes, using Bierman’s idea of ”Process Nets”. Process Nets are a graphical representation of the term calculus for Full Intuitionistic Linear Logic. They represent a collection (network) of parallel asynchronous processes connected via directed, typed channels. Evaluation is given by dataflow through the circuit, rather than by evolution of the circuit itself (as in Girard’s proof nets). This is aimed at providing a version of the Curry-Howard isomorphism for concurrent processes, discussed in the Workplan. So far only a preprint has been prepared.

In [21], Sergei Soloviev shows how some reductions known from ordinary intuitionistic propositional calculus can be modified for intuitionistic linear logic (without ! and ?). The main reductions are: 1) reduction of the depth of formulas in the sequents by addition of new variables, and 2) elimination of linear disjunction and the constant F. Both transformations preserve deducibility, i.e. the sequent is deducible iff the initial one was deducible. The growth of the size of sequent is linear for 1) and cubic for 2).

Marcus Moore (Larry Paulson’s PhD student) has implemented linear logic in Isabelle using de Groote’s sequent-calculus.

Petri Nets as Models of Linear Logic

Uffe Engberg and Winskel’s completeness results for linear logic with respect to individual Petri nets as a model appeared in MFCS93 [12, 13]. The paper settles questions raised in the Workplan. Completeness is shown for several versions of Girard’s linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with ⊗, −, &, ⊕ and the exponential ! (“of course”), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. Completeness is shown for several versions of Girard’s linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with ⊗, −, &, ⊕ and the exponential ! (“of course”), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed.

Concurrency

The handbook chapter [23] is now complete. 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, dIdomains, Petri nets, transition systems with independence, ordinary transition systems and Hoare traces. The papers [18, 19, 20] extend the work in [23] with new models suggested by the classification.

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. In “Bisimulation and open maps”[16], an abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets) and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner’s strong bisimulation. On event structures it explains and leads to a revision of history-preserving bisimulation of Rabinovitch and Traktenbrot, Goltz and van Glabeek—a revision that has previously been proposed by Bednarczyk. There is an accompanying generalisation of Hennessy-Milner logic characteristic for the general definition of bisimulation. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. The abstract definition of bisimulation answers a problem of the Workplan, and begins to address issues on atomicity and refinement discussed there.

Rosolini in Genoa has continued collaboration with Pierpaolo Degano and Roberto Gorrieri on the semantic aspects of process refinement. They have developed a way of describing the refinement of actions based purely on the structure of the category of algebraic Scott domains. The basic construction considers the data of a refinement as a domain (of configurations) and a functor from the domain (considered as a category) into a category of domains. The values of the functor are the replacement domains and the actions of the functor on the order describe how to refine the relation of causality. On these data one takes a certain fibration (first presented in [9] of CLICS-I) and the continuous sections of this produce the domain result of the replacement. It is worth noting that this is a more general construction than the others presented in the literature, and while the others had to preserve the relations of causality and conflict, this acts with no restrictions, and it is possible to control preservation of either causality or conflict by suitable requirements on the functor.

The paper [7] continues Brown and Gurr’s study of a category of Petri which models linear logic (see [6])—the morphisms are forms of simulations. It presents a method for proving temporal properties of the behaviour a Petri net. The analysis of dynamic behaviours is based on particularly simple nets (test nets), and temporal properties of a complex net are established by considering morphisms between it and various test nets. The main result is the syntactic characterisation of two expressive classes of formulae: those whose satisfaction is preserved by morphisms and those whose satisfaction is reflected.

Hardware

At Göteborg there is research into an application of noncommutative linear logic to hardware. Two papers of Carolyn Brown and Graham Hutton are in preparation: “The Geometry of Relational Programs” and “Categories and Allegories for Circuit Design”. Ruby is a calculus developed by Jones and Sheeran for describing and designing circuits. The approach aims to derive executable terms from specifications by application of a small set of rules. Ruby terms denote binary relations, and larger terms are constructed from smaller terms using operators of relational calculus. There is a geometric interpretation of Ruby terms as networks of primitive relations connected by wires, which is crucial when circuit layout is considered in Ruby derivations and is also widely used for informal reasoning about Ruby terms. The theory of allegories helps formalise the pictorial interpretation of Ruby terms and algebraic laws, which has not previously been made precise. The formal notion of network allows a precise definition of executable Ruby terms. It is intended to implement the formalisation in Hutton’s existing interpreter for Ruby terms.

[1] S. Abramsky and R. Jagadeesan, Games and Full Completeness for Multiplicative Linear Logic. Extended abstract appeared in Proceedings of FSTTCS 92, Springer LNCS 652. Full version to appear in Journal of Symbolic Logic, 1993.

[2] S. Abramsky and R. Jagadeesan, Games and Full Completeness for Simple Types. Paper in preparation for Proceedings of First Linear Logic Workshop, 1993.

[3] Benton, Bierman, Hyland, de Paiva , Term assignment for intuitionistic linear logic. TR 262, Computer Lab, Cambridge University, 1992.

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

[5] Benton, Bierman, Hyland, de Paiva , Linear Lambda-Calculus and Categorical Models for intuitionistic linear logic Revisited. In CSL’92, to appear in the LNCS Series, 1993.

[6] Brown, C., and Gurr, D., A Linear Specification Language for Petri Nets, accepted for MSCS.

[7] Brown, C., and Gurr, D., Temporal Logic and Categories of Petri Nets. Appears in Proc ICALP 1993

[8] Cattani, G., Modelli categoriali per la logica lineare. Tesi di laurea, Dipartimento di Matematica, Università di Parma, December 1992.

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

[10] Degano,P-P., Gorrieri, R., and Rosolini, P., A categorical view of process refinement. In Procs. of the REX Workshop on Semantics: Theory and Applications (J. de Bakker, W.-P. de Roever, G. Rozenberg ed.), volume 666 Lectures Notes in Computer Science, 1992, pag. 138–154. Springer-Verlag.

[11] de Paiva, V., and Ritter, E., ”Syntactic Multicategories and Categorical Combinators for Linear Logic” by , accepted for CTCS’93, Amsterdam.

[12] Engberg,U., and Winskel, G., Completeness results for linear logic on Petri nets. Extended abstract in proceedings of MFCS 93, Poland (1993).

[13] Engberg,U., and Winskel, G., Completeness results for linear logic on Petri nets. Full version of above, submitted to Annals of Pure and Applied Logic. Available as DAIMI PB 435, April 1993.

[14] Hyland, J.M.E.,and de Paiva, V., “Full Intuitionistic Linear Logic”. To appear in Annals of Pure and Applied Logic.

[15] J. M. E. Hyland and C.-H. L. Ong ”Fair Games and Full Completeness for Multiplicative Linear Logic without the MIX-rule” (Working Draft), 29 pages.

[16] Joyal, A., Nielsen, M., and Winskel, G., Bisimulation and open maps. Extended abstract in LICS 93 proceedings. A full version is being written for a LICS 93 special issue of Information and Computation.

[17] Nesi, de Paiva V., and Ritter E., Rewriting Properties of Combinators for Intuitionistic Linear Logic. Accepted for HOA’93, Amsterdam.

[18] Sassone, V., Nielsen, M., and Winskel, G., A classification of models for concurrency. Submitted to CONCUR 93.

[19] Sassone, V., Nielsen, M., and Winskel, G., Deterministic behavioural models for concurrency.To appear in proceedings of MFCS 93, Poland (1993).

[20] Nielsen, M., and Winskel, G., Trace structures and other models for concurrency. Invited chapter for the “Trace Book”, editors Diekert, V., and Rozenberg, G.

[21] Soloviev, S., Reductions in Intuitionistic Linear Logic (extended abstract). In CTCS (Category Theory and Computer Science) Proceedings, Amsterdam, 7-10 September 1993.

[22] Soloviev, S., A Complete Axiom System for Isomorphism of Types in Closed Categories. In proc of LPAR-93 S.Petersburg, Published in LNAI (Lect.Notes in Art.Int.) v.698, 1993.

[23] Winskel, G. and Nielsen, M., Models for concurrency. To appear as a chapter in the Handbook of Logic and the Foundations of Computer Science, Oxford University Press, 1994.

5.8 Report on Topic H: Computational Content of Classical Proofs

5.8.1 Summary

This report describes work done during Year 1 on Topic H (computational content of classical proofs). This topic contributes to the project objectives in the areas of “Type Theory” and “Semantics and Logics of Programming Languages”. The deliverable planned for milestone 1 was to pursue the analysis of the use of point-free topology in order to get constructive proofs using the notion of inductive definition.

We have made progress in this area. A new example has been analysed by this method: the topological proof of Van der Waerden’s theorem on arithmetical progression. Furthermore, the computational behaviour of the classical proof of Higman’s lemma, in the special case of binary words, has been completely explicited [2].

A closely connected work has been done in a game theoretical analysis of proofs in classical arithmetic. There is an unexpected simple connection with A. Blass’ interpretation of intuitionistic propositional logic: a cut-free classical proof of A is exactly a winning strategy for the game R(A) (with Blass’ notations). This provides a very intuitive description of cut-free proofs, and it does suggest new way of combining cutfree proofs that are described below. Hugo Herbelin has shown the connection between Gentzen’s cut-elimination and the interaction between strategies [9]. The next natural step will be to relate this work to the game-theoretical and dialogue interpretation of processes and sequentiality at higher type developped in Imperial College and Cambridge.

5.8.2 Work completed

5.8.2.1 Point-Free Topology

Thierry Coquand has presented in [4] a possible analysis of Ramsey’s theorem. It has been confirmed by Gavin Wraith that some tools used for this analysis are indeed close to others used in topos theory (for instance the lemma C in [10]). The question raised on this article of a more explicit description of the algorithm associated to this proof has been carried out by Daniel Fridlender, in a Licensiate Art thesis work, to be defended in october 93, using tools developed in the B.R.A. Types and Proofs.

Thierry Coquand has used ideas of point-free topology in order to give a constructive version of the topological proof of Van der Waerden’s theorem on arithmetical progression [3]. This involves a point-free version of the existence of minimal dynamical system, in a special concrete case. This may be seen as a first step of, and give some insights for a point-free theory of dynamical system.

5.8.2.2 Classical Arithmetic

Thierry Coquand has presented in [5] a game theoretical interpretation of Gentzen’s cut-elimination. Some connections have been made with the work of Novikoff and a simplified version of his proof has been presented. This can be also as a quite suggestive way of describing some cut-free proofs in ω-logic. In particular, this gives an alternative argument explaning why cut-elimination holds, as a proof of finiteness of “internal chattering” like in the theory of communicating processes. Furthermore, this suggests a new way of combining cut-free proofs. If one uses the notation of Blass [1], a classical proof of a formula A is defined as a winning strategy for the game R(A). In [5], it is shown that there are three natural composition maps

R(ΣA_{i}) × R(ΣB_{j}) → R(ΣA_{i}B_{j}).

One of these composition gives an alternative way of performing the “ternary” cutelimination of proofs of A_{1} + A_{2}, ¬A_{1}, and ¬A_{2} + B, if B is a Σ_{1}^{0} formula.

5.8.3 Future plans

The next step in the work of point-free topology should be to look at concrete examples involving topological spaces that are “classically very big”, such as the space of ultrafilters over N. There is a quite elegant proof by Glazer (presented in [8]) of Hindman’s theorem involving this space. A point-free formulation of this proof would be extremely interesting. It is not at all clear if it is possible to do this proof in the framework of inductive definitions. This analysis may provide some new insights on the problem of a constructive interpretation of classical analysis. This should be closely connected to the work of formalization of point-free topology in Intuitionistic Type Theory.

The work presented in [2] will be completed, probably in a joint paper with Hugo Herbelin and Daniel Fridlender. We want to describe how algorithms can be extracted from an intuitionistic proof, and how they can be seen as a possible constructive content of the minimal bad sequence argument. The method seems to be general and applies to the work of [7]: one first program we get from the intuitionistic proof is a program with continuations (which correspond to the use of bar-induction). The next step is to write a first-order interpreter for these programs. This is then a first-order program, which is equivalent to the original higher-order program. In the case of Higman and Ramsey, we get a first-order program which gives a clear and suggestive description of the computational content of the original proof. In particular, it can be shown that the algorithm we get is not the “while loop algorithm”, which given u_{1}, u_{2}, … compares successively all u_{i} to u_{j} for i⟨j.

The work of Daniel Fridlander [7] has confirmed that there are potential connections between this constructive analysis of topological proofs in combinatorics, and the game theoretic interpretation of classical proofs. More precisely, it has been shown that the algorithm we get for the intuitionistic Ramsey theorem can be seen as a constructive content of a natural classical proof of Ramsey’s theorem. An analysis of this and similar examples should point out the way to the extension of the game theoretical interpretation of classical arithmetic to stronger theories, with function symbols and quantification over functions.

Finally, the work on game theoretical interpretation of classical arithmetic should be connected to the work on game interpretation for processes and analysis of sequentiality at higher type done in Cambridge and Imperial College. It may be interesting to see if Hugo Herbelin’s work on classical sequent calculus could be adapted to intuitionistic sequent calculus, and connect this with the work of Felsher [6] and dialogue interpretations of PCF.

5.8.4 References and selected publications

[1] A. Blass Degrees of indeterminacy of games Fundamenta Mathematicae, LXXVII, (1972), 151-166.

[2] Th. Coquand A proof of Higman’s lemma by structural induction invited paper presented at the Takeuti’s conference, Luminy, July 1993

[3] Th. Coquand A constructive topological proof of Van der Waerden’s theorem draft paper

[4] Th. Coquand Another Proof of the intuitionistic Ramsey Theorem Theoretical Computer Science 115, (1993), 63-75

[5] Th. Coquand A Semantics of Evidence for Classical Arithmetic to appear in the Journal of Symbolic Logic

[6] W. Felsher Dialogues as a Foundation for Intuitionistic Logic in D. Gabbay and F. Guenthner (eds.) Handbook of Philosophical Logic, Vol. III, (1985), 341-372

[7] D. Fridlender Intuitionistic Ramsey Theorem, Formalizations and Programs Dissertation for the Licensiate Degree in Computer Science, automn 1993

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

[9] H. Herbelin Weak reduction in sequent calculus to appear as a Tech. Report, University of Lyon

[10] I. Moerdijk and G. Wraith Connected Locally Connected Toposes are Path-Connected Transactions of the American Mathematical Society 295, (1986), 849-860

Aim of report (Article 6.1.b): to enable the Commission to evaluate the progress and cooperation in respect of the work under contract, and in respect of the contract and any set of related research projects performed by different???? contractors in the framework of a Community Research Programme.

Interactions. Pitts visits Göteborg 21-24/03/93 Ritter visits Göteborg 10-16/05/93 Interaction with related research projects. Topic H is highly relevant for BRA-TYPES. Chalmers is also a site of this action. Actually, the explicit development of proofs in point-free topology using inductive definitions on a machine has been essential here.

Coquand, Dybjer, and Herbelin participated in the annual BRA-TYPES workshop in Nijmegen 24-28/05/93

5.9 Report on Topic I: Symbolic Computation

In Gothenburg, Catarina Coquand has made an analysis of simply-typed lambdacalculus with explicit substitution done mechanically. This work has been presented presented at CSL 93, Swansea. Thierry Coquand and Peter Dybjer have worked on the internalization of normalization theorems in Type Theory.

The theory of higher dimensional rewriting invented by Albert Burroni has been developed by Yves Lafont (CAIMENS, presently in Laboratoire de Mathématiques Discrètes, CNRS, Marseille) in two directions:

• higher dimensional rewriting as a generalization of term rewriting [1],

• higher dimensional rewriting as an algebraic theory of computation [2].

In [1], he introduces the 2-dimensional syntax for finitely presentable monoidal categories. He gives the basic examples of such finite presentations:

• 3 generators and 7 equations for the category of finite maps,

• 5 generators and 17 equations for the category of finite relations.

The first case is crucial for embedding terms into this syntax. Some equational theories which are not naturally expressed by means of terms, for example Hopf algebras, braids or knots, are very nicely expressed in this framework. This paper should serve as a reference for future work on symbolic computation, including a theory of 2-dimensional rewriting, which seems to be harder than expected, and the design of software for interactive diagrammatic reasoning.

In [2], he explains a recent result of Craig Squier in terms of 2-dimensional rewriting. Squier’s new condition is a kind of non abelian invariant for monoids which allows to discriminate some monoid which cannot be presented by means of a finite complete rewriting system. To sum up, this paper shows strong connections between the following topics:

• word problems,

• complete rewriting systems,

• higher dimensional rewriting,

• homology of monoids.

All this is also connected with coherence theorems in category theory.

[1] Yves Lafont Equational reasoning with 2-dimensional diagrams (preliminary version)

[2] Yves Lafont A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)

Both papers are available by ftp anonymous in /pub/lafont.

5.10 Appendix A: A Categorical Abstract Machine for the Calculus of Constructions

Background I define in my thesis [Rit92] categorical abstract machines for the Calculus of Constructions, a special higher-order λ-calculus. I start with the derivation of categorical combinators, i.e. an equational theory based on a categorical structure for the calculus. It turns out that only a generalization of Ehrhard’s D-categories [Ehr88] can be used for this purpose; all other categorical structures modelling the calculus yield only conditional equations or no equations at all. Next I orient the equations to obtain reduction rules. When I want to show that this reduction corresponds to reduction in the calculus, I run into difficulties in proving strong normalization. I can only show that any reduction that leads first to a combinator corresponding to a weak head-normal form is finite. These results are the key to formulate an eager and a lazy strategy for the reduction of a combinator to its normal form.

I then construct abstract machines for the eager and lazy strategy. Their correctness proof consists of an induction over the definition of the reduction strategies. These machines specialize to the CAM [CCM87] and Krivine’s machine [Kri85] [Cur91] in the first-order case respectively. The original construction of the CAM is based on cartesian closed categories (CCC’s). They model both environments and terms by morphisms regardless of their conceptual difference, whereas the D-categories separate theses two notions. Hence the correspondence between the D-categories and the abstract machines described in my thesis is closer than that between the CAM and the CCC’s. I also obtain an abstract machine for type checking of these combinators, which uses the above reduction machines.

The implementation I implemented the eager and the lazy machine in SML. These machines accept terms of the Calculus of Constructions as input and produce its type and its normal form (if well-typed) as output. I used Church-numerals to compare the efficiency of my machine with other implementations, namely LEGO [LP92] and Coq [DFH^{+}91]. The reduction of the term corresponding to the expression 2^{12} to its normal form, which is the Church-numeral 4096, yields the following results:

User Garbage collection
Eager Machine  4.20s  0.07s
Lazy Machine  2.85s  4.77s
LEGO  1102.62s  1118.13s
Coq  25.65s  66.57s

Execution Times for Reduction of 2^{12} to Normal Form

These results are quite encouraging and show that these machines are an efficient alternative to previous ones. Moreover, the implementation was straightforward because every transition of the machine is captured by an alternative in a case-statement.

[CCM87] Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine. Science of Computer Programming, 8:173–202, 1987.

[Cur91] Pierre-Louis Curien. An abstract framework for environment machines (Note). Theoretical Computer Science, 82(2):389–402, 1991.

[DFH^{+}91] Gilles Dowek, A. Felty, Gérard Huet, H. Herbelin, Christine Paulin-Mohring, and B. Werner. The system Coq. Users Guide, 1991.

[Ehr88] Thomas Ehrhard. A categorical semantics of constructions. In Third Annual Symposium on Logic in Computer Science, pages 264–273. IEEE, 1988.

[Kri85] J.-L. Krivine. Un interpréteur du λ-calcul. Unpublished, 1985.

[LP92] Zhaohui Luo and Robert Pollack. Lego proof development system: User’s manual. Unpublished Manuscript of the University of Edinburgh, May 1992.

[Rit92] Eike Ritter. Categorical Abstract Machines for Higher-Order Lambda Calculi. PhD thesis, University of Cambridge, 1992. Also available as Technical Report No. 297.

5.11 Appendix B: Report on implementation of LiLac

Lilac A prototype functional programming language based on Linear Logic has been developed at Imperial College to conduct experiments to determine the usefulness of Linear Logic proof terms (Linear Lambda Calculi) as a programming language [Mac93]. This preliminary version consists of a small environment where programs can be edited and executed. The 3000 lines of code is written in Standard ML.

The main aim of this research is to look closer into the notion of reduction in the λ-calculus by using more refined calculi with explicit substitutions, copying and discarding. Linear Logic proof terms provide a solid basis for a more refined implementation:

• Substitutions are made explicit: indeed the progress of a substitution through a term appears as explicit steps in the cut-elimination process.

• Copying an argument corresponds to the contraction rule of the logic. Knowing that an argument is not copied tells us that we can perform In-place updates safely.

• Discarding an argument corresponds to the weakening rule of the logic. Knowing that an argument is discarded tells us that it is not strict in that argument.

The philosophy behind Lilac is a very explicit language where the programmer is very much aware of the resource manipulations of the algorithm. Lilac is a very small strongly typed functional programming language without many of the advanced features found in languages such as Standard ML.

Examples:

A small script is shown below to give the flavour of the language. The functions are shown together with their types generated by Lilac.

fun square (!x@!y) = x ∗ y ;

square : !nat −∘ nat fun S f g (y@z) = fy(gz) ;

S : (!α −∘ β −∘ γ) −∘ (!α −∘ β)−∘!α −∘ γ fun K x = x;

K : α−∘!β −∘ α fun fst < x, >= x ;

fst : α&β −∘ α funrec length ( : t) = let length be !len in 1 + len(t) end

length [ ] = let length be in 0 end ; length : !(list(!α) −∘ nat)

funrec sum (h : t) = let sum be !s in h + s(t) end sum [ ] = let sum be in 0 end ; sum : !(list(nat) −∘ nat)

BIBLIOGRAPHY 87 [Mac93] I.C. Mackie. Lilac: A functional programming language based on linear logic.

Journal of Functional Programming, 1993. To appear.

5.12 Report on Workshop on Evaluation Logic and Synthetic Domain Theory

The first workshop of CLICS II was held in Cambridge on the 9th and 10th of January 1993. The topic announced in the proposal as Evaluation Logic (EL) was extended to include Synthetic Domain Theory (SDT), since at the least the question of whether SDT could be used to provide good models for EL seemed like a good test of the value of the SDT point of view.

The meeting was attended by 20 people from seven of the sites contributing to the project and also by a student from Edinburgh. The effective organizers (Hyland, Moggi and Pitts) spent the week 4th to 8th January together in Cambridge preparing the meeting. The workshop was organized around a series of formal presentations and closed with an extended structured discussion. There was also time for informal discussions.

The main stress of the workshop was on Evaluation Logic. Significant issues arose, the most obvious being the clear incompatibility which emerged between propositions which seem valid for logics of dynamic allocation (Pitts and Stark) and those valid in the interpretations described by Moggi. It may be that there are many variants of evaluation logic. A consciously divided approach emerged in the discussion. On the one hand it seems good to persevere with interpretations of the simple ‘extensional’ kind developed by Moggi; on the other hand the importance of the problems addressed by Pitts and Stark was accepted, and the possibility of a closer pragmatic study of the semantics of references was considered. In addition there were presentations of the basic ideas of Synthetic Domain Theory, and a suggestion for research on LCF-style logic in the context of SDT was outlined. In the final discussion a number of tentative workplans for the future agreed. These formed the background to much of the research reported on under Topics E and F at the 1st milestone, as well as that on SDT reported in Topic B. Thus the workshop formed a valuable part of the overall CLICS II initiative.

BIBLIOGRAPHY 89 Programme of the workshop Saturday 9th January

10.00am Andrew Pitts Is there such a thing as evaluation logic?
11.15am  Coffee
11.30am  Eugenio Moggi Completeness results for evaluation logics
1.00pm  Lunch
2.30pm  Martin Hyland Survey of synthetic domain theory
3.45pm  Tea
4.15pm  Valeria de Paiva Computational Types from a Logical Perspective

Sunday 10th January

10.00am Ian Stark Dynamic Allocation of Store
11.15am  Coffee
11.30am Paul Taylor Elementary Theory of Σ-spaces

List of those attending

C. Brown (Chalmers) R. Crole (Imperial) P. Dybjer (Chalmers)
T. Ehrhard (CAMIENS)  Y. Fu (Manchester) L. Hallnas (Chalmers)
B. Hilken (Manchester)  M. Hyland (Cambridge) J. Longley (Edinburgh)
P. Malaccaria (CAMIENS) E. Moggi (Genova) L. Ong (Cambridge)
V. de Paiva (Cambridge)  A. Pitts (Cambridge) E. Ritter (Cambridge)
G. Rosolini (Genova)  D. Rydeheard (Manchester) A. Schalk (Darmstadt)
H. Simmons (Manchester)  I. Stark (Cambridge) P. Taylor (Imperial)

BIBLIOGRAPHY 90

5.13 Preliminary Programme of Workshop on Games, Logic and Processes

TUESDAY (5/10/93)
9:15 WELCOME
9:30 Jean-Yves Girard (Marseille - LMD)
Denotational semantics and geometry of interaction: towards a
unified approach
10:30 Francois Lamarche (London - Imperial)
Coalgebras as a foundation for abstract syntax
11:30 Sergei Soloviev (Aarhus)
Reductions in linear logic
12:30 LUNCH
14:30 Martin Hyland & Luke Ong (Cambridge)
Linear Logic, Fair Games, and Full Completeness Theorem
15:30 discussion on semantics and completeness
17:00 Louis-Andre Gerard-Varet (Marseille - GREQE)
Logical problems in recent developpments in non cooperative game
theory
19:30 DINNER
WEDNESDAY (6/10/93)
9:30 Yves Lafont (Marseille - LMD)
A new finiteness condition for monoids presented by complete
rewriting systems
10:30 Andy Pitts (Cambridge)
Observational equivalence versus applicative equivalence in the
presence of local state
11:30 Eugenio Moggi (Genova)
Evaluation Logic : an update + what's next?

12:30 LUNCH
14:30 Glynn Winskel (Aarhus)
Bisimulation and open maps
15:30 Paul Taylor (London - Imperial)
Synthetic domain theory and Stone duality
19:30 DINNER
THURSDAY (7/10/93)
9:30 Thierry Coquand (Gothenburg)
Composition of classical cut-free proofs via the proof-as-strategy
interpretation
10:30 Hugo Herbelin (Paris - INRIA)
Cut-elimination and interaction between strategies
11:30 Glynn Winskel (Aarhus)
Bistructures, bidomains and linear logic
12:30 LUNCH
14:30 Thomas Ehrhard (Paris - ENS)
Hypercoherences
15:30 Samson Abramsky (London - Imperial)
Games and Full Abstraction for PCF
20:00 BANQUET
FRIDAY (8/10/93)
REVIEW MEETING