CLICS II

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

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

3rd Periodic Progress Report

September 5th, 1995

DRAFT

Contents

1 Executive summary 2 1.1 Milestones and Deliverables . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 External Contacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

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

3 Workpart Summaries 5 3.1 Progress on Deliverables . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Site management report for Imperial . . . . . . . . . . . . . . . . . . 8 3.3 Site management report for Aarhus . . . . . . . . . . . . . . . . . . . 9 3.4 Site management report for CAIMENS (not available) . . . . . . . . 12 3.5 Site management report for Cambridge . . . . . . . . . . . . . . . . . 12 3.6 Site management report for Genova . . . . . . . . . . . . . . . . . . 14 3.7 Site management report for Chalmers . . . . . . . . . . . . . . . . . 15 3.8 Site management report for TH Darmstadt . . . . . . . . . . . . . . 16 3.9 Site management report for GMD (not available) . . . . . . . . . . . 19 3.10 Site management report for Manchester . . . . . . . . . . . . . . . . 19 3.11 Site management report for Sussex . . . . . . . . . . . . . . . . . . . 21

4 Deliverables Overview 23

5 Deliverables 24 5.1 Topics A & G: Sequentiality and Stability, and Applied Linear Logic 24 5.2 Report on topic B: Duality in Domain Theory . . . . . . . . . . . . . 29 5.3 Report on topic C: Logic of Inductive and Recursive Datatypes … 36 5.4 Report on topic D: Subtypes and polymorphism in higher order lan-

guages. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5.5 Report on topic F: monadic programming language semantics …. 40 5.6 Report on topic H: Computational Content of Classical Logic …. 43 5.7 Report on topic I: Symbolic Computation . . . . . . . . . . . . . . . 45

A  46

A.1 Joint CLICS-TYPES workshop . . . . . . . . . . . . . . . . . . . . . 46 A.2 Workshop on Full Abstraction of PCF and Related Languages … 48 A.3 Semantics of Computation . . . . . . . . . . . . . . . . . . . . . . . . 50 A.4 School on Semantics and Logics of Computation . . . . . . . . . . . 53

Chapter 1

Executive summary

1.1 Milestones and Deliverables

The CLICS II project started on October 1st 1992. The third Milestone occurs after 36 months. The third Review meeting will take place in Cambridge on September 5th 1995. 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 Leaders”. 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. Hard copies of these papers will be available at the review meeting.

The progress on the specific deliverables targeted for Milestone 3 (see Section 3.3 of the 2nd Periodic Progress Report) is summarized in Section 3.1 of this report. The overall picture is that there has been considerable progress on most of the targeted deliverables. Our general assessment is that the third year has been particularly concerned with integration of contributions coming from different strands of the project, with dissemination of information and results (particularly relevant are the semester on “semantics of computation” and the summer-school at the Newton Institute), and in seeking coordination with other projects and research communities (particularly relevant are the joint CLICS-TYPES workshop, and again the semester on “semantics of computation”). This is in line with the reviewers’ recommendations (contained in the reviewer’s report dated January 1995) regarding information dissemination activities.

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. In addition, there has been interactions with Edinburgh in the area of Axiomatic and Synthetic Domain Theory, through a Science Twinning, and with several other sites in Europe through the HCM Scientific Cooperation Network on “Lambda Calcul Typé”.

• Interaction with TYPES has been very lively, indeed we organized a joint CLICS-TYPES workshop in January 1995 at Chalmers (see Appendix).

• The semester on “semantics of computation” at the Newton Institute (see Appendix) is acting as a catalyst for CLICS, TYPES and CONFER. Moreover, it is stimulating the interactions between these research projects and more applied research via a series of thematic workshops.

• The workshop on Full Abstraction of PCF and Related Languages (see Appendix) has attracted most of the experts in the area, and was an important occasion both for deep technical discussions and for clarifying what problems are still open.

There was considerable activity by members of the project as regards information dissemination.

• Several members are lecturing at the Summer School on Semantics and Logics of Computation (see Appendix): Abramsky, Coquand, Hyland, Moggi, Pitts, Winskel. This summer school is an important occasion to transfer the know-how developed inside the project. Moreover, the lecture notes will be published as a volume in the CUP Newton Institute Lecture Series.

P. Aczel at a Nato Summer School on ”Semantics of Computation” (Marktoberdorf), while A. Pitts, A Gordon and J. van Oosten gave advanced courses at BRICS (Aarhus).

• H. Simmons has written a book on “Taking the Curry-Howard correspondence seriously” and a monograph on “First Steps in Modal Logic”.

The CLICS group at Darmstadt has organised a well-attended international workshop on “Logic, Domains and Programming Languages”, and a selection of the papers presented will be published in a special issue of MSCS (see Darmstadt site report).

• Various members of the project have been invited speakers at international conferences: G. Winskel at the CTCS conference (Cambridge, August 1995), K. Wagner at the 11th Summer Conference on General Topology and Applications (Gorham ME, August 1995), T. Coquand at Mathematics of Program Construction (Kloster Irsee, Germany, July 1995) and Foundations of Software Technology and Theoretical Computer Science (Madras, December 1994).

Others members have been invited speakers at specialized workshops: A. Jung at the MASK workshop (Mannheim, October 1994), K. Wagner and E. Moggi at the MASK workshop (Alghero, May 1995), Dybjer at the meeting on Mathematische Logik (Oberwolfach, April 1995) and the workshop on Automation of Inductive Proof (SchloßDagstuhl, July 1995),

Update on the worldwide state-of-the-art

The CLICS project comprises a considerable proportion of the state of the art over most of topics it addresses. Moreover, we have excellent contacts with the leading researcehrs in the areas relevant to the project. The following is a brief overview of work by others, which is particularly relevant to the topics of the project.

• Synthetic Domain Theory. John Longley (Edinburgh) has investigated several realizability models, some of them substantially different from those considered so far in the context of SDT. In collaboration with Alex Simpson, he has also introduced an alternative to the notion of replete object, well-complete object. Although they have considered it only in the context of realizability models, the construction seems to enjoy good properties also in other settings.

• Axiomatic Domain Theory. Plotkin has been working (for some time) on an axiomatization of categories of domains based on linear types. In collaboration with Fiore and Power, they are aiming at representation results for these categories. This work is still in progress, and the axiomatizations have not yet stabilized. However, they are likely to provide new insights and may prompt a revision at the level of semantic-based calculi/logics for reasoning about programs and set different standards for models of SDT.

• The workshop on Full Abstraction was a major occasion to compare different approaches and make precise what is left to do. At this stage it is still premature to say whether an approach is better than another. In any case, the game-theoretic approach pioneered by the project has been exceptionally fruitful in linking apparently unrelated subjects.

• John Reynolds and Peter O’Hearn have been able to capture certain features of Algol-like languages, namely local variables and irreversibility of state changes, via suitable translations in typed calculi featuring some form of parametric polymorphism and linear types. They have also some fairly simple models models for such calculi. It is not clear whether these results may be extended to languages like SML. However, they indicate that parametric polymorphism is an important tool for studying abstraction mechanisms.

• Very recently Udday Reddy has proposed an object based semantics for imperative languages, which seems able to capture in a relatively simple way notions like locality and irreversibility of state changes. This work is still at a very early stage, and it is not clear whether it can cope with more complex languages like SML (which have been targeted by Topic F).

Workpart Summaries

Scientific Workpart Summary

In this summary, we will overview the progress made on the deliverables for Milestone 3 described in Section 3.3 of the 2nd Periodic Progress Report. Since the project has been extended until December 1995, it is likely that further progress will be made. Indeed several member of the projects will take part in the programme on “Semantics of Computation” in the period October–December 1995.

3.1 Progress on Deliverables

Significant progress has been made on most of the items mentioned in the Deliverables for Milestone 3 described in Section 3.3 of the 2nd Periodic Progress Report, although in some cases there were unexpected complications. Moreover, as promised in Section II-4.2 of the Technical Annex, a Summer School will be held in Cambridge (25-29 September 1995), and lecture notes for the school will be published by CUP. A full account, including additional work done under the aegis of CLICS II, can be found in the Topic Reports in Chapter 5. Worth pointing out is the solution by Soloviev of an old conjecture by MacLane (see report on Topic A and G).

Topic A (continuation)

• Models of PCF based on a modified notion of bistructure This have been investigated by Winskel, who has incorporated ideas from hypercoherences, moreover additional notions of domains are under investigation in relation to game semantics (see report on topic B).

• Connections between hypercoherences, logical relations and other presentations of the fully abstract model. These were investigated at the full abstraction workshop, but not clear links have been established, yet.

Moreover, various connections between games and more operationally presented calculi (Milner’s π-calculus and Parigot’s λμ-calculus) have been established by Hyland, Ong and Ritter. Abramsky’s has introduced a notion of typed realizability, which seems useful in a variety of contexts, not necessarily related to game semantics.

Topic B

• Extension of the maximality results. These results have been extended to the bounded complete setting.

• Domain theory in logical form in the continuous case. There has been major progress by Jung and Sünderhauf.

• Applications of Stone Duality to static data types. These have made use of the snack-powerdomain.

As part of the integration effort, Hyland and Moggi have investigated the replete construction in a fibered setting. Moreover, there has been important work on probabilistic powerdomains.

Topic C (continuation)

• Categorical modeling of type theory. A new notion of categorical model for dependent types has been introduced, which is closer to the syntax than previously proposed notions.

• Simultaneous induction-recursion and applications. Categories with families have been used to represents type-theory inside itself, while simultaneous inductive definitions have been used to establish the correctness of this representation.

Moreover, Altenkirch, Streicher and Hofmann have clarified the connection between reduction-free normalization proofs and categorical glueing. Andy Gordon has considered applications of various forms of co-induction to establish equational laws for a functional language with a rich type structure.

Topic D.

• Test of the model construction for parametric polymorphism. This has been tested on those models which can be obtained from an internal complete category. In the case of models obtained from fibrations of domains, it is not clear if a parametric completion can be obtained because these models do not have all limits.

• Adapt the semantic construction to generate models for system R. This has not been worked out, yet. However, a first attempt suggests that the approach to logical relations proposed by Hermida should be relevant.

Topic E (integration effort, see report on topic F).

• A first proposal for LCF++. This has been formulated in the context of a type theory, by combining ideas from Axiomatic and Synthetic Domain Theory, and revising the notion of computational type.

Topic F.

• Extend the model of the Store Calculus to interpret Evaluation Logic, and test it use for proving properties of SML programs. As preliminary to this, Pitts and Ritter have considered a translation from SML to the Store Calculus, and prove that it is fully abstract. The proof is not trivial, and makes essential use of applicative bisimulation.

Moreover, Moggi (in collaboration with Fiore and Sangiorgi) has given a fullyabstract model for the π-calculus, by applying existing semantics techniques.

Topic G.

• Sheaf models for refinement and weak bisimulation. These models present substantial technical advantages w.r.t. more concrete models (e.g. event structures), and still support a notion of refinement and weak bisimulation.

Moreover, Lafont has identified a simple system of interaction combinators, in which any other system can be faithfully represented.

Topic H.

• Investigate connections between game semantics of PA and game semantics for processes and for sequentiality. Curien reported on this at the full abstraction workshop, but no firm results are available, yet.

• Computational interpretation of proofs in classical analysis with the Axiom of Choice. Coquand has formulated a general way of extracting computational content of some classical proofs using the axiom of choice.

Topic I.

• An interactive tool for manipulating diagrams. Such a tool has been developed at Marseille by Anne Massol under the supervision of Yves Lafont.

• General theory for rewriting Penrose. We have not reached a satisfactory level of generality, yet.

Management Workpart Summary

3.2 Site management report for Imperial

People working on the project

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

EPSRC-funded Research Fellows: Paul Taylor (1 man-month), Duško Pavlović (3 man-months)

EPSRC-funded Research Assistant: Antonio Bucciarelli (6 man-months).

External Collaborator: Pasquale Malacaria (HCM fellow at ENS, Paris), 3 manmonths.

EPSRC-funded Research students: Guy McCusker (3 man-months).

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

These people made contributions to the following Topics in the project Workplan:

Topic A: Abramsky, Malacaria, McCusker, Bucciarelli. Topic B: Taylor, Vickers. Topic G: Abramsky, Lamarche, Pavlović.

Interaction with other sites

Imperial has had important interactions with a number of other project sites during the review period:

1. Cambridge. The Newton Insitute for Mathematical Science will host for six months (July 95 - December 95) conferences and activities in the domain of Theoretical Computer Science. Samson Abramsky is the main organiser of the event. Leading scientists from all over the world are providing an exceptional forum of ideas on major issues as semantics, types, languages. Major progresses have been achieved in clarifing the relationships between different game semantics. In particular Guy McCusker has developed a version of game semantics synthesizing features of the Imperial and Cambridge approaches.

2. CAIMENS. Antonio Bucciarelli, which has been working at ENS in the last years took up a position at Imperial starting from July 94. Pasquale Malacaria is visiting Imperial Their presence has been very helpful in maintaining the flow of ideas and contacts between the two sites.

3. Aarhus. A two weeks workshop on “Full Abstraction for PCF and related languages” has been held in April 95. Imperial contributed with lectures on the game semantics approach to full abstraction (Samson Abramsky and Pasquale Malacaria gave two lectures each). Antonio Bucciarelli gave a talk on refining models of types lambda-calculi by logical relation.

Conferences attended

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

Peripatetic Seminar on Sheaves and Logic, Tours (February 1995), attended by Paul Taylor.

BRICS Workshop, Aarhus (March 95), attended by Samson Abramsky, Antonio Bucciarelli, Pasquale Malacaria

Mathematical Foundations of Programming Semantics, New Orleans U.S. (april 95), attended by Francois Lamarche.

Logic in Computer ScienceSan Diego (June 1995), attended by Guy McCusker, Francois Lamarche

Themes on Semantics of Computation Cambridge (July 1995), attended by Samson Abramsky and Pasquale Malacaria

Category Theory in Computer Science Cambridge (August 1995), Attended by Samson Abramsky, Dusko Pavlovic, Paul Taylor

Oberwolfach meeting on descent theory Attended by Dusko Pavlovic

Publications

Samson Abramsky, Radha Jagadeesan and Pasquale Malacaria, Full Abstraction for PCF, In the proceedings of Theoretical Aspects of Computer Science.

Samson Abramsky and Guy McCusker, Games and Full Abstraction for the Lazy Lambda-calculus, in Proceedings of 10th Annual IEEE symposioum on Logic in Computer Science

Samson Abramsky and Guy McCusker Games for Recursive Types in Theory and Formal Methods 1994: Proceedings of the Second Imperial College, Department of Computing, Workshop on Theory and Formal Methods World Scientific/IC Press 1995.

Antonio Bucciarelli Degrees of parallelism in the continous type hierarchy accepted for publication in Theoretical Computer Science

Steve Vickers Locales are not pointless in Theory and Formal Methods 1994: Proceedings of the Second Imperial College, Department of Computing, Workshop on Theory and Formal Methods World Scientific/IC Press 1995.

François Lamarche, Games semantics for full propositional linear logic in Proceedings of 10th Annual IEEE symposioum on Logic in Computer Science

François Lamarche, A generalisation of coherence spaces and hypercoherences in Proceedings of Mathematical Foundation of Computer Science

Dusko Pavlovic On Completeness and cocompleteness in and around small categories in Annals of Pure and Applied Logic 1995

Dusko Pavlovic Maps I: relative to a factorisation system in Journal of Pure and Applied Algebra 1995

Dusko Pavlovic A Categorical Setting for the 4-Colour theorem in Journal of Pure and Applied Algebra 1995

Dusko Pavlovic Convenient categories of processes and simulations I: modulo strong bisimilarity in Category Theory and Computer Science 95 Springer Verlag

Duscko Pavlovic Chu I: cofree equivalence, dualities and *-autonomous categories to appear in Mathematical Structures in Computer Science

3.3 Site management report for Aarhus

3.3.1 People working on the project

• Permanent members of staff : Glynn Winskel has contributed about 4 man months. Mogens Nielsen has each 1 man month.

• Contract research workers: Sergei Soloviev has been employed by the project since January 1993, and so has contributed 24 man-months. Claudio Hermida, also employed by the project since September 1993, has contributed 18 man months . Since July ’94, Vladimiro Sassone has been employed in a postdoctoral position at Aarhus, funded by a HMC grant administered by Mogens Nielsen. Jaap van Oosten is employed full time since January 1994 at BRICS, funded by the Danish National Research Foundation; his work on realisability and constructive mathematics is highly relevant to CLICSII.

• Research students: Torben Brauner, Bettina Blaaberg Sørensen, Gian Luca Cattani, and just recently Thomas Hildebrandt, are working towards PhD’s full time; Their research areas fall within CLICSII.

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Sergie Soloviev and Claudio Hermida. The above people contributed to the following Topics in the project Workplan:

Topic A: Winskel, Soerensen. Topic D: Hermida, Soloviev. Topic G: Brauner, Nielsen, Soloviev, Winskel, Cattani,Soloviev.

3.3.2 Interaction with other sites

During the review period, Aarhus has had significant interactions with the project sites.

• Cambridge (Winskel is a participant of the Newton programme, Pitts’ visit to Aarhus)

• Sussex (Robinson’s 2 month visit to Aarhus)

• Genova (Cattani’s discussions with Rosolini, Rosolini’s visit to Aarhus)

• Goteborg (Van Oosten, Hermida,Soloviev’s visit)

• Imperial (Abramsky’s visit to Aarhus, Van Oosten’s visit to Imperial)

• Marseilles (Ehrhard’s visit)

• Darmstadt (Winskel, plus Streicher and Jung’s visit to Aarhus)

Soloviev (Aarhus) and Longo and Milsted (Paris) have collaborated on papers addressing subtyping and polymorphism. In addition there have been fruitful exchanges with Ehrhard, Bucciarelli and Curien (Paris). BRICS at Aarhus ran a extended theme in “Logic in Semantics” and many CLICSII participants attended Aarhus either as guests or as participants in the Workshop on Full Abstraction of PCF and Related Languages.

3.3.3 Conferences attended

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

Logic in Computer Science, Paris, July 1995 ∗Workshop on Full Abstraction of PCF and Related Languages, BRICS, Aarhus, March 1995. ∗Joint Types/CLICS Workshop, Göteborg January 1995. Workshop on Logic and Domains, Darmstadt, May 1995. Conference in Category Theory in Computer Science and Mathematics, Cambridge, August 1995. ∗MASK meeting on structures for concurrency, Alghero (Sardegna), May 1995. ∗56 Peripatetic Seminar on Sheaves and Logic, Aarhus, December 1995. ∗57 Peripatetic Seminar on Sheaves and Logic, Genova, May 1995. ∗TAPSOFT, Aarhus, May 1995. ∗CAAP, Aarhus, May 1995.

3.3.4 Publications

[Braa] T. Braüner. The Girard Translation Extended with Recursion. Full version of paper to appear in Proceedings of CSL ’94, LNCS 933, 1995. (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/13/BRICS-RS-95-13.ps.gz)

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

[CN] A. Cheng and M. Nielsen. Open Maps (at) Work. April 1995. (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/23/BRICS-RS-95-23.ps.gz)

[EW95] Uffe H. Engberg and Glynn Winskel. Completeness results for linear logic on Petri nets. Accepted for Annals of Pure and Applied Logic, 1995.

[NW] M.Nielsen and G.Winskel. Petri Nets and Bisimulations. January 1995. To appear in TCS. (ftp.daimi.aau.dk) (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/4/BRICS-RS-95-4.ps.gz)

[SLM] G.Longo, K.Milsted and S.Soloviev A Logic of Subtyping Published in LICS-95 proceedings.

[JvO] Jaap  van  Oosten.  Fibrations

and Calculi of Fractions. November 1994. (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/94/37/BRICS-RS-94-37.ps.gz)

[Oos] J. van Oosten. Basic Category Theory. January 1995.(Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/LS/95/1/BRICS-LS-95-1.ps.gz)

[Sas1] V. Sassoe. An Axiomatization of the Algebra of Petri Net Concatenable Processes. To appear in Theoretical Computer Science.

[Sas2] V. Sassone. On the Category of Petri Net Computations. In Proceedings of the 6th International Conference on Theory and Practice of Software Development, TAPSOFT ‘95, LNCS n. 915, pp. 334–348, Springer-Verlag, 1995.

[SNW] V. Sassone, M. Nielsen, and G. Winskel. Models for Concurrency: Towards a Classification. To appear in Theoretical Computer Science.

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

[Sol1] S.Soloviev. Reductions in Intuitionistic Linear Logic Accepted for 4-th issue of Math.Structures in Comp. Sci., 1995.

[Win] G.Winskel. Hypercoherences. Manuscript, September 1994.

3.4 Site management report for CAIMENS (not available)

3.5 Site management report for Cambridge

3.5.1 People working on the project

• Permanent members of staff :

Andrew Pitts and Martin Hyland have each contributed about 4 man months.

• Contract research workers:

Francis Davey was employed as a Research Assistant by the project, and so has contributed 12 man months.

Valeria de Paiva was employed as a Senior Research Associate by the project from 1 March 1995, and so has contributed 7 woman months.

Ian Stark was employed as a Research Assistant by the project until 31 December 1994, and so has contributed 3 man months.

Nick Benton, Gavin Bierman, Andrew Gordon, Anrdea Schalk, and Kim Wagner each contributed about 1 man month.

• PhD students: Joshua Ross and Gareth Rees 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 Francis Davey (12 man months), Ian Stark (3 man months) and Valeria de Paiva (7 woman months).

These people made contributions to the following Topics in the project Workplan:

Topic A: Hyland. Topic B: Hyland, Wagner. Topic C: Gordon. Topic F: Paiva, Pitts, Stark. Topic G: Benton, Bierman, Hyland, Paiva.

3.5.2 Interaction with other sites

Several members of the Cambridge project site visited Marseille for an HCMP workshop on Proofs, Nets and Types, 7–10 Oct 1994.

Several members of the Cambridge project site visited Chalmers in January 1995 for the joint workshop of the CLICS-II and TYPES ESPRIT projects.

Pitts visited the Aarhus site for the period 21 Nov–2 Dec 1995 to give a lecture course on “Inductive and co-inductive techniques in the semantics of functional programs”. He also visited the Aarhus sitte for the period 17–23 Apr 1995, for the BRICS workshop on Full Abstraction.

T. Brauner (Aarhus) visited the Cambridge site for the period 9 Oct–11 Nov 1995.

The following other short visits were made:

04/10/94: visit of Hyland to Imperial College site. 09/11/94: visit of Pitts to Manchester site. 02/12/94: visit of D. Pavlovic (Imperial) to Cambridge.

09/12/95: visit of Pitts to Sussex site. 11-13/01/95: visit of Moggi (Genova) to Cambridge. 10-13/01/95: visit of Dybjer (Chalmers) to Cambridge. 05/95: visit of Wagner and Schalk to Darmstadt. 05/05/95: visit of M. Fernandez (LIENS) to Cambridge. 05/06/95: visit of K. Honda (Manchester) to Cambridge.

3.5.3 Conferences attended

The following conferences and workshops contained presentations of work done on the project at the Cambridge site. Project funds were used to cover attendance at the first of these.

Joint CLICS-II TYPES workshop (Chalmers, January 1995), Second International Conference on Typed Lambda Calculus and Applications (Edinburgh, April 1995), BRICS Workshop on Full Abstraction (Aarhus, April 1995), Eleventh Conference on the Mathematical Foundations of Programming Semantics (New Orleans, May 1995), 7th Annual ACM Conference on Functional Programming Languages and Computer Architecture (La Jolla CA, June 1995), Euroconference on Advances in Type Systems for Computing (Cambridge UK, August 1995), Summer School on Semantics and Logics of Computation (Cambridge UK, September 1995).

3.5.4 Publications

[BBdP95] P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective I. Technical Report 365, Cambridge Univ. Computer Laboratory, May 1995.

[Ben94] P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. Technical Report 352, Cambridge Univ. Computer Laboratory, October 1994.

[Bie95] G. M. Bierman. What is a categorical model of intuitionistic linear logic? In 2nd Int. Conf. on Typed Lambda Calculus and Applications, Edinburgh, 1995, volume 902 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1995.

[Gor95] A. D. Gordon. Bisimilarity as a theory of functional programming. In Eleventh Conference on the Mathematical Foundations of Programming Semantics, New Orleans, 1995, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.

[HO95] J. M. E. Hyland and C.-H. L. Ong. Pi-calculus, dialogue games and PCF. In Proceedings of 7th Annual ACM Conference on Functional Programming Languages and Computer Architecture, La Jolla, California. ACM, 1995.

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

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

[Sta95] I. D. B. Stark. Names and higher-order functions. Technical Report 363, Cambridge Univ. Computer Laboratory, April 1995.

[Wag] K.R. Wagner. Liminf convergence in omega-categories. Submitted for publication.

3.6 Site management report for Genova

3.6.1 People working on the project

• Permanent members of staff : Eugenio Moggi has contributed about 6 man months. Pino Rosolini has contributed about 6 man months.

• Research students: Daniela Archieri, Gianna Belle’.

These people made contributions to the following Topics in the project Workplan:

Topic B: Moggi, Rosolini. Topic D: Rosolini. Topic F: Moggi.

3.6.2 Interaction with other sites

The main interactions have been with Cambridge, Imperial College and Sussex????. The following visits were made (project funds were not used to cover visits marked with a ∗):

03-08/10/94 Moggi (Genova) visits Imperial College and Cambridge. ∗17-21/10/94 Reus (Munich) visits Genova. 01-06/12/95 Rosolini (Genova) visits Århus. ∗5-7/12/94 Moggi (Genova) visits INRIA Sophia-Antipolis. ∗10-23/12/94 Moggi (Genova) visits Jay at UTS (Sydney). ∗17-24/12/94 Rosolini (Genova) visits LMU, München. 07-12/01/95 Rosolini (Genova) visits Göteborg. 08-10/01/95 Moggi (Genova) visits Göteborg. ∗11-21/01/95 Moggi (Genova) visits Cambridge and Edinburgh. ∗05-11/02/95 Schewe (Hamburg) visits Genova. ∗22-24/02/95 Sangiorgi (INRIA Sophia-Antipolis) visits Genova. ∗05-14/03/95 Rosolini (Genova) visits Århus. ∗08/03-31/04/95 Lamarche (Imperial College) visits Genova ∗18/04-16/05/95 Paré (Halifax) visits Genova. ∗10-14/04/95 Moggi (Genova) visits Edinburgh. ∗24/04-05/05/95 Simpson (Edinburgh) visits Genova. ∗07-15/05/95 Power (Edinburgh) visits Genova. ∗18/06/95 Fiore (Edinburgh) and Sangiorgi (INRIA) visit Genova.

All the researchers at Genova have taken part in the programme “Semantics of Computation” at the Newton Institute (Cambridge).

3.6.3 Conferences attended

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

∗Computing: the Australian Theory Seminar Sydney, December 1994. 56th PSSL, Århus, December 1994. joint CLICS-TYPES workshop, Göteborg, January 1995. ∗twinning meeting, Edinburgh, April 1995. ∗58th PSSL, Genova, May 1995. ∗MASK workshop, Alghero, May 1995. “Themes in sem. of comp.” workshop, Cambridge, July 1995. CTCS conference, Cambridge, August 1995. Advances in type systems for computing, Cambridge, August 1995.

Work done in the project was also presented in a course taught by Moggi at the summer school Semantics and Logics of Computation Cambridge, September 1995.

3.6.4 Publications

[Bel95] Gianna Bellè. Syntactical properties of an extension of girard’s system f where types can be taken as generic input. In Italian Conference on Theoretical Computer Science, 1995.

[BR95] A. Bucalo and G. Rosolini. Repleteness and the associated sheaf, 1995. submitted for publication.

[HMar] J.M.E. Hyland and E. Moggi. The S-replete construction. In CTCS 1995, volume 953 of LNCS. Springer Verlag, to appear.

[Mogar] E. Moggi. Metalanguages and applications. volume ?? of CISM Lecture Notes. Springer Verlag, to appear.

[Ros95] G. Rosolini. Notes on synthetic domain theory, 1995. available by ftp from theory.doc.ic.ac.uk in directory imported-papers/RosoliniG.

3.7 Site management report for Chalmers

3.7.1 People working on the project

• Permanent members of staff : Thierry Coquand and Peter Dybjer have contributed 6 man-months each.

• Contract research workers: The following people have been employed as postdoctoral researchers: Thorsten Altenkirch (11 man-months), Christophe Raffalli (9.5 man-months), and Michael Hedberg (9 months).

• Research students: Catarina Coquand and Daniel Fridlender are research students at Chalmers and have contributed 1 man-month each. Hugo Herbelin was a research student at ENS Lyon and INRIA-Rocquencourt supervised by Thierry Coquand until he graduated in January. He has contributed 2 man-months to the project.

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Thorsten Altenkirch, Christophe Raffalli, Michael Hedberg, Catarina Coquand, and Daniel Fridlender.

These people made contributions to the following Topics in the project Workplan:

Topic C: Altenkirch, C. Coquand, T. Coquand, Dybjer, Hedberg, Raffalli. Topic H: T. Coquand, Fridlender, Herbelin.

3.7.2 Interaction with other sites

Thorsten Altenkirch visited Darmstadt in June and Cambridge in August. Thierry Coquand visited Aarhus in April. Peter Dybjer visited Cambridge and Imperial in January. Peter Dybjer is visiting the Newton Institute in Cambridge July - December. Thierry Coquand will be visiting the Newton Institute in September.

3.7.3 Conferences attended

The following conferences and workshops contained presentations of work done on the project at the Chalmers site: Joint CLICS-TYPES Workshop on Categories and Type Theory, Göteborg, January 1995, the TYPES Workshop, Torino, June 1995, The meeting on Mathematical Logic, Oberwolfach, April 1995, the Minisymposium on Topological Methods in Constructive Model Theory in Uppsala, May 95.the conference on Mathematics of Program Construction, ??, July 1995, the Dagstuhl Seminar on Automation of Proof by Induction, SchloßDagstuhl, July 1995, the conference on Category Theory and Computer Science, Cambridge, August 1995.

3.7.4 Publications

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

[BD95] Ilya Beylin and Peter Dybjer. A short formal proof of coherence for monoidal categories. Draft paper, 1995.

[CD] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science. Accepted for publication. Preliminary version appears in Proceedings of the 1993 TYPES Workshop, Nijmegen.

[Dyb95] Peter Dybjer. Internal type theory. In Proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, Göteborg, January 1995.

3.8 Site management report for TH Darmstadt

3.8.1 People working on the project

• Permanent members of staff : Klaus Keimel: 4 man months.

Thomas Streicher: 5 man months.

Achim Jung: 9 man months.

Michael Huth: 9 man months.

Thomas Streicher has been appointed as a Professor in the Department of Mathematics effective from 1 April 1995.

Achim Jung has accepted a Chair of Computer Science at the University of Birmingham starting 1 October 1995.

Michael Huth is on leave from 1 August 1995 to 31 July 1996 working as a Research Assistant at the University of Birmingham.

• Research students: Hermann Puhlmann, Christine Strüder, Barbara Henhapl, Mathias Kegelmann, Regina Tix, Martin Hofmann, Michael Marz, Alexander Lehmann.

• Topics of research: All have been working on Topic B, Duality in Domain Theory. Achim Jung amd Barbara Henhapl have also worked on Topic A, Sequentiality and Stability. Thomas Streicher has also worked on Topics H.

No labour costs are charged to the project.

3.8.2 Interaction with other sites

Main interactions have been with Imperial and ENS.

The following visitors came to Darmstadt for short visits:

Abbas Edalat (London) Wolfgang Henhapl (Darmstadt) Christoph Thies (Darmstadt) Y. L. Ershov (Novosibirsk) Martin Hofmann (Erlangen/Edinburgh) Jan Paseka (Brno) Martin Hotzel Escardo (London)

3.8.3 Conferences attended

The following conferences and workshops were attended.

Mathematical Structures in Concurrency (MASK), Mannheim, October 1994 (Jung, Keimel). Symposium on Categorical Toplogy, Cape Town, November 1994 (Sünderhauf). Joint CLICS-TYPES workshop, Göteborg, January 1995 (Jung, Streicher). Mathematical Foundations of Programming Semantics XI, New Orleans (USA), March 1995 (Huth, Puhlmann). Full Abstraction for PCF, Aarhus, April 1995 (Jung). Category Theory and Computer Science, Cambridge, August 1995 (Streicher). Conference on Topology and Applications, Portland, August 1995 (Sünderhauf). Semantics and Logics of Computation Summer School, Cambridge, September 1995 (Kegelmann, Marz, Tix).

3.8.4 Publications

The following papers have appeared in print: [FH94, Hut94c, AJ95, Hut94d, Hut95b, JP95, MS95].

The following papers have been accepted for publication: [Hut94a, Hut94e, Sün95c, Sün95a, Sün95b].

Submitted to journals are: [Haa94, Hut94a, HJK94a, SR95] As technical reports have been published: [JP94, KJH94, HM94, Hut95d]. Diploma theses completed: [Str95, Mar95, Hen95, Tix95]. PhD theses completed: [Puh95].

3.8.5 Other activities

The CLICS working group at Darmstadt has organized an international workshop on Logic, Domains, and Programming Languages, which took place from May 24 to May 27, 1995. It was attended by 120 participants from all over the world. Proceedings of the workshop are to be published as a special volume of Mathematical Structures in Computer Science.

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

[FH94] A. Fiech and M. Huth. Algebraic Domains of Natural Tranformations. Theoretical Computer Science, 136(1):57–78, December 1994.

[Haa94] C. Haack. A decomposition theorem for domains. Technische Hochschule Darmstadt. Submitted, 1994.

[Hen95] B. Henhapl. Ein voll abstraktes, extensionales Modell für endliches PCF. Master’s thesis, Technische Hochschule Darmstadt, May 1995. 57pp.

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

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

[Hut94a] M. Huth. Functional Bisimulation. submitted, 1994.

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

[Hut95a] M. Huth. Interaction Orders as Games. In C. Hankin and R. Nagarajan, editors, Theory and Formal Methods 1994, Workshops in Computer Science, pages pp.21–40. Springer Verlag, 1995. to appear.

[Hut95b] M. Huth. Knowledge organization in theories of mind. Knowledge Organization, 1, 1995. To appear.

[Hut95c] M. Huth. A maximal monoidal closed category of distributive algebraic domains. Information and Computation, 116(1):pp.10–25, January 1995.

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

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

[JP94] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. Technical Report 1706, Technische Hochschule Darmstadt, 1994. 23 pp.

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

[KJH94] K. Keimel, A. Jung, and M. Huth, editors. Workshop Domains. Technische Hochschule Darmstadt, 1994. 133 pp.

[Mar95] M. Marz. Monomorphe Typsysteme des λ-Kalküls. Master’s thesis, Technische Hochschule Darmstadt, June 1995. 46pp.

[MS95] M. Marz and P. Selinger. A very well known theorem. Semsoc Newsletter, 4:7–8, 1995.

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

[SR95] Th. Streicher and B. Reus. Continuation semantics : Control operators and abstract machines. Journal of Functional Programming, 1995. (Submitted.).

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

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

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

[Sün95c] Ph. Sünderhauf. Quasi-uniform completeness in terms of Cauchy nets. Acta Mathematica Hungarica, 69(1–2), 1995. To appear.

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

3.9 Site management report for GMD (not available)

3.10 Site management report for Manchester

3.10.1 People working on the project

• Permanent members of staff :

David Rydeheard has contributed about 7 man months, Harold Simmons and Peter Aczel have each contributed about 4 man months.

• PhD Student: Anthony Bailey is working with Peter Aczel on machine checked formalisation of abstract algebra in type theory.

• Visiting research workers and RAs: Amokrankie Saibi was an RA in the Dept for 4 months, May-Aug 1995. He was visiting from INRIA, Paris, where he has implemented a significant body of category theory in the COQ software system. Gilles Barthe was an RA for 1 month in August 1995.

These people made contributions to the following Topics in the project Workplan:

Topic B: Simmons (Analysis of ‘Glueing’) Topic C: Aczel (Generalised set theory, Final Coalgebra Universes) Topic I: Bailey, Aczel (Machine Formalisation of Category Theory and Abstract Algebra)

3.10.2 Interaction with other sites

Manchester has had interaction with other sites as follows.

1. David Rydeheard has been visiting Cambridge (our managing site) for 7 months, partly as a participant in the Newton Institute Programme on Semantics of Computation.

2. Harold Simmons took part in the Newton Institute associated Conference on Category Theory and Computer Science at Cambridge.

3.10.3 Conferences and Seminars attended

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

∗ David Rydeheard: British Colloquium on Theoretical Computer Science, Swansea, April 1995.

∗ Peter Aczel: Joint Types/CLICS Workshop, Gothenborg, Jan 8-10, 1995.

∗ Peter Aczel: Logic of Computation, International Summer School, NATO Advanced Study Institute, Marktoberdorf, July-Aug 1995.

3.10.4 Publications

[Acz94] Peter Aczel. Final universes of processes. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, LNCS Vol 802, pages 1–28, 1994. Edited by S. Brookes, M. Main, A. Melton, M. Mislove, D. Schmidt.

[Acz95] Peter Aczel. Generalised set theory. In Proceedings of the 1994 Conference on Information-oriented appraoches to Logic, Language and Computation, CLSI Lecture Notes, 1995. Edited by Jerry Seligm and Dag Westerstahl.

[Aczar] Peter Aczel. Schematic consequence. In D.M. Gabbay, editor, What is a logical system? Oxford University Press, To appear.

[Fua] YuXi Fu. Categorical properties of logical frameworks. To appear in Mathematical Structures in Computer Science. Available on ftp.cs.man.ac.uk: pub/applied-logic/fuyuxi/CPLF.ps.

[Fub] YuXi Fu. CZF in Martin-Löf’s type theory without identity types. Submitted to Theoretical Computer Science. Available at ftp.cs.man.ac.uk: pub/applied-logic/fuyuxi/CZFs.ps.

[Fuar] YuXi Fu. Recursive models of general inductive types. Studia Logica, To appear. Available on ftp.cs.man.ac.uk: pub/appliedlogic/fuyuxi/rectypes.ps.

[Fups] YuXi Fu. Encodings in polymorphism, revisited. Studia Logica, To appear: Available on ftp.cs.man.ac.uk: pub/appliedlogic/fuyuxi/polymorphism.ps.

[Hil] B.P. Hilken. Towards a proof theory of rewriting: The simply-typed 2lambda calculus. To appear in Mathematical Structures in Computer Science.

[HR] B.P. Hilken and D.E. Rydeheard. A theory of classes: Proofs and models. Submitted to Mathematical Structures in Computer Science. Available on ftp.cs.man.ac.uk: pub/applied-logic/classes.ps.

[Sima] H. Simmons. Axiomatic substitution. Preprint. Available on from the Dept of Computer Science, University of Manchester.

[Simb] H. Simmons. Boolean reflection of frames. Submitted, Available as Preprint.

[Simc] H. Simmons. A density property of the primitive recursive degrees. Submitted to Theoretical Computer Science, 1994.

[Simd] H. Simmons. Ordered structures, topologies and duality. Preprint: Lecture Notes. Available on ftp from pub/applied-logic.

[Sime] H. Simmons. Program extraction by the Leivant method. Preprint. Available on from the Dept of Computer Science, University of Manchester.

[Simf] H. Simmons. Taking the Curry-Howard correspondence seriously. Preprint: Lecture Notes. Available on ftp from ftp.cs.man.ac.uk in pub/applied-logic/logic-and-comp.ps (134 pages).

[Sim94a] H. Simmons. The glueing construction and lax limits. Mathematical Structures in Computer Science, 1994. 40 pages.

[Sim94b] H. Simmons. The monotonous elimination of predicate variables. J of Logic and Computation, 1994. 45 pages.

3.11 Site management report for Sussex

3.11.1 People working on the project

• Permanent members of staff : Edmund Robinson has contributed about three man-months.

• Contract research workers: Andrea Schalk moved from Sussex to Cambridge.

• Research students: Adam Eppendahl has contributed about one man-month.

Of the above man-months of labour, none are charged as labour costs to this project. These people made contributions to the following Topics in the project Workplan:

Topic D: Robinson.

3.11.2 Interaction with other sites

1. 21/1/95 - 17/3/95: visit of Robinson to Aarhus. This visit was supported by BRICS rather than CLICS, but it enabled some work to be done on two problems in the province of CLICS: work with C. Hermida on linking the type structure of logical relations to predicate logic using fibrations, and work on linking the Joyal-Nielsen-Winskel account of bisimulation to accounts using final coalgebras.

2. 9/7/95 - 18/8/95: visit of Robinson to the Newton Institute for Mathematical Sciences in Cambridge.

3. In addition, we have a continuing interaction with the TYPES project, (ES-PRIT BRA ??) through John Power (Edinburgh).

The following short visits were made:

20/3/95: visit of Robinson to Göteborg.

3.11.3 Conferences attended

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

Eleventh Annual Conference on the Mathematical Foundations of Programming Semantics, New Orleans, March-April 1995

3.11.4 Publications

Deliverables Overview

The deliverables for Milestone 3 comprise the following:

1. Reports on each of the Topics A through I compiled by the Topic Leaders. There is a joint report on the topics A and G.

Thus the list of reports and authors is as follows:

Report on Topic A Sequentiality and Stability  Abramsky
and G Applied Linear Logic  Glynn Winskel
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 F Monadic Semantics  Andrew Pitts
Report on Topic H Computational Content of Classical Proofs Thierry Coquand
Report on Topic I Symbolic Computation  Yves Lafont

There was no work directly on topic E, instead there was an integration effort, reported under topic F.

2. A report on the CLICS-TYPES workshop held in Göteborg in January 1995 (see Appendix).

3. A report on the workshop on “Full Abstraction of PCF and Related Languages” held in Aahrus in April 1995 (see Appendix).

Deliverables

5.1 Topics A & G: Sequentiality and Stability, and Applied Linear Logic

As earlier, we group reports on Topics A and G together because of their close interdependence.

5.1.1 Full Abstraction for PCF and related languages

A major workshop on this topic was held at BRICS in Arhus in April 1995. Participants in CLICS II contributed in strength to this very successful event. There were lectures by Abramsky, Jagadeesan, Malacaria, Ong, Ehrhard, Bucciarelli, Winskel and Jung. One valuable outcome of the meeting was a summary of a cluster of decision problems centering around two key questions:

1. Is the fully abstract model for (finitary) PCF effectively presentable?

2. Is definability in finitary PCF for the full monotone hierarchy over the booleans decidable?

(Of these, (1) is implied by (2), but the converse is open.) These questions probably contain the remaining technical content of the “full abstraction problem for PCF”. This material has been written up by Glynn Winskel, and made available by World-Wide Web.

5.1.2 Relation between the fully abstract model and the standard model

In his thesis, Mulmuley studies a logical relation ϕ between the Scott-lattice model and the terms of PCF. Derived from this relation is a preorder on the model as follows:

x < y ⟺ ∀t.yϕt ⇒ xϕt.

He then shows that the equivalence classes corresponding to this preorder contain a maximal element and that the collection of maximal elements is isomorphic to the fully abstract model of PCF (plus a top element). Achim Jung and his student Barbara Henhapel have analyzed this construction in some detail. They have distinguished which parts of Mulmuley’s thesis depend on taking lattices in the model. As it turned out, many of his results hold under very general conditions.

In particular, one gets a very simple proof of Milner’s context lemma this way from the existence of just any denotational model.

The preorder can also be defined for any model and the corresponding quotient will always be isomorphic to the fully abstract model. The crucial point is that application can not be defined on the quotient structure by representatives. This is where the lattices come in; the maximal elements of each class are precisely representatives through which application can be defined.

In the general situation one can define application through a different technique which we borrowed from ‘Formal Concept Analysis’ [Wil82]. In fact, we get two applications. For one of them we can show isomorphism with the fully abstract model. One also sees that for the lattice model the two applications coincide.

The results are presented in Henhapl’s master’s thesis [Hen95].

5.1.3 Game semantics

Progress has been made on a number of fronts.

• Abramsky, Jagadeesan and Malacaria, and Hyland and Ong, have completed major papers giving detailed accounts of their syntax-free constructions of the fully abstract model for PCF based on game semantics. Much of this was presented in depth at the BRICS workshop mentioned above.

• Hyland and Ong have explored the use of the π-calculus to describe strategies in their model; a paper on this appeared in this year’s Functional Languages and Computer Architecture conference [HO95].

• Abramsky and McCusker have given a game semantics for recursive types by showing that the category of games used by Abramsky, Jagadeesan and Malacaria is algebraically compact in the sense of Freyd [AM95b]. Building on this work, they have shown that the canonical solution for the equation

D = (D ⇒ D)_{⊥}

in this category yields a fully abstract model for the lazy λ-calculus. This is the first syntax-free xonstruction of a fully abstract model for a reflexively typed sequential language. This work was presented at LICS ‘95 [AM95a].

• McCusker has developed a version of game semantics synthesizing features of the “Imperial” and “Cambridge” approaches. One main outcome of this work is a full abstraction result for the computational meta-language FPC, which incorporates products, functions, sums, lifting, and recursive types. This is by far the most expressive language for which a result of this kind has been obtained to date. He is writing up this work for his Ph.D. thesis, which will appear next year.

• The notions of rational category and intrinsic preorder, introduced by Abramsky in connection with game semantics, have received considerable axiomatic development by McCusker and Brauner. In particular, the whole theory of minimal invariants for recursive types is lifted to the more general setting of rational categories; and rationality itself is derived from the more primitive concept of a fixpoint object (introduced originally by Crole and Pitts). Also, Pitts’ method for proving computational adequacy using “relational properties of domains”, developed under topic C of CLICS II, has been adapted to this general setting.

• Ong and Ritter have investigated the categorical semantics of Parigot’s λμ-calculus, which provides a computational interpretation of Classical logic. This is basic to making substantive connections between game semantics and Classical logic, which is one of the objectives of CLICS.

• Abramsky, Jagadeesan and Malacaria have developed a game semantics for polymorphism incorporating a notion of relational parametricity. This will be presented by Abramsky at the CLICS summer school in Cambridge in September.

• Abramsky presented a notion of “typed realizability” at the Cambridge Summer Meeting on Category Theory in August. This is intended to serve as a basis for the study of sequential realizability and the resulting higher-order logic and type theory.

5.1.4 Bistructures

Another tack holds promise for producing directly extensional models of PCF, and hopefully of the fully abstract model of PCF. Bistructures are a generalisation of event structures to represent spaces of functions at higher types. Last year, it was shown that bistructures form a categorical model of Girard’s classical linear logic. The comonad of the model has associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry’s bidomains. Moreover, the use of bistructures in modelling PCF, and the theory on PCF terms induced, was studied. This year a broader potential for bistructures has been uncovered. In particular, by incorporating the work of Ehrhard on hypercoherences, they extend to sequentiality. Further joint work between Curien, Plotkin and Winskel is planned to consolidate the various strands of work on bistructures. In particular, Winskel has observed a way to generalise Ehrhard’s hypercoherences [Win], analogous to the generalisation of logical relations to Kripke logical relations, the idea being to map out the range of the various kinds of “consistency relations” to accompany bistructures aiming at narrowing down to the fully abtract model of PCF.

5.1.5 MacLane’s conjecture

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

5.1.6 Concurrency

Several advances have been made in the field of concurrency within the latter project period.

The paper [JNW94] has been accepted for a LICS93 Special issue of Information and Computation. In it an abstract definition of bisimulation is presented. The concept is based on open maps in a topos, as they appear in the work of Joyal and Moerdijk. Nielsen and Winskel have shown that the results also apply to Petri nets, an article accepted for TCS [NW], and significantly that the same bisimulation equivalence is obtained there. Preliminary ideas in [JNW94] has been significantly extended by Cattani and Winskel’s work on presheaf models for concurrency. Presheaves over pomsets for example can be seen as generalisations of event structures (the category of event structures embeds fully and faithfully into presheaves over pomsets). Such presheaf models have several technical advantages over existing models. In particular, they can be made into a bifibration which is useful in the abstract approach initiated by Winskel into weak bisimulation, based on a monad to account for the invisibility of internal actions. More generally, by results dating back to Kan’s work, presheaf models are related by naturally occurring functors which have been shown to preserve open maps by Cattani and Winskel [CW]—a very useful general result. The suspicion that the new presheaf models supported “refinement” operators, has been formally confirmed in the results of Cattani (PhD student of Winskel); for example, the refinement of event structures by finite pomsets (well-known from the work of van Glabeek and others) appears especially simply as the restriction of a general construction on presheaves. This relates to earlier CLICS work of Rosolini et al, where general refinement of event structures is considered.

Engberg and Winskel’s work on linear logic on Petri nets, essentially in [EW95], has been accepted for the Annals of Pure and Applied Logic

5.1.7 Interaction nets

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

5.1.8 Summary

In summary, very striking progress has been made on these topics over the course of the CLICS II project. It seems fair to say that the current state of insight into sequentiality has progressed very considerably from where it stood at the start of CLICS II, and much of this progress has been achieved by participants in CLICS. Of course, much remains to be done, but the lines of enquiry mapped out at the start of the project have for the most part proved very fruitful, and seem likely to continue to do so.

5.1.9 References and selected publications

[AM95a] S. Abramsky and G. McCusker. Games and full abstraction for the lazy λcalculus. In D. Kozen, editor, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 234–243. IEEE Computer Society Press, 1995.

[AM95b] S. Abramsky and G. McCusker. Games for recursive types. In C. Hankin, S. J. Gay, and R. Nagarajan, editors, Theory and Formal Methods ‘94. Imperial College Press, 1995.

[Hen95] B. Henhapl. Ein voll abstraktes, extensionales Modell für endliches PCF. Master’s thesis, Technische Hochschule Darmstadt, May 1995. 57pp.

[HO95] J. M. E. Hyland and C.-H. L. Ong. Pi-calculus, dialogue games and PCF. In Proceedings of 7th Annual ACM Conference on Functional Programming Languages and Computer Architecture, La Jolla, California. ACM, 1995.

[Wil82] Rudolf Wille. Restructuring lattice theory: an approach based on hierarchies of concepts. In Ivan Rival, editor, Ordered sets, pages 445–470, Dordrecht–Boston, 1982. Reidel.

[Braa] T. Braüner. The Girard Translation Extended with Recursion. Full version of paper to appear in Proceedings of CSL ’94, LNCS 933, 1995. (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/13/BRICS-RS-95-13.ps.gz)

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

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

[CN] A. Cheng and M. Nielsen. Open Maps (at) Work. April 1995. (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/23/BRICS-RS-95-23.ps.gz)

[EW95] Uffe H. Engberg and Glynn Winskel. Completeness results for linear logic on Petri nets. Accepted for Annals of Pure and Applied Logic, 1995.

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

[NW] M.Nielsen and G.Winskel. Petri Nets and Bisimulations. January 1995. To appear in TCS. (ftp.daimi.aau.dk) (Available by anon ftp from ftp.daimi.aau.dk at pub/BRICS/RS/95/4/BRICS-RS-95-4.ps.gz)

[Sas1] V. Sassoe. An Axiomatization of the Algebra of Petri Net Concatenable Processes. To appear in Theoretical Computer Science.

[Sas2] V. Sassone. On the Category of Petri Net Computations. In Proceedings of the 6th International Conference on Theory and Practice of Software Development, TAPSOFT ‘95, LNCS n. 915, pp. 334–348, Springer-Verlag, 1995.

[SNW] V. Sassone, M. Nielsen, and G. Winskel. Models for Concurrency: Towards a Classification. To appear in Theoretical Computer Science.

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

[Sol1] S.Soloviev. Reductions in Intuitionistic Linear Logic Accepted for 4-th issue of Math.Structures in Comp. Sci., 1995.

[Win] G.Winskel. Hypercoherences. Manuscript, September 1994.

5.2 Report on topic B: Duality in Domain Theory

5.2.1 Summary

This report describes work done during Year 3 on Topic B (Duality in Domain Theory). This topic contributes to the project objectives in the area of “Domain Theory”. The work done addresses the key issues of “Unification of Formalisms”, “Modularity” and “Simplicity”. Work has taken place on a number of interrelated fronts. Work on extensions of traditional domain theory has been centred on Darmstadt; that on synthetic domain theory involved Cambridge, Genova Sussex and Imperial with additional input from Streicher and Reuss in Munich. Other work related to this topic has involved Aarhus and CAIMENS. The following publications form the deliverables under this Topic: papers appearing in print [FH94, Hut94c, HJK94b, Haa94, KP94, AJ95, Hut94d, Hut95b, JP95, MS95, HM]; accepted for publication: [Hut94a, Hut94e, Sün95c, Sün95a, Sün95b]; submitted to journals[Haa94, Hut94a, HJK94a, SR95]; technical reports [JP94, KJH94, HM94, PW94, Win94, Hut95d]; research notes [Ros95]; Diploma theses [Str95, Mar95, Hen95, Tix95]; PhD theses [Sün94a, Puh95].

The proposed deliverables for milestone 3 were the following extensions and developments of classical domain theory explained in the report at milestone 2: an extension of the maximality results to the bounded complete setting; a treatment of domain theory in logical form for the continuous case; and applications of Stone Duality to static data types, such as the relational database datatype. Work on these three topics (together with some other work in ‘classical’ domain theory pertinent to the aims of the project) is described under the heading traditional domain theory below. (The bulk of the publications are in this area.) We draw attention to the remarkable and challenging developments in the area of Stone Duality for continuous domains.

In addition it was part of our original plan that work should continue on Synthetic Domain Theory (SDT). The impact of ideas from SDT typed metalogics for programming semantics is indicated under Topic F. Here we report on the pure theory alone. the deliverables [Ros95, HM] represent this area. Related work in extensions of domain theory and connections with games is briefly mentioned.

5.2.2 Work completed: traditional domain theory

5.2.2.1 Linear Types

The motivation and background for this work was explained in last year’s report and we only mention two new developments. These are technical in nature, but each of them is deep and asking for more research.

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

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

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

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

5.2.2.2 Stone duality for continuous domains

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

These results confirm in a very convincing fashion our view that by studying the world of continuous domains one can get a deeper insight into the workings of domain theory. Philipp Sünderhauf will present the work at the Conference on Topology and Applications in Portland next week.

By further strengthening the axioms one gets predomains which correspond precisely to FS-domains. The main change is to replace the order of approximation by a stratified set of relations. It confirms the idea that FS-domains allow a quantitative analysis of computation.

5.2.2.3 Stone duality for static datatypes

In our research on a semantics for databases we have followed the idea of modelling set-constructs by the snack-powerdomain as outlined in last year’s progress report. The new result to be reported here is that on this basis one can define so-called nest and unnest operations between different levels of grouping data together. Unlike in any other approach, we get that these two operations are adjoint to each other, thereby clearly exhibiting the precise nature of the information lost by first unnesting and then nesting again. This is contained in Hermann Puhlmann’s doctoral thesis [Puh95].

5.2.2.4 Probabilistic computation

There is a longstanding interest in the probabilistic powerdomain construction of Saheb-Djahromi and others ([SD80, JP89, Jon90]) in Darmstadt. Two master’s theses were written over the last twelve month which are concerned with this. In the first, [Tix95], Regina Tix has generalized many lemmas in the theory to their natural setting. Furthermore, she has demonstrated that an often-cited result about the probablilistic powerdomain is in fact unproven and that the proofs of it in the literature are in fact wrong. In a very detailed study she describes attempts from many different angles and shows why they are insufficient. Whether there exists any cartesian closed category for which the probabilistic powerdomain can be defined, remains an open and important problem.

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

The interest in the probabilistic powerdomain is rising recently because of Abbas Edalat’s results in Dynamical Systems. We have applied for a bilateral ARC project on these connections which involves Darmstadt, Saarbrücken, Leipzig, London, and Birmingham. It has been approved for an initial period of two years.

5.2.3 Work completed: synthetic domain theory and related topics

5.2.3.1 Foundations of SDT

Basic research in this area has been kept kept in the public domain through the SDT email list set up by Paul Taylor. However project members are beginning to make accounts of parts of the theory available in more traditional forms. The impact of the theory is already making itself felt as is indicated by the report under Topic F.

In the first place, Rosolini’s notes on SDT mentioned in the 2nd annual report have been extended in a number of directions. As well as an introduction to the general theory they now contain much new research material. In particular, they make a major contribution to the applicability of SDT in traditional programming semantics by giving a precise analysis of conditions leading to algebraic compactness for categories of algebras. There are also applications of the basic idea of repletion to fundamental results in pure topos theory. The view point of these notes was explained in detail to project members and others during a visit of Rosolini to BRICS in Aarhus.

The S-replete construction was originally introduced by Hyland and Taylor in the setting of a topos E with an object S of computable truth values. In a detailed analysis, [HM] considers the replete construction in the more general setting of a cartesian closed fibration over a base category with finite products, (parameterized w.r.t. an arbitrary object S in some fibre). This encompasses the case of a cartesian closed category fibered over Set (or simply 1) and that of a locally cartesian closed category (quasi-topos or topos) fibred over itself. (The first case is of interest in the context of Classical Domain Theory, while the second one is typical of SDT.) There are important conceptual advantages of working in a fibred setting:

• It provides a general setting which accommodates many examples and so allows comparisons between them.

• It makes clear that additional properties of the construction rarely depend on further assumptions about the base category.

• It enables one to distinguish between the stability needed in a fibre and that which involves reindexing. This clarifies many arguments.

• It avoids appeals to internal category theory, which many find obscure!

The paper identifies simple properties, which ensure that the full sub-fibration of S-replete objects relates nicely to the ambient fibration. On the other hand it does not investigated which properties of S ensure that the replete objects are good for Denotational Semantics, e.g. satisfies the criteria set by Axiomatic Domain Theory. However, part of the general results, namely those about plumb sub-fibrations, should be applicable to other constructions for SDT, such as the well-complete objects studied in Longley’s thesis.

Lack of sufficiently well qualified personnel together with other commitments of project members have led to a relatively slow development of the pure side of SDT during the project. However young researchers (in particular at Edinburgh: Fiore, Longley, Simpson) have been attracted to the subject and to the related topic of axiomatic domain theory. So there are signs that the project is having an impact in this area.

5.2.3.2 Extended notions of domain: connections with game theory

Last year we reported on innovative work by Plotkin and Winskel which extended our understanding of an approach to domains in which both the extensional and a more intensional (computational) order are taken as basic. Work in this area (extensions of the notion of bidomain) has continued, but without as it seems getting close to full abstraction for PCF. Considerable effort is now going into understanding the connection between the extended notions of domain and ideas of intensional semantics arising from work on the game models [AJM, HO] reported elsewhere. Project members were much in evidence at the Workshop on ‘Full Abstraction for PCF and Related Languages’ held at BRICS, Aarhus in April 1995. They gave substantial accounts of aspects of strong stability (Ehrhard, Bucciarelli) including a new method (Bucciarelli) for relating equational theories arising from the models, and also of game semantics (Abramsky, Jagadeesan, Malacaria, Ong). Work is also in progress on a variety of abstract notions of domain/game; most recently de Paiva and Schalk in Cambridge have produced elegent new categories by abstracting from ideas of Lamarche (cf [Lam94]). But as yet the wealth of possibilities seems bewildering.

5.2.4 References and selected publications

[AJ94] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 1994. To appear.

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

[AJM] S. Abramsky, R. Jagadeesan, and P. Malacaria. Games and full abstraction for PCF, preliminary draft.

[GHK80] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer Verlag, 1980.

[Gir87] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[FH94] A. Fiech and M. Huth. Algebraic Domains of Natural Tranformations. Theoretical Computer Science, 136(1):57–78, December 1994.

[Haa94] C. Haack. A decomposition theorem for domains. Technische Hochschule Darmstadt. Submitted, 1994.

[Hen95] B. Henhapl. Ein voll abstraktes, extensionales Modell für endliches PCF. Master’s thesis, Technische Hochschule Darmstadt, May 1995. 57pp.

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

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

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

[Hut94a] M. Huth. Interaction Orders as Games. In C. Hankin and R. Nagarajan, editors, Theory and Formal Methods 1994, Workshops in Computing. Springer Verlag, 1994. to appear.

[Hut94b] M. Huth. Interaction Orders as Games. Technical Report 1639, Technische Hochschule Darmstadt, 1994.

[Hut94a] M. Huth. Functional Bisimulation. submitted, 1994.

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

[Hut94d] M. Huth. A maximal monoidal closed category of distributive algebraic domains. Information and Computation, 1994. To appear.

[Hut94e] M. Huth. Zero Dimensional and Connected Domains. Semigroup Forum, 1994. to appear.

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

[Hut95b] M. Huth. Knowledge organization in theories of mind. Knowledge Organization, 1, 1995. To appear.

[HM] J. M. E. Hyland and E. Moggi. The S-replete construction. In , editors, CTCS 1995, volume ? of Lecture Notes in Computer Science, pages ?, 1995.

[HO] J. M. E. Hyland and L. Ong. On full abstraction for PCF: I, II and III. preliminary draft.

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

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

[JP94] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. Technical Report 1706, Technische Hochschule Darmstadt, 1994. 23 pp.

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

S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 235–258. Springer Verlag, 1992.

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

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

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

[KJH94] K. Keimel, A. Jung, and M. Huth, editors. Workshop Domains. Technische Hochschule Darmstadt, 1994. 133 pp.

[KP94] K. Keimel and J. Paseka. A direct proof of the Hofmann-Mislove theorem. Proceedings of the AMS, 120:301–303, 1994.

[Lam94] F. Lamarche. Dialectics: a model of linear logic and pcf.

[Mar95] M. Marz. Monomorphe Typsysteme des λ-Kalküls. Master’s thesis, Technische Hochschule Darmstadt, June 1995. 46pp.

[MS95] M. Marz and P. Selinger. A very well known theorem. Semsoc Newsletter, 4:7–8, 1995.

[PW94] G. Plotkin and G. Winskel. Bistructures, Bidomains and Linear Logic. BRICS Report Series RS-94-9, 1994.

[Puh93] H. Puhlmann. The snack powerdomain for database semantics. In A. M. Borzyszkowski and S. Sokołowski, editors, Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 650–659, 1993.

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

[Ros95] G. Rosolini. Notes on Synthetic Domain Theory. Genova, 1995.

[SD80] N. Saheb-Djahromi. CPO’s of measures for nondeterminism. Theoretical Computer Science, 12:19–37, 1980.

[SR95] Th. Streicher and B. Reus. Continuation semantics : Control operators and abstract machines. Journal of Functional Programming, 1995. (Submitted.).

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

[Sün93] Ph. Sünderhauf. The Smyth-completion of a quasi-uniform space. In M. Droste and Y. Gurevich, editors, Semantics of Programming Languages and Model Theory, volume 5 of Algebra, Logic and Applications, pages 189– 212. Gordon and Breach Science Publ., 1993.

[Sün94a] Ph. Sünderhauf. Discrete Approximation of Spaces. PhD thesis, Technische Hochschule Darmstadt, 1994. 91 pp.

[Sün94b] Ph. Sünderhauf. A faithful computational model of the real numbers. Technical Report 1610, Technische Hochschule Darmstadt, 1994. 17 pp.

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

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

[Sün95c] Ph. Sünderhauf. Quasi-uniform completeness in terms of Cauchy nets. Acta Mathematica Hungarica, 69(1–2), 1995. To appear.

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

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

[Win94] G. Winskel. Stable Bistructure Models of PCF. BRICS Report Series RS-94-13, 1994.

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

5.3.1 Summary

This report describes work done during Year 3 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”. It involves contributions from Cambridge, Chalmers, and Darmstadt.

The deliverables planned for milestone 3 were (i) categorical modeling of type theory; (ii) applications of simultaneous induction-recursion to internal model constructions and reduction-free normalization proofs.

The publications which form the deliverables under this Topic are items [AHS95, CD, BD95, Dyb95, Gor95].

(i) We have developed a new notion of model for dependent types: category with families [Dyb95] which is closer to syntax than previously proposed notions, and yet a perfectly good categorical notion which directly gives rise to an elegant set of categorical combinator.

We have also proposed a new category-theoretic semantics of inductively defined universes in terms of initial algebras in a slice category (unpublished work by Thomas Streicher). Let C be a model of a basic logical framework of dependent types with El → Set a generic family of sets. A predicative universe can be understood as the initial algebra for a certain endofunctor on the full subcategory of C/Set whose objects are those i : A → Set for which A is a small set, that is, A → 1 is a pullback of El → Set along some a : 1 → Set.

(ii) We have also shown how to represent categories with families inside intuitionistic type theory giving rise to what we call “internal type theories” [Dyb95]. The notion of an internal type theory has a coherence problem which we solve by reduction-free normalization using a model of normal forms defined by a simultaneous inductive-recursive definition.

In addition to these planned deliverables there has been progress in several other areas. These are reported below.

5.3.2 Work completed

In the workplan we predicted that work on Topic C would stop at the end of Year 2. This has not been the case however, but the goals related to this topic have evolved and we shall therefore restructure the contributions.

Previous progress reports on Topic C were divided into the following three areas:

• logic of well-founded datatypes;

• logic of non well-founded datatypes;

• logic of recursive types in functional languages.

The study of the logic of well-founded datatypes has concentrated on the structure of inductive definitions in Martin-Löf’s intuitionistic type theory. In particular we have focussed on the application of simultaneous inductive-recursive definitions to the internalization of the metatheory of type theory in itself (see the description of the deliverables).

There was a proposal for a general formulation of inductive and inductiverecursive definitions in Dybjer [Dyb94]. An alternative to this formulation has recently been proposed by Altenkirch and Coquand. This formulation also incorporates in a uniform way a version of Coquand’s pattern-matching [Coq92].

Questions about the internalization of the metatheory of type theory focussed in particular on the internalization of normalization proofs. For this reason T. Coquand and Dybjer [CD] took up the study of “reduction-free” normalization proposed in early work by Martin-Löf [ML75] (and rediscovered in different guises by Berger and Schwichtenberg [BS91] and by Lafont [Laf88]). This direction has proved to be an interesting field of study in its own right.

Recently, Altenkirch, Steicher, and Hofmann made a categorical reconstruction of C. Coquand’s [Coq93] Kripke-model based reduction-free normalization of the simply typed λ-calculus (also related to Berger and Schwichtenberg [BS91]. They also showed how this construction is related to categorical glueing (something which was only hinted at in [CD]) by introducing a notion of twisted glueing related to Kripke logical predicates. Further work is in progress on extending this construction to the case of λ-calculus with coproducts. Sheaf models, which can be viewed as a proof relevant generalisations of Beth models, are relevant here. However, it is still not clear how to derive a decision procedure for full strong coproducts. The problems and partial results have been presented by Martin Hofmann at the Workshop on Logic, Domains and Programming Languages in Darmstadt, June 95.

Another application of reduction-free normalization is a new syntactic proof of coherence for monoidal categories by Beylin and Dybjer [BD95]. An interesting feature of this proof is that it is obtained almost without extra work from a reduction-free normalization proof for free monoids.

Coherence problems seem to be of general interest for intensional intuitionistic type theory. As mentioned above the notion of an internal type theory gives for example rise to a coherence problem. Hofmann and Streicher’s [HS94] striking result of the existence of “non-coherent” models (where there is more than one element of the equality set) aroused a lot of interest. However, as shown by Hedberg, such coherence hold if we restrict ourselves to decidable intensional equality.

Much of this work relies on the internalization of various categorical structures inside intuitionistic type theory. A natural question to ask here is whether it is feasible to develop a substantial fragment of (constructive) category theory inside this framework in general – and also implement it using a proof assistant for type theory. There has been several developments towards this goal both within CLICS and within TYPES. For example, Beylin and Dybjer [BD95] implemented their coherence proof for monoidal categories in the proof assistant Alf, and showed that this implementation gives rise to a “metacoherence problem”: to prove coherence of monoidal categories we have to use a coherence proof for equality in the metalanguage of intuitionistic type theory.

Coinduction has been a central theme in our studies of the logic of non wellfounded datatypes and of recursive types in functional languages. Recent work has focussed on applications of various forms of coinduction.

For example A. Gordon [Gor95] established equational laws for FPC (PCF plus sums, products and recursive types). This is a deterministic functional language for which Morris-style contextual equivalence—invariance of termination under any context of ground type—is the usual notion of operational equivalence. Contextual equivalence is hard to establish directly. Instead he defined a labelled transition system for call-by-name FPC (and variants) and proved that CCS-style bisimilarity equals contextual equivalence—a form of operational extensionality. By considering variations of Milner’s ‘bisimulations up to ∼’ he obtained a second co-inductive characterisation of contextual equivalence in terms of reduction behaviour and production of values. Furthermore, co-inductive proofs were used to establish contextual equivalence in a series of stream-processing examples. Finally, he considered a form of Milner’s original context lemma for FPC, but concluded that his form of bisimilarity supported simpler co-inductive proofs.

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

[BD95] Ilya Beylin and Peter Dybjer. A short formal proof of coherence for monoidal categories. Draft paper, 1995.

[BS91] Ulrich Berger and Helmut Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 203–211, July 1991.

[CD] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science. Accepted for publication. Preliminary version appears in Proceedings of the 1993 TYPES Workshop, Nijmegen.

[Coq92] Thierry Coquand. Pattern matching with dependent types. In Proceedings of The 1992 Workshop on Types for Proofs and Programs, June 1992.

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

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

[Dyb95] Peter Dybjer. Internal type theory. In Proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, Göteborg, January 1995.

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

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

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

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

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

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

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

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

5.4.1 References and selected publications

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

5.5 Report on topic F: monadic programming language semantics

5.5.1 Summary

This report describes work done during Year 3 on Topic F (monadic programming language semantics). This topics contributes to the project objectives in the areas of “Semantics and Logics of Programming Languages” and “Domain Theory”. The work done addresses the key issue of “Unification of Formalisms”. It has involved the collaboration of Moggi in Genova, and Pitts and some of his research associates and students in Cambridge.

The results reported here were presented at the following international conferences and workshops: Advanced School on Typed Lambda Calculus and Functional Programming (Udine, September 1994); Second International Conference on Typed Lambda Calculus and Applications (Edinburgh, April 1995); BRICS Workshop on Full Abstraction (Aarhus, April 1995); Summer School on Semantics and Logics of Computation (Cambridge UK, September 1995).

The publications which form the deliverables under this Topic are items [Mogar], [Mog95], [Pit99], [RP95], and [Sta95a].

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

5.5.2 Work completed

5.5.2.1 Metalanguages and Applications

[Mogar] considers typed metalanguages of increasing complexity, ranging from a naive one (with a set-theoretic semantics) to one incorporating ideas from Synthetic and Axiomatic Domain Theory. which corresponds to a first proposal for LCF++.

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

The approach adopted differs from advanced textbooks on denotational semantics in three aspects:

• it makes significant use of type theory as a tool for describing languages and calculi, while this is usually done via a set of formation or inference rules; • it incorporates ideas from Axiomatic and Synthetic Domain Theory into met-

alanguages, while most metalanguages for denotational semantics are minor variants of LCF;

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

5.5.2.2 Semantics of dynamically allocated local state

Work has continued on applying techniques developed earlier in the project to study properties of dynamically allocated local state in higher order languages.

A Fully Abstract Translation between a λ-Calculus with Reference Types and Standard ML. Ritter and Pitts [RP95] consider a translation into a suitable typed lambda calculus of a substantial fragment of the core Standard ML language containing recursively defined datatypes and imperative features in the form of reference types. The translation compiles SML’s use of declarations and pattern matching into lambda terms, and transforms the use of environments in the operational semantics into a simpler relation of evaluation to canonical form. The main result is that this translation is ‘fully abstract’, in the sense that it both preserves and reflects contextual equivalence. The motivation for establishing such a result stems from ongoing work on logics for verifying properties of SML programs (in particular, equivalence of programs). It is more convenient to develop such logics on top of a suitable typed lambda calculus rather than the programming language itself. However, one then needs results such as the one established in loc. cit. to relate equivalence of SML programs to equivalence of the corresponding lambda calculus expressions. Preservation and reflection of contextual equivalence along the translation is certainly to be expected, since apart from the use of patterns and environments, the two languages are quite similar. However the proof of this property is not straightforward, because it is hard to reason directly about contextual equivalence for programming languages such as SML which involve dynamic creation of local storage for higher order functions. Instead Ritter and Pitts make use of a notion of applicative bisimilarity for functional languages with state which was developed earlier in the project.

Names and higher-order functions Pitts’ student Stark completed, and successfully defended, his PhD thesis on names and higher-order functions [Sta95a]. Most of his results on operational and monad-based denotational semantics of higher order functions involving dynamically generated names have been described in previous reports.

5.5.2.3 Monadic semantics of CCS-like languages

In some joint work with D. Sangiorgi (Sophia-Antipolis) and M.Fiore (Edinburgh), which is not yet completed, Moggi has investigated the denotational semantics of CCS-like calculi, including Milner’s π-calculus (see [Mog95]). (Related work has been carried out by Stark [Sta95b] since he left the project to take up an HCMP Fellowship in Pisa, and by G. Meredith at Imperial.) The main technical result is a fully-abstract model, in the functor category Cpo^{I}, for π-calculus agents (with a minor variant for replication) up to strong late bisimulation.

An important methodological aspect of this work is that the technical tools needed had already been introduced independently from the π-calculus:

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

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

5.5.3 References and selected publications

[Mog95] E. Moggi. Monadic semantics of CCS-like calculi. presented at the MASK workshop, Alghero, Italy, May 1995, 1995.

[Mogar] E. Moggi. Metalanguages and applications. In ??, volume ?? of CISM Lecture Notes. Springer Verlag, to appear. Revised and expanded version of lectures given at the Advanced School on Typed Lambda Calculus and Functional Programming (Udine, September 1994).

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

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

[Sta95a] I. D. B. Stark. Names and higher-order functions. Technical Report 363, Cambridge Univ. Computer Laboratory, April 1995.

[Sta95b] I. D. B. Stark. Outline of a denotational semantics for the π-calculus. unpublished note, June 1995.

5.6 Report on topic H: Computational Content of Classical Logic

5.6.1 Summary

This report describes work done during Year 3 on Topic H. This topic contributes to the project objectives in the areas of “Type Theory” and “Semantics and Logics of Programming Languages”. It involves contributions from Chalmers.

We have formulated a general way of extracting computational content of some classical proofs using the axiom of choice. This uses topological model. We interpret the proof effectively in an effectively built topological model. If the statement proved is existential, it is then possible to extract effectively a witness.

5.6.2 Work completed

Thierry Coquand has systematised his previous work of applying point-free topology, or constructive local theory, to the extraction of computational content of classical proof. The method can now be described as follows.

If an argument uses a non effective object, like a non principal ultrafilter, or a prime ideal, whose existence is only ensured by an indirect argument, one can often interpret the existence of this object in a relativised sense, namely in the sense of a topological model over a formal space.

Furthermore, if this formal space satisfies the condition that any covering of the whole space is inhabited, then it is the fact that an existential statement is valid in a relativised sense transfers to the ”absolute” validity of the statement. For having transfer for a purely universal statement, it is enough that the space is not covered by the empty set (which is intuitionistically weaker).

This method has been applied to make constructive sense of some uses of non principal ultrafilter over natural numbers, leading to a purely intuitionistic proof of the closed open Ramsey’s theorem, and of the existence of minimal closed invariant subspaces of a boolean space with a continuous endomap. What is “extracted” in this case is a simple algebraic lemma on boolean algebra. This improves on the previous work on extracting computation content of van der Waerden’s theorem.

This work has been presented in a seminar in P. Martin-Löf’s logic seminar in Stockholm, October 1994, in th Minisymposium on Topological Methods in Constructive Model Theory in Uppsala, April 1995, and in the meeting on Mathematical Logic, Oberwolfach, April 1995.

Sara Negri, from Padova, has been visiting our department. A joint work with Thierry Coquand produced a new constructive argument for the localic version of Hahn-Banach’s theorem, whose statement (and indirect proof) is due to Ch. Mulvey. A previous constructive proof of this theorem can be found in J. Vermeulen’s Ph.D. thesis, Susseix 1986, but the new argument may have the advantage of being closer to the usual Helly’s proof of this theorem.

Hugo Herbelin, supervised by Thierry Coquand has defended his thesis in january 95, at the University Paris VII, with the mention très honorable. He presented a clear connection between sequent calculus and lambda-calculus on one hand, and a precise connection between cut-elimination in sequent calculus, and the game interpretation proposed by Coquand of Novikov’s calculus.

Some suggestions of how to use this work in connection with the presentation of a fully abstract model for PCF have been presented by P.L. Curien in the meeting on Full Abstraction, Aarhus, March 1995, and it is to be hoped that this direction will be analysed by Hugo Herbelin.

5.6.3 References and selected publications

• Th. Coquand “A Formal Space of Ultrafilters”, draft paper

• Th. Coquand “Minimal Invariant Spaces in Formal Topology”, draft paper • S. Berardi, M. Bezem and Th. Coquand “Computational Content of the

Axiom of Choice”, presented at TLCA 95, Edinburgh

• Th. Coquand “A Semantics of Evidence for Classical Arithmetic,” JSL, 1995 • H. Herbelin “Interpretations algorithmiques du Calcul des Séquents”, Ph. D.

thesis, Paris VII, January 1995.

5.7 Report on topic I: Symbolic Computation

5.7.1 Summary

This report describes work done on Topic I (symbolic computation). This topic has been mainly developed in Marseilles, by Yves Lafont and his student Anne Massol. The publications corresponding to this topic are [1], [2], and [3]. The main deliverable is a software written in CAML, by Anne Massol.

5.7.2 Work completed

Yves Lafont has started a new direction of research inspired by the work of Albert Burroni. Instead of making symbolic computation with terms, one uses planar diagrams (Penrose diagrams) which are more general and allow to decompose the operations of substitution into more primitive ones. With this new syntax, it is still possible to work with terms, but also with various objects occurring in topology (knots), theoretical physics (quantum groups) and computer science (digital circuits). Anne Massol has designed a software for manipulating these diagrams. With this software, it is possible to edit a diagram or an equation between diagrams. It is also possible to perform equational reasoning according to a given set of equations. The interface is purely graphical.

The theory of diagram rewriting is still rudimentary [1]. Anne Massol is now working on the following topic: given a 2-dimensional equational theory, for instance the presentation of the category of finite maps [2], prove that no equation is superfluous. In order to do this, she has to write efficient programs for the automatic search of certain finite model of the equational theory, except one equation. Among the 7 equations for the category of finite maps, we have proved that 5 at least are necessary.

Another related topic has been considered by Yves Lafont in [3]: the use of geometrical invariants to prove that certain equational theories do not have a complete rewriting system.

5.7.3 Future plans

A general theory of rewriting for Penrose diagrams must be developed. One should experiment the software developed by Anne Massol in one of its fields of application.

5.7.4 References and selected publications

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

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

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

Appendix A

A.1 Joint CLICS-TYPES workshop

We organized a joint workshop together with the ESPRIT Basic Research Action TYPES (for Proofs and Programs) in Göteborg, January 8-10, 1995. The purpose of this workshop was to discuss topics of interest to both actions.

One of the themes of the workshop was the use of categories as a tool for furthering the understanding of the syntax and semantics of the type theories underlying the proof assistants Coq, Lego, and Alf developed by the TYPES project. There were presentations of categorical normalization proofs, categorical aspects of proof search, and proof principles for coinductive definitions among other things.

Another theme was the use of type theory as a general logic which can be used for facilitating the implementation of various logical systems developed within the CLICS project, such as a logic based on synthetic domain theory and evaluation logic.

A third theme was the formalization of category theory using type theory based proof assistants. The discussion here focussed on the role of object equality and the relevance of coherence problems.

The workshop was attended by 55 participants from both actions.

Joint CLICS-TYPES Workshop on Categories and Type Theory
January 8 - 10, 1995
Programme
SUNDAY 8 JANUARY
IMPLEMENTING CATEGORY THEORY IN TYPE THEORY
 9.30 - 10.10 Saibi: Constructive category theory in Coq
CATEGORICAL NORMALIZATION PROOFS
10.10 - 10.50 Berger: Positive inductive definitions
11.30 - 12.10 Altenkirch, Streicher: Categorical reconstruction of
a "reduction-free" normalization proof
COHERENCE, OBJECT/TYPE EQUALITY
14.00 - 14.50 Soloviev: Logical systems and coherence: a survey
14.50 - 15.30 Preller: A constructive axiomatization of equality
of objects in lcccs
16.10 - 16.50 Dybjer: On the syntax of dependent types and
the coherence problem
16.50 - 17.30 Discussion on implementing category theory in

type theory, coherence, type/object equality
(introductions by Huet and Altenkirch)
MONDAY 9 JANUARY
FIBRATIONS
9.00 -  9.50 Jacobs: Introduction to fibred categories
in logic and type theory
9.50 - 10.30 Hermida: Fibrations, induction, and coinduction
11.10 - 11.50 van Oosten: Quotient type theories
EVALUATION LOGIC
11.50 - 12.10 Cenciarelli: Partial correctness in evaluation Logic
12.10 - 12.30 Aczel: Compositum algebras for the untyped lambda calculus
CATEGORICAL ASPECTS OF PROOF SEARCH
14.00 - 14.20 Pym: Introduction into proof search
14.20 - 14.40 Ritter: A calculus for linear sequent derivations
14.40 - 15.00 Pym: Kripke models for lambda Pi
15.00 - 15.10 Smith: First order proof search for fragments of type theory
15.10 - 15.30 Discussion
MODULES IN TYPE THEORY
16.10 - 16.50 Salvesen: Classes in ALF
16.50 - 17.30 Discussion on the relevance of category theory for
modularization in type  theory and for the formalization
of abstract algebra (introductions by Aczel and Moggi)
TUESDAY 10 JANUARY
LCF++, DOMAINS
 9.00 -  9.50 Moggi: A proposal for LCF++
 9.50 - 10.30 Reus, Streicher: Axiomatizing synthetic domain theory in LEGO
11.10 - 11.50 Palmgren, Stoltenberg-Hansen: Logically presented domains
CATEGORICAL ASPECTS OF PROGRAMMING LANGUAGES
11.50 - 12.15 Hasegawa: Decomposing typed lambda calculus into
a couple of categorical programming languages
12.15 - 12.30 Jacobs: Coalgebras for the semantics of classes
in object oriented programming
EXTENSIONALITY AND QUOTIENTS IN TYPE THEORY
14.00 - 14.40 Hofmann: Conservativity of equality reflection in
Martin-Loef's type theory
14.40 - 15.30 Discussion (introduction by Coquand)
END OF WORKSHOP

A.2 Workshop on Full Abstraction of PCF and Related Languages

As part of this year’s BRICS theme in “Logic and Semantics”, Glynn Winskel hosted a two week workshop on “Full Abstraction of PCF and Related Languages” from 18 to 28 April, 1995. This focussed attention on recent developments in the semantics of functional languages, in particular, exploring in depth such topics as: game semantics and intensional full abstraction, new work on sequentiality, in particular, strong stability, the use of logical relations in reasoning and refining models, as well as related problems to do with local state. The workshop succeeded in attracting most of the experts in the area, participants including: Abramsky, Bucciarelli, Curien, Coquand, Ehrhard, Gandy, Geva, Jagadeesan, Jung, Malacaria, Nickau, O’Hearn, Ong, Pani, Pitts, Riecke, Sazonov, Sieber, Stoughton. Based on the workshop, a collection of open problems is being assembled, along with a BRICS WWW page collecting the relevant literature.

(http://www.brics.aau.dk/BRICS/FA/)

The workshop began with a broad discussion on the nature of models for PCF (Stoughton) which was followed by a fairly intensive two days on logical relations both for building and reasoning about the fully abstract model of PCF (Riecke, Sieber, Jung and Stoughton), as well as issues related to sequentiality in programming languages with local state (O’Hearn, Pitts). Sequential algorithms as well as their relations with the recent game semantics of PCF and Herbelin’s work were discussed in the two broad sweeping talks of Curien. Interesting examples and problems, as well as historical insight were provided by work on the lines of traditional higher type recursion theory (Gandy, Pani, Nickau, Sazonov). The more leisurely style of the workshop gave room for fairly complete expositions, amounting to minicourses, on game semantics (Abramsky, Jagadeesan, Malacaria, Ong) and strong stability (Ehrhard, Bucciarelli)–the latter included a new method (Bucciarelli) for relating the equational theories arising from models—and time for a recapitulation on the open problems brought to light during the workshop.

Full Abstraction of PCF and Related Languages
April 18-28, 1995
Preliminary Programme
Tuesday, April 18, Auditorium D4
09.15 Introduction, Glynn Winskel
 Allen Stoughton
 Theme: Logical Relations
 Peter O'Hearn & Jon Riecke
13.00 Lunch
14.15 Achim Jung
Wednesday, April 19, Auditorium D4
09.15 Theme: Logical Relations (cont.)
 Kurt Sieber
 Peter O'Hearn
 Andy Pitts
13.00 Lunch
14.15 Allen Stoughton

Thursday, April 20, Auditorium E
09.15 Theme: Sequential Algorithms
 Pierre-Louis Curien
 Robin Gandy (1)
13.00 Lunch
Friday, April 21, Auditorium D4
09.15 Theme: Games
 Rahda Jagadeesan
 C.H. Luke Ong
 Thomas Ehrhard (1)
13.00 Lunch
Saturday, April 22, Auditorium D4
10.15 Thomas Ehrhard (2)
 Antonio Bucciarelli
Monday, April 24, Auditorium D1
09.15 Robin Gandy (2)
 Thomas Ehrhard (3)
 Hanno Nickau
13.00 Lunch
Tuesday, April 25, Auditorium D4
09.15 Pasquale Malacaria (1)
 Samson Abramsky
13.00 Lunch
Wednesday, April 26, Auditorium F
09.15 Vladimir Sazonov
 Pierre-Louis Curien
13.00 Lunch
Thursday, April 27, Auditorium E
09.15 Glynn Winskel
 Shai Geva
13.00 Lunch
Friday, April 28, Auditorium D4
10.15 Open problems
13.00 Lunch

A.3 Semantics of Computation

A 6-month research programme (July to December 1995) at the Isaac Newton Institute for Mathematical Sciences, University of Cambridge, UK.

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge).

Theme of the Programme

The general aims of the programme are twofold. First, to refine the current framework for the semantics of computation so that it is capable of dealing with the more subtle computational features present in the programming languages of today and tomorrow. Secondly, to provide a framework for interaction between such fundamental research and the issues confronted by language designers and software engineers. We particularly have in mind current developments such as object-based concurrent programming, and projects to develop the next generation of advanced programming languages, such as ML 2000. The range of technical and conceptual challenges involved in this work requires active collaboration and flow of information between overlapping communities of mathematicians, computer scientists and computer practitioners. Our main objective for the programme is to provide an ideal, focussed setting for intensifying this interaction.

Programme of Events

The following meetings are being organised in connection with the programme.

Jul 10-12: Semantics for System Design(SSD). The object of this short workshop is to stimulate discussion of the top-down approach to semantics for system design. The format will be highly informal. The idea is to stimulate more intimate discussions between those experienced in a variety of semantic approaches. For this reason, the emphasis will be on challenges, open questions, and work in progress, rather than background, results or conclusions. The following people have agreed to give talks so far: H Jifeng, P Gardiner, CAR Hoare, C Martin, O de Moor. For further details contact Tony Hoare (email via: Jane.Ellory@comlab.oxford.ac.uk).

Jul 17-21: Themes in the Semantics of Computation (TSC). This workshop is intended to open up some of the themes to be pursued during the Semantics of Computation research programme, with some emphasis on the interplay between theory and practice. Apart from the invited talks and accompanying sessions, there will also be scope for contributed talks. Invited speakers will include: CAR Hoare, C Jones, G Kahn, R Milner, JC Reynolds, and A Yonezawa. For further details contact Samson Abramsky (email: sa@doc.ic.ac.uk).

Aug 14-18: Advances in Type Systems for Computing (ATSC). A Euroconference focussing on three related areas of concern to the programme, namely extensions of the ML type system, types in object-oriented programming and type theories for reactive systems. Invited speakers will include: M Abadi, K Bruce, L Cardelli, R Harper, D MacQueen, X Leroy, J Palsberg, B Pierce, V Saraswat, S Smith, M Tofte, A Yonezawa.

Sep 25-29: Summer School on Semantics and Logics of Computation (SLC) in collaboration with the CEC ESPRIT project Categorical Logic in Computer Science (CLICS-II). Lecturers: S Abramsky, T Coquand, M Hofmann, M Hyland, E Moggi, M Neilsen, A Pitts, G Winskel. Organisers: A Pitts (for the programme) and P Dybjer (for CLICS-II). For further details contact Andrew Pitts (email: ap@cl.cam.ac.uk).

Oct 2-4: High-level Concurrent Languages: Foundations and Verification Techniques (HLCL). The object of this short workshop is to bring together programming language designers and concurrency theorists to share both ideas and problems, focussing on what can be achieved with present-day tools and techniques and on the search for new foundations. For further details contact either Benjamin Pierce (email: benjamin.pierce@cl.cam.ac.uk) or Matthew Hennessy (email: matthewh@cogs.sussex.ac.uk).

Oct 16-18: Linear Logic and Applications (LLA). This short workshop will focus on recent developments in Linear Logic and its applications to computer science. For further details contact Gavin Bierman (email: gmb@cl.cam.ac.uk).

Oct 28-31: Higher Order Operational Techniques for Semantics (HOOTS). This short workshop will focus on current developments in operational techniques for the semantics of higher-order languages. This includes (but is not limited to): operational techniques such as verification of type-systems; proofs of program properties using observational or contextual equivalence, (applicative) bisimulation, and Hennessy-Milner logics. For further details contact Andrew Gordon (email: adg@cl.cam.ac.uk).

Further Events

Apart from the focussed events mentioned above, we expect to hold a regular seminar series, open to all who are interested. Details of topics and speakers will be announced nearer the time. We plan to hold workshops on the following topics, further details of which will be announced in the future.

• Nov 6-10: Research Workshop on Games, Processes and Logic. Organiser: Samson Abramsky (email: sa@doc.ic.ac.uk).

• Nov or Dec: One week workshop on New Connections between Mathematics and Computer Science, in collaboration with Hewlett-Packard’s Basic Research Institute in the Mathematical Sciences and the sister research programme ”From Finite to Infinite Dimensional Dynamical Systems”. Organiser: Jeremy Gunawardena (email: jhcg@hplb.hpl.hp.com).

The following conferences will take place as a joint meeting at the Newton Institute. We anticipate that this event will be attended by some of the participants in our programme:

• Aug 6-12: 6th biennial conference on Category Theory and Computer Science (CTCS) and a Summer Meeting on Category Theory.

APPENDIX A. 52

Participants

Abadi, M  9 Aug–6 Sep
Abramsky, S  organiser
Benton, PN  local participant
Bierman, GM  local participant
Brookes, S  6 Jul–30 Sep
Bruce, K  1 Aug–31 Oct
Cardelli, L  6 Aug–8 Sep
Compagnoni, A local participant
Coquand, T  1 Sep–31 Oct
Dybjer, P  25 Sep–15 Dec
Forster, T  local participant
Freyd, PJ  6 Jul–15 Dec
Gardner, P  1 Nov–15 Dec
Gordon, AD  local participant
Gordon, MJC  local participant
Gunter, C  10 Aug–31 Dec
Harper, R  1 Sep–30 Nov
Hennessy, M  28 Aug–6 Oct
Hilken, B  local participant
Hoare, CAR  6 Jul–22 Jul
Huet, G  1 Sep–30 Sep
Hyland, JME  local participant
Jagadeesan, R 6 Jul–31 Jul
Johnstone, PT local participant
Jones, CB  6 Jul–15 Dec
Jung, A  1 Oct–15 Dec
Kahn, G  organiser
Lincoln, P  9 Aug–31 Oct
Lipton, J  1 Aug–10 Sep
Longo, G  3 Sep–9 Sep
Macqueen, DB 14 Aug–13 Nov
Milner, R  local participant

Mitchell, JC  organiser
Moggi, E  6 Jul–30 Sep
Montanari, U  20 Jul–20 Aug
Mycroft, A  local participant
O’Hearn, P  1 Oct–15 Dec
Ong, C-HL  1 Aug–30 Sep
Paiva, VCVde local participant
Paulson, LC  local participant
Pierce, B  local participant
Pitts, AM  organiser
Power, AJ  1 Nov–30 Nov
Rees, G  local participant
Reynolds, JC  6 Jul–31 Aug
Riecke, J  1 Oct–15 Dec
Robinson, EP 5 Jul–31 Jul
Rosolini, G  local participant
Rydeheard, DE local participant
Sangiorgi, D  1 Oct–15 Dec
Saraswat, V  6 Jul–31 Aug
Sassone, V  1 Nov–30 Nov
Scedrov, A  5 Aug–10 Nov
Schalk, A  local participant
Scott, DS  15 Jul–15 Oct
Scott PJ  1 Aug–30 Nov
Sieber, K  6 Jul–31 Jul
Stark, IDB  local participant
Stoughton, A  6 Jul–31 Jul
Tennent, RD  6 Jul–31 Jul
Viswanathan R 6 Jul–15 Dec
Wagner, K  local participant
Winskel, G  1 Aug–15 Dec
Yonezawa, A  6 Jul–30 Sep

In addition there will be a number of short-term invited visitors in connection with the various focussed events mentioned above.

A.4 School on Semantics and Logics of Computation

The Summer School on Semantics and Logics of Computation is being held in the week 25–29 September 1995, as part of a six-month research programme on Semantics of Computation at the Isaac Newton Institute for Mathematical Sciences, a new international research centre in Cambridge UK. The Summer School is sponsored by the CEC ESPRIT research project ”Categorical Logic in Computer Science, II” (CLICS-II). The aim is to present a number of modern developments in semantics and logics of computation in a way that is accessible to graduate-level students. Registrations from postgraduate students will be given priority, but applications by interested academics and industrialists are also welcomed.

• ”Semantics of interaction” (4 lectures) S. Abramsky (Imperial)

these lectures will survey some recent developments in intensional semantics, which refines the traditional denotational paradigm by modelling programs by processes under interaction, rather than by functions under composition. This allows fine-structural computational properties such as sequentiality, concurrency, flow of information, and use of resources to be addressed in a syntaxfree, compositional fashion.

Specific topics to be covered include: Geometry of interaction, Game semantics, Interaction categories, Specification structures.

• ”Computational content of classical logic” (4 lectures) T. Coquand (Chalmers)

these lectures give an introduction to the problem of extracting constructive content from classical proofs. This problem has an interesting history since it was an important part of Hilbert’s program, who wanted to ”secure” non-constructive parts of mathematics. It has been revived recently by the discovery of intringuing connections with some concepts in computer science.

They will provide both historical and mathematical background to this problem and present concrete examples of non-constructive reasoning in mathematics that is constructively problematic. The emphasis will be on the prooftheoretical side, but the course will also serve as an introduction to the more recent, computer science oriented work cited above.

• ”Dependent type theory: syntax, semantics, and applications” (4 lectures) M. Hofmann (Edinburgh)

The aim of this course is to familiarise participants with the use of dependent types from the viewpoint of their categorical semantics. Dependent types are types depending on values, for instance lists of a fixed length (arrays), the type of constructive proofs of a fixed proposition, the type of certain algebraic structures over a fixed set, etc. Categorical semantics provides a general framework for formulating and verifying interpretations of dependent types.

The course will start with an introduction to theories of dependent types covering Martin-Lof’s type theory, the Logical Framework, and the Calculus of Constructions. Guided by syntactic intuition we develop the notion of ”categories with families”, a simple yet sufficiently general notion of categorical semantics, and define the interpretation of the syntax therein. We then look at some instances such as term models and realisability models and compare to other semantic notions, in particular models based on fibrations. Finally, we treat some larger applications from Computer Science, such as Paulin-Mohring’s method of program extraction from proofs, Moggi’s work on semantics of modules, and the groupoid interpretation of Martin-Lof’s type theory.

• ”Game Semantics” (4 lectures) M. Hyland (Cambridge)

• ”Computational types and applications” (4 lectures) E. Moggi (Genova)

The prerequisites for this course are some knowledge of typed lambda calculus and equational logic. The use of domain theory will be avoided as much as possible, since the basic ideas do not rely on it.

– Lecture 1: Computational types – syntax and equations.

– Lecture 2: Examples of computational types in the category of sets.

– Lecture 3: Semantics of programming languages via translation into a metalanguage with computational types; examples.

– Lecture 4: Modular approach to denotational semantics via reinterpretation of computational types.

• ”Models for concurrency” (4 lectures) M. Nielsen & G. Winskel (Aarhus)

these lectures will highlight a selection of the mathematical structures used in modelling parallel computation, ranging from ”interleaving” models like transition systems to models like Petri nets and Mazurkiewicz traces, where concurrency is represented more explicitly by a form of causal independence. The presentation is unified by casting the models in a category-theoretic framework. Category theory is used to provide abstract characterisations of constructions like parallel composition, and broadly applicable definitions of bisimulation, valid throughout a range of different models. In addition, category theory yields formal means for translating between different models.

• ”Operationally-based theories for proving program properties” (3 lectures) A. Pitts (Cambridge)

The aim of the lectures will be to describe recent advances in techniques based on operational semantics for establishing equivalence of programs. The coinductive characterization of contextual equivalence between functional programs in terms of ”applicative bisimulation” will be presented. The use of coinduction for reasoning about lazy datatypes will be illustrated. The extent to which this characterization generalizes to ”impure” functional languages will be discussed.

About 100 participants are expected, roughly 75% are post-graduates and postdocs while the rest are academics. The majority of participants come from Europe (both west and east). The lecture notes will be published as a volume in the CUP Newton Institute Lecture Series.