CLICS II

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

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

2nd Periodic Progress Report October 4th, 1994

DRAFT – DO NOT DISTRIBUTE

Contents

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

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

3 Workpart Summaries 6 3.1 Progress on Deliverables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Reassessment of themes and targets . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Proposed deliverables for Milestone 3 . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.4 Site management report for Imperial . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.5 Site management report for Aarhus . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.6 Site management report for CAIMENS . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.7 Site management report for Cambridge . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.8 Site management report for Genova . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.9 Site management report for Chalmers . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.10 Site management report for TH Darmstadt . . . . . . . . . . . . . . . . . . . . . . 21 3.11 Site management report for GMD (not available) . . . . . . . . . . . . . . . . . . . 23 3.12 Site management report for Manchester . . . . . . . . . . . . . . . . . . . . . . . . 23 3.13 Site management report for Sussex . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

4 Deliverables Overview 26

5 Deliverables 27

5.1 Report on topics A and G: Sequentiality and Stability, Applied Linear Logic and

Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.2 Report on topic B: Duality in Domain Theory . . . . . . . . . . . . . . . . . . . . . 31 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 languages . . . . . 40 5.5 Report on topics E and F: higher order modal program logics and monadic pro-

gramming language semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 5.6 Report on topic H: Computational Content of Classical Proofs . . . . . . . . . . . 50 5.7 Report on topic I: Symbolic Computation . . . . . . . . . . . . . . . . . . . . . . . 52

A  55

A.1 Report on the CLICS meeting in Paris . . . . . . . . . . . . . . . . . . . . . . . . . 55

Chapter 1

Executive summary

1.1 Milestones and Deliverables

The CLICS II project started on October 1st 1992. The second Milestone occurs after 24 months. The second Review meeting will take place in London on October 4th 1994.

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” (because of inter-relations between some of the topics, we have produced two joint Topic progress reports: one on Topic A and G, the other on Topics E and F). 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.

The progress on the specific deliverables targeted for Milestone 2 (see Section 3.3 of the 1st 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 second year of the project has been fairly successful, despite financial problems due to a six months delay in signing the contract extension, which caused the loss of some researchers funded on the project (see the Site management report for Cambridge). In comparison to the first year, the second one has been more concerned with consolidation and clarification as a necessary prelude to further progress.

Section 3.2 gives a reassessment of some themes and targets, based on discussions during the project meeting held in Paris. In our intentions, the third year should be more concerned with integration of contributions coming from different strands of the project, and in seeking coordination with other projects.

A provisional specification of deliverables for the third project Milestone is set out in Section 3.3; this will be revised in the light of the reviewers’ comments, and the revisions will be incorporated in the final version of this report.

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 and Munich in the area of Synthetic and Axiomatic Domain Theory, through a Science Twinning (Cambridge-Edinburgh-Genova) and a bilateral Vigoni project (Genova-Munich).

• Interaction with TYPES has been very lively. To investigate direct interaction, we plan a joint CLICS-TYPES workshop in January 1995 at Chalmers. The workshop will be focused on two topics, where the synergies between the projects seem particularly promising (see Section 3.2).

Moreover, there is interaction between Sussex (Robinson) and Edinburgh (Power) relevant to TYPES (see the report on Topic C).

• Abramsky’s work on Interaction categories, which forms his contribution to CONFER, has evident strong analogies to the work on game semantics done under the auspices of CLICS II. These analogies have begun to be made precise by work of Cockett and Spooner at Calgary, and by Pavlovic at Imperial. A number of CLICS II researchers will participate in the CONFER workshop to be held at Imperial October 4th-7th. Moreover, there is also interaction between Aarhus (Hermida) and Edinburgh (Power) relevant to CONFER (see the report on Topic A and G).

• There are researchers in Edinburgh (Fiore, Longley, Simpson) and in Munich (Reus, Streicher) who are making important contributions to Synthetic and Axiomatic Domain Theory. We keep in close contact with them, by inviting them to our workshops (see the Report on the CLICS meeting in Paris) and through bilateral collaborations financed by other projects (see the Site management report for Genova).

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

• Important monographs and advanced textbooks have been published within the last year or are forthcoming: Crole’s “Categories for Types” has been published by CUP, Taylor’s “Practical Foundations” is nearing completion.

There is a major contribution to the Handbook of Logic in Computer Science being published by OUP. Abramsky is one of the editors. The following chapters have been written by project members: Domain Theory by Abramsky and Jung, Full Abstraction by Ong, Categorical logic by Pitts. Winskel and Nielsen’s chapter on Models for Concurrency will appear shortly.

• Several members of the project gave lectures at summer schools: Coquand at the Summer School on Automated Theorem Proving (Chambery, July 1994). Dybjer at ESSLLI’94 (Copenhagen, August 1994), Abramsky at Marktoberdorf summer school on Deductive Program Design (August 1994) and at the Banff workshop on Logics for concurrency (September 1994), Moggi at the Advanced School on Typed Lambda Calculus and Functional Programming (Udine, September 1994), Dybjer and Coquand have jointly written lecture notes for their courses.

Others have been invited speakers at international conferences: Pitts at the Canadian Mathematical Society Winter Meeting (Ottawa, 1993). Abramsky and Jung at Mathematical Foundations of Programming Semantics X (March 1994), Abramsky at the TACS conference in Japan (April 1994), Winskel at Mathematical Foundations of Computer Science (August 1994), and Nielsen presented joint work with Winskel and Joyal at CONCUR (August 1994).

1.3 Resources

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

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

Forecast use of person-months in year 1

Topic  A  B C  D  E F  G H  I
Imperial  10  3.5  10 2  25.5
Aarhus  10  7 3.5  8.5  29
Principal CAIMENS 12.5  3  2.5  4  8  30
sites  Cambridge  5  3 6  6 5  3  2  30
Genova  1.5  1.5  3  3 3  1  13
Chalmers  6  4  5  15
Darmstadt  9  6  15
Associate GMD  3  0.5  3.5
sites  Manchester  3 4  4  1 3.5  15.5
Sussex  3.5  3.5  3  10
Total man-months 41.5 35 21 13 12.5 11 26 7 19.5 186.5

Forecast use of person-months in year 2

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

Actual use of person-months in year 1

Topic  A  B C  D  E F  G H  I
Imperial  12  4  3  12  31
Aarhus  1  2 6  6  14  29
Principal CAIMENS  5  2  8  14  29
sites  Cambridge  3  5 2  1  2 4  6  23
Genova  2  3  4  2  11
Chalmers  20  8  28
Darmstadt  4 18  22
Associate GMD
sites  Manchester  4 8  4  16
Sussex  2  2  4
Total man-months 25 35 36 18  9 6 42 8 14  193

Actual use of person-months in year 2

Update on the worldwide state-of-the-art

The CLICS project comprises a considerable proportion of the worldwide state of the art over much of the range of topics it addresses. Moreover, we have excellent contacts with the leading workers in the areas relevant to the project. We will continue to follow the state of the art closely, and to promulgate our own contributions to it, but at present we see no reason to modify the general course of the project in the light of developments elsewhere.

Workpart Summaries

Scientific Workpart Summary

In this summary, we will overview the progress made on the deliverables for Milestone 2 described in Section 3.3 of the 1st Periodic Progress Report.

3.1 Progress on Deliverables

Significant progress has been made on most of the items mentioned in the Deliverables for Milestone 2 described in Section 3.3 of the 1st Periodic Progress Report. It should be emphasized that the work mentioned below is only that which is most directly related to the deliverables for Milestone 2 as specified in the 1st Periodic Progress Report. A full account, including additional work done under the aegis of CLICS II, will be found in the Topic Reports in Chapter 5.

Topic A

Full abstraction results for extensions of PCF. This task has taken longer than expected, since a number of subtleties came up, and techniques for managing quite intricate intensional models had to be developed. But very significant progress has been made. Abramsky and McCusker have proved an algebraic compactness result for the category of games studied by Abramsky, Jagadeesan and Malacaria. This yields a semantics for recursive types. They have used this to investigate the game semantics of the lazy lambda calculus. Abramsky, Jagadeesan and Malacaria have developed a game semantics both for system F, and for PCF extended with full second-order polymorphism. It seems likely that these studies will lead to further full abstraction results.

Connections between strong stability and game semantics. Work by Lamarche and Curien establishing links between game semantics and sequential algorithms, and by Ehrhard connecting sequential algorithms and strongly stable functions, provide some fundamental connections. It remains to be seen if “tighter” extensional models corresponding to the fully abstract versions of game semantics can be found. The work of Plotkin and Winskel on bistructures may be relevant here.

Sequential realizability. Little progress has yet been made, although the game semantics of System F is a first step in this direction.

Topic B

Development of SDT as a setting for Evaluation Logic. This is partially documented by the notes on SDT written by Rosolini. However, further work is needed (see the report on Topic E and F).

The semantic approach to strong normalization arguments. Ong and Ritter have applied a generic strong normalization argument to the Calculus of Constructions. Coquand is considering semantical or reduction-free normalization proofs (best understood as modifications of the glueing construction) to provide efficient normalization algorithms which avoid the implementation of the usual term rewriting mechanism (see report on Topic C).

Moreover, there has been substantial contributions to classical domain theory, and a very promising notion of bistructure has been investigated (see report on Topic A and G).

Topic C

Applications of mixed inductive-recursive definitions. Inductive-recursive definitions have been used for formalizing in type theory its own metatheory. Different formulations of the syntax of type theory inside type theory have been investigate. As a preliminary step towards this investigation, Dybjer has provided a new approach to the coherence problem for dependent types.

Categorical analysis of constructive infinite objects. The stated aim of providing an interpretation of coinductive types in intensional type theory has been superseded. After the work by Martin Hofmann on elimination of extensionality in type theory, it seemed better to factor such an interpretation via Hofmann’s elimination of extensionality and quotient types.

Moreover, Pitts’ inductive-coinductive principles for recursive types have been used to prove computational adequacy results, and Aczel’s final universe approach has been used to characterize models of CCS-like languages.

Topic D

General theory of parametric models of polymorphism. This has been studied from both the syntactic and the semantic side. Curien (and others) has produced a calculus of logical relations, while Robinson and Rosolini have developed a general machinery for producing parametric models.

Models of subtyping. It is possible to adapt the construction by Robinson and Rosolini to give models for languages with subtypes. However, this has not been fully written up, yet. Moreover there has been further work by Hilken and Rydeheard on the theories of classes.

Topic E

Sound and complete axiomatizations of necessity. In a setting consistent with Synthetic Domain Theory, Moggi has been able to reformulate Evaluation Logic as a definitional extension of higher order predicate logic with dependent types and computational types, i.e. the evaluation modalities and evaluation predicate are definable and axioms for them can be proved sound formally.

Incorporation of proof principles for inductive and coinductive types This has not been done. In the light of the above reformulation of Evaluation Logic, it seems more appropriate to place also Crole and Pitts’ FIX-logic in the setting of SDT.

Experiments with interpreting other program logics. We have found a very simple relative interpretation of Variable Typed Logic of Effects (by Talcott and others) into Evaluation Logic. This interpretation overcomes the intensionality problems present in the original formulation of V T LoE.

Topic F

Monadic semantics for the Store calculus. We have constructed a monadic semantics via a suitable notion of ‘applicative bisimulation’; this side-steps some of the domain-theoretic difficulties in favour of a term-model construction based upon operational methods.

Game semantics for dynamic allocation. It was intended that this would draw upon the work being done on game semantics under Topics A and G. However that work has taken longer than expected to write up and as a result it has not been possible to investigate applications of it.

Topic G

Full completeness theorems for larger fragments of LL. Work on this has not yet been made available in print.

Categorical models of bisimulation and refinement. We have come up with an abstract definition of bisimulation, which can be used across a range of different models for parallel computation presented as categories. We have found a promising new model with “refinement” operators, into which the usual category of labeled event structures embeds fully and faithfully. Moreover, we have considered a notion of refinement for event structures, where both causality and conflict can be refined.

Topic H

Applications to the extraction of computational content from classical proofs We have found a formal space such that it is possible to build a non-principal ultrafilter in the topos of sheaves over this space. This gives a way to extract a computational content from any proof that uses a non-principal ultrafilter. Moreover, using heuristically the previous gametheoretical interpretation of proofs, we have given a realizability interpretation of the negative translation of the axiom of choice.

Connections between game semantics for Classical logic, Linear Logic and PCF Hugo Herbelin has made precise the connection between Coquand’s game-theoretical analysis of Classical Arithmetic and the work of Felsher on game-semantics for Intuitionistic Logic.

Topic I

Higher dimensional rewriting. Lafont has presented many interesting case of symbolic calculus with Penrose diagrams. However, manipulating and drawing diagrams by hand is not very easy. A PhD student in Marseille is developing a software tool (in CAML) for drawing, editing and manipulating diagrams, and for computing their normal forms.

3.2 Reassessment of themes and targets

It is to be expected in a project at the foundational level of CLICS II that new themes and topics may emerge or become more prominent during the course of the project. (See the discussion in the first paragraph under Risk Assessment on page 17 of the Technical Annex.) It is important to keep such developments under review, since they clearly can, and should, influence the evolution of the Workplan. According to the Chart on page 26 of the Technical Annex, work on Topics A, C and E is expected to finish after two years. In some Topics we have reached a state, where it seems appropriate to pursue a better integration with other Topics targeted towards more ambitious goals, or to seek coordination with others ESPRIT BRA on specific objectives, when this seems particularly fruitful.

• Game semantics. It has taken longer than expected to write down the full abstraction results for PCF, because of some subtle points (as explained in the report on Topics A and G). This makes us less optimistic regarding an easy “technology transfer” from Topic A to Topics C, D and F. Moreover, we need to understand the trade-offs between our description of the fully abstract model with alternative ones, that various researchers have recently produced.

However, there are clear interconnections between Topics A, G and H, which should be exploited further in the third year. The work of Hugo Herbelin relating Felsher’s work and the sequent calculus LJ can be seen as a first step in interconnecting Topics A and H. Much more should be done in this direction. In particular, there are clear indications that the work of Topic H on computational content of classical proofs will benefit from making explicit its connections with the work of Topics A on sequentiality, and this should constitute a reasonable goal for the third year.

• Towards LCF++. At this stage it seems possible to blend several contributions from different strands of the project to produce a powerful program logic.

The idea is to start with an expressive logical framework (e.g. the Extended Calculus of Constructions), and then add Axiomatic Domain Theory (e.g. in the form of Crole and Pitts’ FIX-logic), the Monadic Approach (e.g. in the form of Evaluation Logic) and Pitt’s inductive-coinductive principles for relational properties of recursive types. To avoid logical inconsistencies we will take a specific model of Synthetic Domain Theory as intended model.

• interaction with TYPES. We plan a joint CLICS-TYPES workshop (Göteborg 8-10 January 1995) to discuss topics of common interest. Among the topics with the highest potential for interaction there are:

– Categorical modeling of type theory. This was one of the core topics around which CLICS-I was formed. Such modeling have recently given rise to several results which throw light on the logics underlying the type theory based proof assistants (ALF, Coq, and Lego) developed in TYPES. For example, Hofmann constructed a groupoid model which showed that Coquand’s very useful method of pattern-matching with dependent types is a non-conservative extension. Another example, also by Hofmann, is the construction of a “setoid” model, by which extensionality and quotient can be eliminated. A third example is Mendler’s use of categorical reasoning to show that coinductive types in general can be encoded in predicative type theory. A fourth concerns the coherence problem that arises when building models of type theory. These problems have been extensively studied in category theory.

– Logical frameworks for program logics. Much of the work in CLICS-II aims at developing logics for proving the correctness of functional programs. Another point of contact with TYPES concerns the use of ALF, Coq, and Lego as logical frameworks which can be used for implementing these logics. There is already some work in this direction, for example, the formalization of synthetic domain theory by Streicher and Reus, of evaluation logic in Cambridge, and on a modular approach to denotational semantics recently started in Edinburgh and Genova.

3.3 Proposed deliverables for Milestone 3

As stipulated in the Technical Annex page 28, we set out proposed deliverables for Milestone 3 in this report. The deliverables set out below are provisional; they will be revised in the light of the reviewers’ comments at the second review; the revisions will be incorporated into the final version of this report. Moreover, as promised in Section II-4.2 of the Technical Annex, we will set up a Summer School. This will be held in Cambridge in conjunction with the Newton Institute Programme on “Semantics of Computation” (July-December 1995).

Topic A (continuation). Models of PCF based on a modified notion of bistructure, along the lines of Ehrhard’s coherences. Investigation of connections between Ehrhard’s hypercoherences, Seiber’s sequential logical relations and O’Hearn and Riecke’s presentation of the extensional fully abstract model of PCF.

Topic B. Extension of the maximality results (see report on Topic B) to the bounded complete setting. A treatment of domain theory in logical form for the continuous case. Applications of Stone Duality to static data types, such as the relational database datatype.

Topic C (interaction with TYPES). Categorical modeling of type theory. Further work on simultaneous induction-recursion, with applications to internal model constructions and reduction-free normalization proofs.

Topic D. Test the power of the model construction for parametric polymorphism, by presenting the parametric “completions” of some of the known models. Adapt the semantic construction to generate models for the system R.

Topic E (integration effort with B and C). A first proposal for LCF++, obtained by blending Evaluation Logic and FIX-logic in the setting of Synthetic Domain Theory.

Topic F. Extend the model of the Monadic Store Calculus based upon applicative bisimilarity to interpret Evaluation Logic, and test his usefulness for proving properties of SML programs.

Topic G. Further Work on presheaf and sheaf models, on categorical treatments of refinement and weak bisimulation.

Topic H. Further investigation of the connections between game theoretical interpretation of classical arithmetic and game interpretation for processes and for sequentiality. A more computational interpretation of proofs in classical analysis with the Axiom of Choice, possibly using the work of Lamarche and Curien relating games and sequential algorithms.

Topic I. A general theory of rewriting Penrose generalizing word rewriting. An interactive tool for manipulating diagrams.

Management Workpart Summary

3.4 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), Roy Crole and Duško Pavlović (3 man-months)

EPSRC-funded Research Assistant: Pasquale Malacaria (6 man-months). External Collaborator: Radha Jagadeesan (Assistant Professor at Loyola University Chicago),

3 man-months.

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, Jagadeesan, Malacaria, McCusker.

Topic B: Taylor, Vickers. Topic E: Crole. Topic G: Abramsky, Jagadeesan, Lamarche, Pavlović.

Interaction with other sites

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

1. The Cambridge and Imperial sites organised a joint seminar on Game Semantics which met about every month, alternating between the two sites. This was then extended to a tripartite arrangement with Oxford on Luke Ong’s moving there to take up a lectureship; Ralph Loader also participated in this seminar.

2. CAIMENS. François Lamarche and Pasquale Malacaria both took up positions at Imperial, having previously worked at ENS. This has been very helpful in maintaining the flow of ideas and contacts. Also, Pierre-Louis Curien’s work on games and sequential algorithms refers strongly to the work of Samson Abramsky, Radha Jagadeesan and François Lamarche. We have also begun to make connections between the work at Imperial on game semantics, and the work by Vincent Danos, Laurent Regnier, Andrea Asperti and Cosimo Laneve on paths. We intend to pursue this link further during the next review period.

3. Darmstadt. Michael Huth visited Imperial for a week in January 1994 and gave a talk on linear lattices. He has now taken up a five-year research position at Darmstadt. His work on Linear lattices with Achim Jung and Klaus Keimel has thrown up some unexpected and fascinating connections with games. Samson Abramsky and Achim Jung completed their joint chapter on Domain theory for the Handbook of Logic in Computer Science.

4. Cambridge, Edinburgh, Genova and others. The questions raised about synthetic domain theory during Paul Taylor’s visit to Genova in March 1993 led to a lively discussion by electronic mail. An electronic mail forum was set up, based at Imperial. This has about thirty members, mainly CLiCS-II participants but also including Peter Freyd from Philadelphia, and has been very active.

Conferences attended

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

CLiCS-II Workshop, Paris (June 1994), attended by Samson Abramsky, Roy Crole, Ian Mackie, Guy McCusker, Pasquale Malacaria, Paul Taylor.

CONFER workshop, Munich (April 94), attended by François Lamarche and Ian Mackie.

Computer Science Logic 94 , Kasimierz, Poland (September 1994); Roy Crole will talk about A Sound Metalogical Semantics for I/O.

European Colloquium on Category Theory Tours (July 1994), attended by François Lamarche and Paul Taylor. (Roy Crole and Duško Pavlović had to withdraw for personal reasons.)

Logic in Computer Science Paris (June 1994) attended by Samson Abramsky, Ian Mackie, Pasquale Malacaria, Guy McCusker, Duško Pavlović.

Peripatetic Seminar on Sheaves and Logic Brighton (March 1994) and Edinburgh (May), attended by Duško Pavlović, Roy Crole and Paul Taylor.

Mathematical Foundations of Programming Semantics X , Manhattan Kansas (March 1994), attended by Samson Abramsky and Pasquale Malacaria

Theoretical Aspects of Computer Software, Sendai (April 1994), attended by Samson Abramsky

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 for Recursive types, 1994 Theory and Formal Methods Workshop.

Geoffrey Burn, Simon Gay and Mark Ryan, Theory and Formal Methods 1993 , Springer Workshops in Computing.

Roy Crole, Categories for Types. In series Cambridge Mathematical Textbooks, Cambridge University Press, 1994. ISBN 0 521 45092 6. 335pp.

Roy Crole, Computational Adequacy of the FIX Logic. Accepted for the MFPS 1992 special edition of Theoretical Computer Science, to appear in 1994. 26 pp.

Roy Crole, On Fixpoint Objects, FIX-Categories, and Glueing Constructions. Accepted for the European Colloquium on Category Theory, (Tours 1994). To be submitted to the ECCT special edition of Applied Categorical Structures. 26pp.

Roy Crole and Andrew Gordon, A Sound Metalogical Semantics for Input/Output Effects. Accepted for Computer Science Logic 94 , Kazimierz, Poland. 5pp. Full version in preparation.

Roy Crole, Simon Gay and Raja Nagarajan, An Internal Language for Interaction Categories. In preparation, to be submitted to the 1994 Theory and Formal Methods Workshop.

Mark Dawson and Steve Vickers, Towards a GeoZ Toolkit, 1994 Theory and Formal Methods Workshop.

Chris Hankin, Ian Mackie and Raja Nagarajan, Theory and Formal Methods 1994: Proceedings of the Second Imperial College, Department of Computing, Workshop on Theory and Formal Methods, to be held at Churchill College,Cambridge. 11–14 September 1994, Springer-Verlag Workshops in Computing.

François Lamarche, Proof Nets for Intuitionistic Linear Logic I: Essential Nets. Presented at CONFER workshop, preliminary report available.

François Lamarche, Dialectics: a Model of Linear Logic and PCF . Preliminary report available. François Lamarche, Hypercoherences are Chu spaces, 1994 Theory and Formal Methods work-

shop.

Paul Taylor, Intuitionistic Sets and Ordinals, which had been presented at Category Theory and Computer Science in Amsterdam in September 1993, was completed in January 1994 and submitted to a conference special issue of Mathematical Structures in Computer Science.

Paul Taylor, Practical Foundations, to be published by Cambridge University Press, is nearing completion. Much of this academic year has been spent on the chapters Well founded induction and Dependent type theory.

Steve Vickers, Geometric Logic in Computer Science, 1993 Theory and Formal Methods Workshop.

Steve Vickers, Topical Categories of Domains, work in progress arising from presentation at Aarhus CLiCS workshop

Steve Vickers, Locales are not pointless, work in progress for 1994 Theory and Formal Methods Workshop.

Steve Vickers, Geometric Logic as a Specification Language, work in progress for 1994 Theory and Formal Methods Workshop.

3.5 Site management report for Aarhus

3.5.1 People working on the project

• Permanent members of staff : Glynn Winskel has contributed about 4 man months. Mogens Nielsen and Uffe Engberg have each contributed 1 man month. In addition, Anders Kock, employed at the Mathematics Department, is a recognised expert in category theory and topos theory in particular, has at times shown a keen and active interest in CLICSII activities; in particular, a regular seminar on category theory (and computer science) has been held jointly with those interested from the maths department.

• Contract research workers: Sergei Soloviev has been employed by the project since January 1993, and so has contributed 21 man-months so far. Claudio Hermida, also employed by the project since September 1993, has contributed 12 man months. In July, Vladimiro Sassone started a postdoctoral position at Aarhus, employed 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 are working towards PhD’s full time; Their research areas fall within CLICSII. MSc student Henrik Enstrøm is completing a thesis on synthetic domain theory.

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. Topic B: Nielsen, Winskel. Topic C: Hermida. Topic D: Hermida, Soerensen. Topic G: Engberg, Brauner, Nielsen, Soloviev, Winskel.

3.5.2 Interaction with other sites

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

• Cambridge (Brauner has made several visits)

• Paris (Ehrhard visited Aarhus in November, while we have all to varying extents visited Paris)

• Genova (Cattani’s several discussions with Rosolini)

• Imperial (Winskel’s visit in January)

• Goteborg (Soloviev’s visit in February)

• Marseilles (Soloviev’s visit in July)

• Darmstadt (Soloviev’s visit in February)

• Sussex (Hermida’s visit in March)

Soloviev (Aarhus) and Longo and Milsted (Paris) have collaborated on papers addressing polymorphism. In addition there has been many fruitful and promising exchanges with Ehrhard, Bucciarelli and Curien (Paris). It is planned for Pitts to visit Aarhus in November-December and for Robinson (Sussex) to visit for 2 months.

3.5.3 Conferences attended

The following conferences and workshops (not including CLICS meetings) 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 ∗):

∗Computer Science Logic ’94, September, 1994 Peripatetic Seminar on Sheaves and Logic, Edinburgh, May, 1994 ∗Mathematical Foundations of Computer Science, Slovakia, August 1994. Logic in Computer Science, Paris, July 1994. ∗Mathematical Foundations of Programming Semantics IX, Kansas, April 1994. ∗International Colloquium on Automata Languages and Programming, Jerusalem, July 1994. Logic and Computer Science, Luminy, June 1994. ∗CONCUR94, Uppsala, August, 1994.

3.5.4 Publications

[Braa] T. Braüner. A general adequacy result for a linear functional language. Presented at MFPS ’94.

[Brab] T. Braüner. The Girard translation extended with recursion. Accepted to CSL ’94, Warsaw, Poland.

[Bra94] T. Braüner. A model of intuitionistic affine logic from stable domain theory. In ICALP ’94, LNCS 820, 1994.

[EW94] Uffe H. Engberg and Glynn Winskel. Linear logic on Petri nets. Technical Report RS-94-3, February 1994. 54 pp. Appears in: Proceedings of REX ’93 (eds. J. W. de Bakker et al.), LNCS 803, 1994.

[HJ94] C. Hermida and B. Jacobs. Fibrations with indeterminates: Contextual and functional completeness of polymorphic lambda calculi. Accepted for MSCS.

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

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

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

3.6 Site management report for CAIMENS

3.6.1 People working on the project

People working on the project

1. Pierre-Louis Curien, Laboratoire d’Informatique de l’Ecole Normale Supérieure, Paris. Games, Symmetric Sequential algorithms and Linear Logic. From September 93 to September 94, invited by the Academy of Science in Pekin, China.

2. Yves Lafont, CNRS - Laboratoire de Mathématiques Discrètes, Marseille. Linear Logic and Interaction Nets, Geometry of Symbolic Computation.

3. Antonio Bucciarelli, Laboratoire d’Informatique de l’Ecole Normale Supérieure, Paris. Strong Stability, Degrees of Parallelism.

4. Thomas Ehrhard, Institut Gaspard Monge, Université de Marne la Vallée, Noisy-le-Grand. Strong Stability, Hypercoherences.

5. Anne Massol, CNRS - Laboratoire de Mathématiques Discrètes, Marseille. Geometry of Symbolic Computation (implementation)

• Permanent members of staff : P.-L. Curien, T. Ehrhard, Y. Lafont (6 man-months).

• Contract research workers: A. Massol is employed on this project since November 93 (11 man-months). A. Bucciarelli is employed on a HCM-funded research project.

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

Topic A: Bucciarelli, Curien, Ehrhard. Topic D: Curien. Topic G: Curien, Ehrhard, Lafont. Topic I: Lafont, Massol.

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

• ∗Logic in Computer Science IX, Paris, July 1994.

• ∗Mathematical Foundations of Programming Semantics IX, New Orleans, April 1993.

• ∗Mathematical Foundations of Programming Semantics X, Manhattan, March 1994.

3.6.2 Publications

[bucc94] Antonio Bucciarelli Degrees of parallelism in the continuous type hierarchy, unpublished notes, 1994.

[ehrcol94] Loïc Colson and Thomas Ehrhard, On Strong Stability and Higher order Sequentiality, Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pag. 103–109, 1994.

[ehr93] Thomas Ehrhard, Projecting sequential algorithms on strongly stable functions, to appear in Annals of Pure and Applied Logic.

[lafont93] Yves Lafont A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier), to appear in Journal of Pure and Applied Algebra (North Holland).

[lafont94a] Yves Lafont From Proof-Nets to Interaction Nets, to appear in the proceedings of the Linear Logic Workshop (Cornell, 1993).

[lafont94b] Yves Lafont Equational Reasoning with 2-dimensional Diagrams, to appear in the proceedings of a summer school on rewriting (Font-Romeu 93, LNCS, Springer-verlag).

3.7 Site management report for Cambridge

3.7.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:

Eike Ritter was employed as a Research Associate by the project until 31 December 1993, and so contributed 3 man months.

Kim Wagner has been employed as a Research Associate by the project since 1 June 1994, and so has contributed 4 man months.

Nick Benton, Gavin Bierman, Andrew Gordon, Barney Hilken, Valeria de Paiva, and Luke Ong each contributed about 1 man month.

• Research students:

Joshua Ross and Ian Stark have each contributed about 1 man month.

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Eike Ritter (3 man months) and Kim Wagner (4 man months).

These people made contributions to the following Topics in the project Work-plan:

Topic A: Hyland, Ong. Topic B: Hyland, Wagner. Topic C: Pitts, Gordon. Topic D: Hilken. Topic E: Paiva, Pitts, Stark. Topic F: Paiva, Pitts, Ritter, Stark. Topic G: Benton, Bierman, Hyland, Paiva, Ritter, Ross.

3.7.2 Interaction with other sites

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

1. The Cambridge and Imperial sites organised a joint seminar on Game Semantics with Oxford University (following the move of Ong from Cambridge to Oxford in January 1994) which met about once a month.

2. Pitts and Stark both visited the Genova site in connection with work on Topics E and F.

3. Barney Hilken who was an associate of the CLICS-II project in Manchester, moved to the Cambridge site in October 1993 to take up a SERC postdoctoral research fellowship.

4. Andrew Gordon moved from the Chalmers Site to the Cambridge site in January 1994 where he is employed by the ESPRIT Types for Proofs and Programs project. He has made contributions to CLICS Topic C and strengthens our interaction with the Types for Proofs and Programs project.

The following other short visits were made:

21/10/93: visit of G. Bellin (Paris) to Cambridge. 6/6/94: visit of R. Goré (Manchester) to Cambridge. 27/7/94: visit of Th. Altenkirch (Chalmers) to Cambridge.

3.7.3 Conferences attended

The following conferences and workshops contained presentations of work done on the project at the Cambridge site. Project funds were only used to cover attendance at the last one of the events listed.

Canadian Math. Society Winter Meeting, Ottawa (Canada), December 1993. Jumelage meeting on Typed Lambda Calculus, Roma (Italy), December 1993. Theory and Formal Methods Workshop, Cambridge, September 1994. Computer Science Logic’94, Kazimierz, Poland, September 1994.

3.7.4 Publications

[CG] Roy L. Crole and Andrew D. Gordon. A sound metalogical semantics for input/output effects. In Computer Science Logic’94, Kazimierz, Poland, September 26–30, 1994. Proceedings to appear in Springer LNCS.

[Hil94] B. P. Hilken. Towards a proof theory of rewriting: the simply-typed 2-λ-calculus. Technical Report 336, University of Cambridge Computer Laboratory, 1994. Journal version submitted.

[HO93] J. M. E. Hyland and C.-H. L. Ong. Fair games and full completeness for Multiplicative Linear Logic without the mix-rule. preprint, 29 pages, 1993.

[HO94] J. M. E. Hyland and C.-H. L. Ong. Dialogue games and innocent strategies: An approach to observational full abstraction for PCF. preprint, 89 pages, 1994.

[NdPR94] Monica Nesi, Valeria de Paiva, and Eike Ritter. Rewriting properties of combinators for intuitionistic linear logic. In Proceedings of the Workshop on Higher Order Algebra, Logic and Term Rewriting. To appear in Lecture Notes in Computer Science, Berlin, Heidelberg, New York, 1994.

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

[OR94] Luke Ong and Eike Ritter. A Generic Strong Normalization Argument: Application to the Calculus of Constructions. Lecture Notes in Computer Science No. 832, Berlin, Heidelberg, New York, 1994.

[Pit93] A. M. Pitts. Relational properties of domains. Technical Report 321, Cambridge Univ. Computer Laboratory, December 1993. 37 pages.

[Pit94a] A. M. Pitts. Categorical logic. A chapter of Volume XI of the Handbook of Logic in Computer Science (S. Abramsky, D. M. Gabbay and T. S. Maibaum, eds), to appear., April 1994.

[Pit94b] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[Pit94c] A. M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., New Orleans, LA, USA, April 1993, volume 802 of Lecture Notes in Computer Science, pages 72–82. Springer-Verlag, Berlin, 1994.

[Rit94a] Eike Ritter. Normalization for typed lambda calculi with explicit substitution. In Proceedings of the 1993 Annual Conference of the European Association for Computer Science Logic, pages 295–304. Lecture Notes in Computer Science No. 832, Berlin, Heidelberg, New York, 1994.

[Rit94b] Eike Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, to appear 1994.

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

3.7.5 Problems

Cambridge University will not allow its researchers to incur expenses on a research project for which there is no valid contract. The contract for the first 15 months of this project expired on 31 December 1993, but the signed first contract amendment extending the project to its full 3 years was not received by Cambridge until the end of May 1994. This five month hiatus and the uncertainty it caused most definitely hampered progress on the project in Cambridge. The most serious problem was that the Research Associate employed by the project (E. Ritter) was forced to find a job elsewhere (he moved to a research post in Oxford). A secondary problem was that visits by Pitts and Stark to Genova in March 1993 in connection with work on Topics E and F had to be funded from other sources.

3.7.6 Changes of plan

In the initial proposal it was anticipated that Cambridge would employ a single Research Associate on the project for 3 years. This has proved impossible because of the contractual arrangements for this type of project (see the section on Problems above). Eike Ritter and Kim Wagner were employed as postdoctoral Research Associates on the project (for 12 and 4 man months respectively) during the first two project years. During the last year, we plan to employ Valeria de Paiva as a postdoctoral Research Associate for 7 woman months and Ian Stark and Francis Davey as postgraduate Research Assistants for short periods yet to be determined. (All are EU nationals.)

3.8 Site management report for Genova

3.8.1 People working on the project

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

• Research students: Daniela Archieri.

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

Topic B: Moggi, Rosolini.

Topic D: Rosolini. Topic E: Moggi. Topic G: Rosolini.

3.8.2 Interaction with other sites

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

∗7-10/12/93 Cenciarelli and Fiore (Edinburgh) visit Genova.

∗13/01-11/02/94 Moggi (Genova) visits LIENS, Paris.

25-27/03/94 Rosolini (Genova) visits Sussex. 26-30/03/94 Pitts (Cambridge) visits Genova. 30/03-01/04/94 Stark (Cambridge) visits Genova. ∗26-27/05/94 Simpson (Edinburgh) visits Genova.

13/06-11/07/94 Rosolini visits LIENS, Paris. ∗11-31/07/94 Fiore (Edinburgh) visits Genova. ∗8-12/08/94 Moggi (Genova) visits Streicher (Munich) 23-27/08/94 Rosolini (Genova) visits Sussex and Cambridge.

3.8.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 ∗):

Jumelage Meeting on Typed Lambda Calculus, Roma, December 1993. ∗IFIP WG 2.2, San Miniato, June 1994. 54th PSSL, Sussex, March 1994. CLICS-II meeting, Paris, June 1994. 9th LICS Conference, Paris, July 1994.

Work done in the project was also presented in a course taught by Moggi at the Advanced School on Typed Lambda Calculus and Functional Programming, Udine, September 1994, and in a course taught by Rosolini for the Ph.D. degree at the Università di Pisa in September/October ‘94.

3.8.4 Publications

[DGR] P. Degano, R. Gorrieri, and G. Rosolini. Graphs and event refinement. submitted.

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

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

[RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In 9th LICS Conference. IEEE, 1994.

[Ros94] G. Rosolini. Synthetic Domain Theory. draft. Genova, 1994.

3.8.5 Problems

The gap in funding caused by the delay in making available the second round of funds has caused administrative problems, and the University is now reluctant to anticipate money coming from European projects.

3.9 Site management report for Chalmers

3.9.1 People working on the project

• Permanent members of staff : Thierry Coquand and Peter Dybjer have contributed 6 manmonths each. Lars Hallnäs has contributed 1 man-month.

• Contract research workers: Thorsten Altenkirch has been employed as a full-time postdoctoral researcher and has contributed 12 man-months. Graham Hutton has also been employed as a postdoctoral researcher until July (when he moved to Utrecht) and has contributed 10 man-months. Michael Hedberg has been employed as a postdoctoral researcher since July and has contributed 2.5 man-months.

• Research students: Catarina Coquand and Daniel Fridlender are research students at Chalmers and have contributed 3 man-months each. Hugo Herbelin is a research student at ENS Lyon and INRIA-Rocquencourt supervised by Thierry Coquand. He has contributed 3 manmonths.

Of the above man-months of labour, the only ones charged as labour costs to this project are those of Peter Dybjer, Thorsten Altenkirch, and Michael Hedberg.

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

Topic C: Altenkirch, C. Coquand, T. Coquand, Dybjer, Hallnäs.

Topic H: T. Coquand, Fridlender, Herbelin.

3.9.2 Interaction with other sites

Thorsten Altenkirch, Thierry Coquand, and Peter Dybjer visited the Workshop on Games and Processes in Luminy in October. Thorsten Altenkirch and Peter Dybjer visited the CLICS-II workshop at ENS in June. Thorsten Altenkirch visited Cambridge in July. Roy Crole from Imperial visited Chalmers in October.

3.9.3 Conferences attended

The following conferences and workshops contained presentations of work done on the project at the Chalmers site: Workshop on Games and Processes, Marseilles, October 1993, the TYPES Workshop, Båstad, June 1994, the CLICS Workshop, Paris, June 1994, the LICS Conference, Paris, July 1994, Summer School on Interactive Theorem Proving, Chambery, July 1994, ESSLLI ’94 Summer School, Copenhagen , August 1994.

3.9.4 Publications

[Alt94] Thorsten Altenkirch. Consistency in ALF. In La Wintermöte ’94, Lundsbrunn, January 1994.

[BBC94] Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. Technical report, technical report n 116 of the university of Utrecht, 1994.

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

[Coq94a] Thierry Coquand. A constructive topological proof of van der waerden’s theorem. Journal of Pure and Applied Algebra, 1994. To appear.

[Coq94b] Thierry Coquand. A formal space of ultrafilters. Manuscript, August 1994.

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

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

[Dyb94b] Peter Dybjer. Inductive families. Formal Aspects of Computing, 1994. To appear.

[Dyb94c] Peter Dybjer. On the interpretation of coinductive types in intuitionistic type theory. Manuscript, September 1994.

[Dyb94d] Peter Dybjer. On the syntax of dependent types and the coherence problem. Manuscript, September 1994.

[HB94] Graham Hutton and Carolyn Brown. Categories, allegories, and circuit design. In Proc. IEEE symposium on Logic in Computer Science, July 1994.

[Her94] Hugo Herbelin. A lambda-calculus structure isomorphic to sequent calculus structure. In paper accepted to CSL (Computer Science Logic), 1994.

[MH94] Erik Meijer and Graham Hutton. Fold and unfold simplified and extended (working title). Work in progress, Utrecht University and Chalmers University, 1994.

3.10 Site management report for TH Darmstadt

3.10.1 People working on the project

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

Achim Jung: 9 man month.

Michael Huth: 9 man month.

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

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

No labour costs are charged to the project.

3.10.2 Interaction with other sites

Main interactions have been with Imperial, ENS (Paris), and Sussex.

The following short visits were made:

25–30/1/94: visit of Michael Huth to London. 18–22/2/94: visit of Achim Jung to London.

The following visitors came to Darmstadt for short visits:

Pietro DiGianantonio (Udine) Jürgen Koslowski (Hannover) Kurt Sieber (Saarbrücken) Alberto Pardo (Darmstadt) Andrew Moshier (Saarbrücken) Ralph Kopperman (New York)

3.10.3 Conferences attended

The following conferences and workshops were attended.

CLICS II workshop: Games, Logic, and Processes, Marseille, October 1993 (Jung, Keimel). Workshop on Topology and Completion in Semantics, Chartres, November 1993 (Huth, Jung, Keimel, Sünderhauf). CONFER workshop, Munich, April 1994 (Huth). Short conference on Domain Theory and Semantics, New Orleans, March 1994 (Huth, Jung, Keimel). Mathematical Foundations of Programming Semantics X, Manhattan (Kansas), March 1994 (Huth, Jung, Keimel). CLICS II workshop, Paris, June 1994 (Huth, Jung). Logic in Computer Science IX, Paris, July 1994 (Huth, Jung).

3.10.4 Publications

The following papers have appeared in print: [Hut94c, HJK94b, KP94].

The following papers have been accepted for publication: [Hut94d, Hut94a, Hut94e, AJ94b, FH94].

Submitted to journals are: [Haa94, Hut94a, HJK94a, Sün92, Sün93, Sün94b] As technical reports have been published: [Hut94b, Sün94b]. One PhD thesis has been completed: [Sün94a].

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

[FH94] A. Fiech and M. Huth. Algebraic Domains of Natural Tranformations. Theoretical Computer Science, 1994. to appear.

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

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

[Hut94a] M. Huth. Functional Bisimulation. submitted to the special issue of TCS commemorating the workshop on Semantics and Completion in Chartres, France, November 1993, 1994.

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

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

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

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

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

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

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

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

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

3.10.5 Problems

The administration at Darmstadt has caused us tremendous difficulties because of the delay in the second payment.

3.11 Site management report for GMD (not available)

3.12 Site management report for Manchester

3.12.1 People working on the project

• Permanent members of staff : David Rydeheard, Harold Simmons and Peter Aczel each contributed 4 man-months to the project.

• Contract research workers: Fu Yuxi was employed on CLICS-II funds for 4 months, 1.4.93 – 30.6.93, but has now left to take up a post in China. The work undertaken during this period is now in the process of being published (see below). Gilles Barthe was funded by the EU Types for Proofs and Programs project for 4 months during which some of his work was associated with the CLICS-II project.

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

Topic B: Simmons Topic C: Fu, Aczel Topic D: Rydeheard

3.12.2 Interaction with other sites

Barney Hilken who was an associate of the CLICS-II project, has now moved to our CLICS-II managing site, Cambridge University, as a SERC postdoctoral research fellow.

3.12.3 Conferences attended

The following conferences and workshops contained presentations of work done on the project at Manchester:

The 9th International Conference on Mathematical Foundations of Programming Semantics, New Orleans, April 1993. Peripatetic Seminar on Sheaves and Logic, Sussex University, March 1994. Peripatetic Seminar on Sheaves and Logic, Edinburgh, May 1994.

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

[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. Submitted to Mathematical Structures in Computer Science.

[Fub] YuXi Fu. CZF in Martin-Löf’s type theory without identity types. Submitted to Theoretical Computer Science.

[Fuara] YuXi Fu. Encodings in polymorphism, revisited. Studia Logica, To appear.

[Fuarb] YuXi Fu. Recursive models of general inductive types. Studia Logica, To appear.

[HRa] B.P. Hilken and D.E. Rydeheard. Categories with computable structure. Submitted to Mathematical Structures in Computer Science.

[HRb] B.P. Hilken and D.E. Rydeheard. A theory of classes: Proofs and models. Submitted to Mathematical Structures in Computer Science.

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

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

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

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

[Sime] H. Simmons. Taking the Curry-Howard correspondence seriously. Preprint: Lecture Notes. Available on ftp from 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.12.5 Problems

The gap in funding caused by the delay in making available the second round of funds has caused administrative problems at Manchester, which now seem to be overcome.

3.13 Site management report for Sussex

3.13.1 People working on the project

• Permanent members of staff : Edmund Robinson has contributed about four man-months. Allen Stoughton left in October 1993 to take up a position in the United States.

• Contract research workers: Andrea Schalk moved to Sussex from Darmstadt in October.

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. Topic F: Robinson.

3.13.2 Interaction with other sites

Sussex has had an important interaction with Genova during the review period.

1. Genova. We have had visits from Rosolini. These contributed to joint work on parametricity which we expect will continue into the next review period.

In addition, we have had an interaction with the ESPRIT BRA project TYPES, through John Power (Edinburgh).

The following short visits were made:

11,12/11/93: visit of John Power (Edinburgh) to Sussex. 23,24,25/2/94: visit of Edmund Robinson (Sussex) to Edinburgh. 26,27/3/94: visit of Pino Rosolini (Genova) to Sussex. 25,26,27/3/94: visit of John Power (Edinburgh) to Sussex. 9/5/94: visit of Martin Hyland (Cambridge) to Sussex. 10/8/94: visit of Francois Lamarche (Imperial) to Sussex.

3.13.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 ∗):

CLICS-II Workshop on Games and Processes, Luminy, October 1994 Peripatetic Seminar on Sheaves and Logic 54, Sussex, March 1994. Peripatetic Seminar on Sheaves and Logic 55, Edinburgh, May 1994. CLICS-II Workshop, Paris, June-July 1994. Logic in Computer Science 9, Paris, July 1994.

Note that the site was involved in hosting the 54th Peripatetic Seminar on Sheaves and Logic, in March 1994.

3.13.4 Publications

[Rob94a] E.P. Robinson. A note on the presentation of enriched monads. available by ftp from

theory.doc.ic.ac.uk, August 1994.

[Rob94b] E.P. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Computer Science Technical Report 6/94, University of Sussex, April 1994. (submitted to Mathematical Structures in Computer Science).

[RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In S. Abramsky, editor, Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, July 4-7, 1994, Paris, France, pages 364–371, Los Alamitos, California, 1994. IEEE Computer Society Press.

Chapter 4

Deliverables Overview

The deliverables for Milestone 2 comprise the following:

1. Reports on each of the Topics A through I compiled by the Topic Leaders. There are two joint reports: one on the topics A and G, the other on the topics E and F. 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 E Evaluation Logic  Eugenio Moggi
and F Monadic Semantics  Andrew Pitts
Report on Topic H Computational Content of Classical Proofs Thierry Coquand
Report on Topic I Symbolic Computation  Yves Lafont

2. A report on the CLICS meeting held in Paris in June 1994.

Deliverables

5.1 Report on topics A and G: Sequentiality and Stability, Applied Linear Logic and Concurrency

5.1.1 Summary

This report describes work done during Year 2 on Topics A (Sequentiality and Stability) and G (Applied Linear Logic and Concurrency). Because so much work on sequentiality and stability rests on linear logic, the two topics are combined in this presentation. This topic contributes to the project objectives in the areas of “Semantics and Logics of Programming Languages”, “Domain Theory” and of course “Concurrency and Linear Logic”. The proposed deliverables for Milestone 2 were:

• Full abstraction results for extensions of PCF. Significant progress has been made on. Abramsky and McCusker have proved an algebraic compactness result for the category of games studied by Abramsky, Jagadeesan and Malacaria. This yields a semantics for recursive types. They have used this to investigate the game semantics of the lazy lambda calculus. Abramsky, Jagadeesan and Malacaria have developed a game semantics both for system F, and for PCF extended with full second-order polymorphism. It seems likely that these studies will lead to further full abstraction results.

• Connections between strongly stable functions and game semantics. The work by Lamarche and Curien establishing links between game semantics and sequential algorithms, and by Ehrhard connecting sequential algorithms and strongly stable functions, provide some fundamental connections. It remains to be seen if “tighter” extensional models corresponding to the fully abstract versions of game semantics can be found. The work of Plotkin and Winskel on bistructures seems relevant here.

• sequential realizability and the logic of sequentiality. Little progress has yet been made, although the game semantics of System F is a first step in this direction

• Full completeness theorems for larger fragments of Linear Logic, and for fragments of Intuitionistic and Classical Logic via translations into Linear Logic. Progress is not yet presented in print.

• Further investigation of categorical models of bisimulation and refinement. Work on this is contained in the deliverables [JNW94, DGR94]; further work is in progress, but not yet documented.

The results reported here largely appear in conference proceedings, though a few have recently been submitted to journals. The publications forming the deliverables of these two topics are: [Col94], [Bra94], [HB94], [Laf93], [Rit94], [NdPR94], [DGR94], [PW94], [JNW94], [EW94], [Win94].

5.1.2 Work completed

Very striking progress was made in this area in the first year of CLICS-II (see the first Periodic Progress Report):

• Ehrhard showed that strongly stable functions were the extensional collapse of sequential algorithms.

• Abramsky, Jagadeesan and Malacaria and Hyland and Ong developed somewhat different versions of game semantics for PCF, and proved that these gave rise to fully abstract models.

In following these lines, the second year has been more concerned with consolidation and clarification, as a necessary prelude to further progress.

• Ehrhard and Colson [Col94] have given another striking characterization of strong stability in terms of a kind of logical relation extension of sequentiality to higher types. This provides further evidence for the robustness of strong stability, and its intrinsic connections to sequentiality.

• Abramsky, Jagadeesan and Malacaria and Hyland and Ong have been writing detailed accounts of their results on game semantics, definability and full abstraction. These papers are now nearing completion. The task has necessarily been rather lengthy, since a number of subtleties were thrown up, and also techniques for managing these quite intricate intensional models had to be developed.

Among the issues which were encountered:

• The notion of model of PCF had to be refined. Abramsky, Jagadeesan and Malacaria introduced the notion of rational cartesian closed categories, which require only the existence of suprema of chains “definable” by iterating morphisms, rather than of arbitrary chains. This notion appears to have some independent interest as a more general framework for Axiomatic Domain theory than cpo-enrichment. Hyland and Ong took a more categorical approach; their notion of model should mesh well with Synthetic Domain Theory.

• The results on definability were extended by both groups to Universality theorems, to the effect that all recursive strategies are PCF-definable.

• The notion of intrinsic preorder introduced by Abramsky et al. as a way of constructing the extensional quotient of the games model was put in a more abstract setting by Hyland and Ong.

• Hyland and Ong have investigated a translation of their strategies into Milner’s π-calculus.

• Abramsky and McCusker have extended the AJM semantics to recursive types, proving minimal invariance properties a la Freyd. The fact that rationality suffices for this purpose indicates that weaker axioms than had previously been considered should suffice for (orderenriched) Axiomatic Domain Theory.

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

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

The work [EW94] is directly concerned with linear logic, exploring Petri nets as models for intuitionistic linear logic. This article shows how individual Petri nets form models of Girard’s intuitionistic linear logic. It explores questions of expressiveness and completeness of linear logic with respect to this interpretation. An aim is to use Petri nets to give an understanding of linear logic and give some appraisal of the value of linear logic as a specification logic for Petri nets. This article might serve as a tutorial, providing one in-road into Girard’s linear logic via Petri nets. With this in mind it contains several exercises and their solutions.

In [Laf93, Laf94], Yves Lafont has developed the paradigm of interaction for concurrent computing, which is based on a generalisation of Girard’s proof-nets. Recently, he introduced a very simple system of interaction combinators with only 3 symbols and 6 rules. This system is complete in the sense that any other interaction system can be translated into it. It also happens that any net built with these 3 symbols defines a sequential machine with 2 stacks. This machine is a simple kind of Geometry of Interaction.

Ruby is a relational calculus for describing digital circuits, and deriving circuits from their specifications by a process of algebraic reasoning. A key aspect of Ruby is that the relational terms also have a pictorial interpretation as simple circuit diagrams. This interpretation was formalised in [1]. Circuit diagrams are shown to form a unitary pretabular allegory (upa). Moreover, with respect to a natural equivalence on diagrams defined in terms of obtaining one diagram from other by adding extra wires and components, the upa axioms are shown to be sound and complete for the interpretation of terms as circuit diagrams. This result also provides a decision procedure for equality of upa terms.

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

In [JNW94] (a journal version submitted to a LICS93 Special issue of Information and Computation) an abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labeled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. Gian Luca Cattani is investigating refinement and presheaf models for concurrency, under the supervision of Winskel.

Related is the work of [DGR94], where general refinement of event structures is considered, where both causality and conflict can be refined. it is a direct development of a previous proposal [DGR92], which shared some technicalities with [CGW89], to a completely unconstrained notion of refinement of event structures. The main contribution of the paper is the new point of view from which to consider event structures (and their domain representations). An event structure is seen as a symmetric graph of posets. By this it is possible to define refinement data in an almost straightforward way, and obtain directly the domain representation of the refined event structure as the poset of “sections” of the refinement data. It is also able to state conditions ensuring refinement preserves causality or conflict.

Finally there has been work on naming structures (this is joint work between C. Hermida (Aarhus) and A.J. Power (Edinburgh)). Some preliminary progress has been made towards a categorical refinement of Milner’s work on action/control structures, which recast the main ideas of this latter in a more traditional categorical logic framework, using fibrations with structure. The emphasis is placed upon a purely categorical account of the manipulation of ‘names’ within actions (or processes), while keeping a precise correspondence with Milner’s original and current work. Further work is required to account for some essential concepts, like bisimilarity, in this setting, as well as a refined analysis of the relationship with existing models.

5.1.3 Future plans

Game semantics and strong stability continue to stimulate new research set out above. Several intriguing issues/questions remain as regards models of PCF, and related languages like its linear counterpart. For instance, further work is planned on bistructure models of PCF; in particular, on connections between Ehrhard’s hypercoherences and Seiber’s sequential logical relations and O’Hearn and Riecke’s presentation of the extensional fully abstract model of PCF (this builds on work of Jung, of CLICSII Darmstadt, and Tiuryn). Is there an analogue of Loader’s undecidability result for pure typed lambda calculus for finitary PCF? Work will continue on presheaf and sheaf models, and on categorical treatments of refinement, as well as weak bisimulation.

5.1.4 References and selected publications

[Bra94] T. Braüner. A general adequacy result for a linear functional language. Presented at MFPS ’94.

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

[DGR94] P. Degano, R. Gorrieri, and G. Rosolini. Graphs and event refinement. submitted.

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

[EW94] Uffe H. Engberg and Glynn Winskel. Linear logic on Petri nets. Technical Report RS-94-3, February 1994. 54 pp. Appears in: Proceedings of REX ’93 (eds. J. W. de Bakker et al.), LNCS 803, 1994.

[HB94] Graham Hutton and Carolyn Brown. Categories, allegories, and circuit design. Proc. IEEE symposium on Logic in Computer Science, July 1994, 1994.

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

[Laf93] Y. Lafont. From proof-nets to interaction nets. to appear in the proceedings of the Linear Logic Workshop (Cornell, 1993.

[Laf94] Y. Lafont. The paradigm of Interaction. In preparation, 1994.

[NdPR94] Monica Nesi, Valeria de Paiva, and Eike Ritter. Rewriting properties of combinators for intuitionistic linear logic. In Proceedings of the Workshop on Higher Order Algebra, Logic and Term Rewriting. To appear in Lecture Notes in Computer Science, Berlin, Heidelberg, New York, 1994.

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

[Rit94] Eike Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, to appear 1994.

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

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

5.2 Report on topic B: Duality in Domain Theory

5.2.1 Summary

This report describes work done during Year 2 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 new notions ofdomains has mainly involved Aarhus and CAIMENS; collaboration on synthetic domain theory involved Cambridge, Genova and Imperial with additional input from Streicher and Reuss in Munich. The following publications form the deliverables under this Topic: papers appearing in print [Hut94c, HJK94b, Haa94, KP94, OR94]; papers accepted for publication [Hut94d, Hut94a, Hut94e, AJ94b, FH94]; technical reports [Hut94b, Sün94b, PW94, Win94]; research notes [Ros94]; PhD thesis [Sün94a].

The proposed deliverables for milestone 2 were the development of Synthetic Domain Theory as a setting for evaluation logic, and the extension of the semantic approach to strong normalization arguments. The first of these is partially represented by [Ros94] and more fully by discussions on the SDT email list. But more work is needed in view of the report on topic EF. The second is represented by [OR94]. The other deliverables constitute substantial contributions to classical domain theory.

5.2.2 Work completed: traditional domain theory

5.2.2.1 Linear Types

Linear logic was identified as an important technical tool in the original proposal. In the context of traditional (Scott and stable) domain theory, it has been studied by Paul Taylor at Imperial, and this theme has been developed further. Huth [Hut94e] took as starting point the cartesian closed category of prime-algebraic domains [Win88], a proper full subcategory of Scott-domains. There is a simple monad on a symmetric monoidal closed category PRIME of distributive Scott-domains whose Kleisli category is a cartesian closed category of prime-algebraic domains. Further, PRIME is the greatest such category with distributive Scott-domains as objects [Hut94e]. Extensions of such results to all Scott domains present problems. For example, the function space A_{2}−^{∘}A_{2} of the Scott-domain A_{2} in [Hut94c] is not a Scott-domain (not even continuous!). However, Scottdomains are exactly those bounded complete domains where the identity is approximated by Scottcontinuous projections with finite image. So we can call a domain linear [Hut94c] if these functions can be chosen to preserve all existing (not only all directed) suprema. We thus obtain a symmetric monoidal closed category LIN which properly contains PRIME as a full subcategory; an object in PRIME is nothing but a distributive linear domain [Hut94c]. Therefore, it is indeed possible to extend the linear types beyond the prime-algebraic setting such that it even encompasses all finite objects and has colimits of ω-chains of projection-embedding pairs.

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

A fascinating topological symmetry is the coincidence of the Lawson topologies

λ(A) = λ(A^{⊥})  (5.1)

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

5.2.2.2 Other areas

In connection with classical domain theory we report the completion of the chapter Domain Theory which will be part of volume III of the Handbook of Logic in Computer Science [AJ94b]. Its purpose is to give an up-to-date account of domain theory, in particular, the theory of continuous domains. Many people around the world are already using this text as their main reference to domain theory. However a treatment of domain theory in logical form for the continuous case is not included, and is now a focus of research.

Work is also in progress on static datatypes (ordered algebraic structures which derive from datatype definitions not involving the function space operator). The prime example is the datatype relational database. Jung and Puhlmann have been considering the snack powerdomain construction which provides a promising model. Their results will be reported in a paper submitted to MFPS 95. A full account will be given in Puhlmann’s doctoral thesis.

Finally Philipp Sünderhauf has continued his research on quasi-uniform spaces and has presented a PhD-thesis entitled Discrete Approximation of Spaces [Sün94a]. The first half of this thesis is concerned with the problem of finding a good computational model of the real numbers. In the second half he extends his construction to a very general class of spaces. This work should be compared with work by the theory group at Imperial.

5.2.3 Work completed: new notions of domain

In our last report we discussed the important new work done in the project by Ehrhard and his collaborators in providing more sophisticated notions of domain in the stable tradition. This included approaches along the lines of Berry’s bidomains. This year, innovative work by Plotkin and Winskel has extended our understanding of an approach to domains in which both the extensional and a more intensional (computational) order are taken as basic. Bistructures are a generalization of event structures to represent spaces of functions at higher types. In place of the partial order of causal dependency, one has two orders, associated respectively with input and output behaviour. Bistructures give a representation of Berry’s bidomains. This representation can itself be considered the result of a linear decomposition. Bistructures give a categorical model of linear logic (a linear category plus suitably structured comonad). The corresponding Kleisli category is equivalent to a cartesian closed subcategory of Berry’s bidomains.

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

5.2.4 Work completed: synthetic domain theory

Much of the project work in this area remains unpublished, though research is kept in the public domain through the SDT email list set up by Paul Taylor. There have been a number of disparate lines of work.

The great innovation in the subject has been Paul Taylor’s duality theory which provides a context in which there is a miraculously close connection between the abstract domains and their Σ-logic. This work can be seen as a completely abstract and subtle piece of basic category theory, discovered in the context of computer science, but presumably of wider application. Taylor’s work is being studied by project members in Cambridge with a view to understanding better the proof of his main results, and the context in which to see them. There may also be connections with work of Pavlovic on duality and the universal properties characterizing Chu’s construction. An outstanding problem however is the extent to which Taylor’s models can be understood as part of SDT in the original sense of “domains as sets”.

In the second place we have been considering properties of models of SDT which allow for a natural interpretation of Evaluation Logic (along the lines descibed in the report on topic E). This is successfully worked out for the case of the replete objects in some suitable small complete subcategory of a quasi-topos. But as far as Evaluation Logic is concerned we do not need to exploit the special properties of domains and pre-domains; we might as well consider the small complete category itself. Further and more interesting issues arise in connection with the proposal for a program logic LCF ++ as outlined in the report on topic E.

We have also been considering the problem identified in the original proposal to develop duality in analogy with the logical form approach to domain theory. Crude approaches to this have been discussed between the Cambridge, Genova and Munich sites. The general theory which has been developed exploits the essentially algebraic theory of the object Σ and is quite complex, though the analogy stands up quite well. (Things are much improved in the more sophisticated approach taken by Paul Taylor, but see the outstanding problem above.) Another strand of thinking in SDT is that perhaps the duality is not really needed for program semantics.

Finally Rosolini has been preparing some definitive notes on the present state of SDT [Ros94]. These notes contain in fairly complete details the fundamentals on the subject. They are based on the original philosophy that “domains are sets” and try to pursue a general line for as long as possible. They start from the basic results about duality (as in categorical logic, not as in *-autonomous categories), and cover the material about domains as replete objects reformulating the standard theory for denotational semantics to cover the synthetic solution of domain equations.

5.2.5 Future plans

5.2.5.1 Linear aspects

We would be able to extend the maximality results described above to the bounded complete setting presented in [Hut94e] as soon as we could show the following: Conjecture. If A−^{∘}A is a continuous lattice then the uniformity induced by the filters

U_{f} := {(x, y) | x ≤ f(x)},  (5.2)

where f is way-below id_{A} in A−^{∘}A, is totally bounded [Sün94b]. □ This would readily imply the following:

• Such an A would be a linear FS-lattice.

• LFS would be the greatest ∗-autonomous full subcategory of SUP such that every object is bicontinuous; the condition above on the symmetric topologies would therefore be redundant.

• LIN would simply be the greatest symmetric monoidal closed category of Scott-domains.

We hope that progress in that direction can be made using the body of work on quasiuniformities and totally bounded uniform spaces in [Sün94b]; moreover, in [Hut94a], a first version of the fine structure of generating sup-bases for the linear types has been established, providing thereby links with the corresponding work on game semantics in [AJM, AJ94a, HO].

5.2.5.2 Other aspects of traditional domain theory

We expect to contribute to duality theory by producing a treatment of domain theory in logical form for the continuous case. A further goal of this research is a semantically sound logic for approximate measurement. Also we intend more work on the application of Stone Duality to static data types.

5.2.5.3 New models of domains

We aim to replace the conflict relation in extended bistructures by a relation along the lines of Ehrhard’s coherences with the hope of moving closer to a fully abstract model of PCF.

5.2.6 References and selected publications

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

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

[AJ94b] 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, 1994.

[AJM] S. Abramsky, R. Jagadeesan, and P. Malacaria. Games and full abstraction for PCF, preliminary announcement. Note distributed August 1993.

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

[BDW91] P. Buneman, S. Davidson, and A. Watters. A semantics for complex objects and approximate answers. Journal of Computer and System Sciences, 43:170–218, 1991.

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

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

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

[HO] M. Hyland and L. Ong. Dialogue games and innocent strategies: An approach to intensional full abstraction for PCF (preliminary announcement). Note distributed August 1993.

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

[FH94] A. Fiech and M. Huth. Algebraic Domains of Natural Tranformations. Theoretical Computer Science, 1994. Interaction Orders as Games. Technical Report 1639, Technische Hochschule Darmstadt, 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.

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

[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. personal communication, 1994.

[LS86] J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics Vol. 7. Cambridge University Press, 1986.

[ML71] S. Mac Lane. Categories for the Working Mathematician. Springer Verlag, 1971.

[OR94] Luke Ong and Eike Ritter. A Generic Strong Normalization Argument: Application to the Calculus of Constructions. Lecture Notes in Computer Science No. 832, Berlin, Heidelberg, New York, 1994.

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

[Ros94] G. Rosolini. Notes on SDT. Genova, 1994.

[Ran52] G. N. Raney. Completely distributive complete lattices. Proc. AMS, 3:667–680, 1952.

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

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

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

[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 2 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 Aarhus, Cambridge, Chalmers, Manchester, and Sussex.

The deliverables planned for milestone 2 were (i) applications of mixed inductive-recursive definitions to the internalization of normalization arguments in type theory, and (ii) categorical analysis of constructive infinite objects and non-well-founded sets.

The publications which form the deliverables under this Topic are items [Acz94, Dyb94d, Dyb94c, Her93, Pit93a, Pit94a].

While investigating deliverable (i) we found that it was essential to get a good solution of the coherence problem for dependent types. A new approach to this problem is described in [Dyb94d]. This solution uses mixed induction-recursion in a different manner from what was anticipated in the workplan.

The goal for deliverable (ii) has changed somewhat as compared to the workplan. There we stated the aim to provide an interpretation of coinductive types in intensional type theory that would refine Mendler’s [Men91] interpretation in extensional type theory. But since the work by Hofmann [Hof93] on elimination of extensionality in type theory and the ensuing discussions on intensionality versus extensionality, it has seemed better to factor such an interpretation via Hofmann’s. In [Dyb94c] we discuss this and also present a formal construction of final coalgebras directly inside intensional type theory extended with an extensionality axiom.

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

5.3.2 Work completed

5.3.2.1 Logic of well-founded datatypes

The intuitionistic theory of types of Martin-Löf can be viewed as a theory of inductively defined datatypes in the framework of dependent types [Dyb94b, Dyb91].

We have continued work reported in the previous progress report on a schematic extension to intuitionistic type theory which provides a general formulation of simultaneous (or mixed) inductive-recursive definition [Dyb94a]. Thorsten Altenkirch has been working on a simplified presentation of this notion [Alt94a].

The notion of a simultaneous inductive-recursive definition is crucial when using type theory for formalizing its own metatheory. As a step towards this goal we have studied different formulations of the syntax of type theory inside type theory. In particular we have formulated an “intrinsic” syntax of the pure theory of dependent types which avoids introducing raw terms, raw types, etc. This formulation gives rise to a coherence problem, which we solve using simultaneous induction-recursion. This work is closely related to earlier work by Curien on “Substitution up to isomorphism” [Cur], where the investigation of the precise relationship between syntax and categorical models gives rise to similar coherence questions.

We continued our work on semantical or reduction-free normalization proofs [CD93, Coq93]. It turns out that they can be best understood in a purely categorical way as a modification of the glueing construction [Laf88]. We are now able to describe Schwichtenberg’s and Berger’s proof [BS91] by applying a presheaf model of the simply typed λ calculus. We are currently working on extending this approach to a calculus with coproducts using sheaves over a finite cover topology. This represents a good example for the possibility of reusing categorical concepts for computational constructions. A directly pragmatic consequence of this work are new efficient normalization algorithms which avoid the implementation of the usual term rewriting mechanism. Another more theoretical motivation is the hope that we are able simplify the usual decidability for other typed λ-calculi. This is relevant in the areas of proof-checkers and proof editors since their correctness directly depends on the decidability of the equality in the underlying λ-calculus. We hope therefore to exploit this work for the cross-verification of proof checkers.

Thorsten Altenkirch presented his joint work with Hofmann in this area in a seminar in Cambridge in July [Alt94b] and got valuable feedback regarding sheaf models. Altenkirch and Hofmann are currently preparing a paper [AH94] on this subject.

Claudio Hermida has given a category-theoretic account of structural induction for inductively defined data types. The account is based on the understanding of inductively defined data types as initial algebras for certain kind of endofunctors T : B→B on a bicartesian/distributive category B. Regarding a predicate logic as a fibration p : P→B on B, we consider a ‘logical predicate lifting’ of T to the total category P. Then, a predicate is inductive precisely when it carries an algebra structure for such lifted endofunctor. The validity of the induction principle is formulated by requiring that the ‘truth’ predicate functor ⊤ : B→P preserve initial algebras. One main result is that whenever the fibration admits a comprehension principle, analogous to the one in set theory, it satisfies the induction principle. We also consider the appropriate extensions of the above formulation to deal with initiality (and induction) in arbitrary contexts, that is, the ‘stability’ property of the induction principle, and show this extension holds when the fibration is ‘functionally complete’.

The above work on induction relies on the categorical account of logical predicates for simply typed theories developed in [Her93]. Such account is based on a characterization of adjunctions between fibrations which yields logical predicates for the several type-constructors in a uniform fashion.

5.3.2.2 Logic of infinite objects

Mendler [Men91] generalized a construction proposed by Hallnäs [Hal87] for constructing the largest bisimulation as the limit of an ω-chain and used by Lindström [Lin89] for representing non-well-founded sets in Martin-Löf’s type theory. Mendler’s observation that Σ (and all other basic type constructors of type theory) preserves ω-limit is based on working in a categorical model of extensional type theory, which makes use of Seely’s equivalence between the category of families of types in a certain context and the slice category with respect to that context.

Since the presently used version of type theory is intensional we proposed in the workplan to try to investigate how Mendler’s construction to be done inside this theory. However, recently Martin Hofmann [Hof93] has shown how to interpret extensional type theory in intensional type theory. This work is also formulated in terms of categorical model notions for type theory. As a consequence it seems preferable to factor Mendler’s construction, which makes use of extensionality, via Hofmann’s interpretation. In [Dyb94c] we give a direct type-theoretic proof of a slightly stronger result than Mendler’s: that coinductive types can be interpreted in (any model of) Martin-Löf type theory extended with an extensionality rule.

The paper [Coq94] presents a possible representation of infinite objects in type theory quite close to the one used in lazy functional programming languages. It contains also a direct inductive description of the kernel of an operator (based on an idea of Hallnäs).

Peter Aczel has described the final universe approach to the characterisation of semantic universes and illustrated it by giving characterisations of the universes of CCS and CSP processes [Acz94].

5.3.2.3 Logic of recursive types in functional languages

There has been further work by Pitts on proof principles for recursive types in functional languages described in last year’s progress report. [Pit93a] presents a definitive account of work on recursive domains begun during the previous year (preliminary accounts of which appeared in [Pit93b, Pit94b]). Working within a general, category-theoretic framework for various notions of ‘relation’ on domains and for actions of domain constructors on relations, Freyd’s analysis of recursive types in terms of a property of mixed initiality/finality is transferred to a corresponding property of invariant relations. The existence of invariant relations is proved under completeness assumptions about the notion of relation. It is shown how this leads to simpler proofs of the computational adequacy of denotational semantics for functional programming languages with user-declared datatypes. The initiality/finality property of invariant relations is specialized to yield an induction principle for admissible subsets of recursively defined domains, generalizing the principle of structural induction for inductively defined sets. The initiality/finality property gives rise to the co-induction principle studied in [Pit94a] and [Fio93].

Another application of categorical ideas in the context of recursive types in functional languages has been studied by Meijer and Hutton. This work concerns Bird and Meertens’ calculus for deriving functional programs from specifications. In recent years this calculus has been generalised from simple lists to arbitrary tree-like recursive datatypes, by using the categorical idea of modeling datatypes as fixed points of functors. This approach permits recursion operators like map, fold and unfold to be uniformly generalised from lists to other recursive datatypes. In [MH94] it is shown how, by exploiting constructor classes (which permit abstraction over type-forming operators in datatype declarations), such generic recursion operators can be implemented directly in a reallife functional programming language. Previously, the general theory had to be instantiated by hand for each datatype. Moreover, using Freyds recent work on algebraically compact categories, the recursion operators are extended from tree-like datatypes to datatypes which can also involve arbitrary uses of function-spaces.

5.3.3 Future plans

As part of a more general work on the category theory underlying the semantics of programming languages, John Power and Edmund Robinson will be investigating the categorical properties of a form of inductive types with respect to various evaluation strategies. This work forms part of a collaboration between CLICS-II and the ESPRIT BRA TYPES.

Thorsten Altenkirch and Peter Dybjer are continuing their work on simultaneous inductionrecursion, internal model constructions and reduction-free normalization proofs.

5.3.4 References and selected publications

[Acz94] Peter Aczel. Final universes of processes. Preprint: Dept. of Computer Science, Univesity of Manchester, 1994.

[AH94] Thorsten Altenkirch and Martin Hofmann. Reduction free normalization and categorical glueing. Manuscript, September 1994.

[Alt94a] Thorsten Altenkirch. Consistency in ALF. In La Wintermöte ’94, Lundsbrunn, January 1994.

[Alt94b] Thorsten Altenkirch. Reduction free normalization. Seminar given in Cambridge, July 1994.

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

[CD93] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen, 1993.

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

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

[Cur] Pierre-Louis Curien. Substitution up to isomorphism.

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

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

[Dyb94b] Peter Dybjer. Inductive families. Formal Aspects of Computing, 1994. To appear.

[Dyb94c] Peter Dybjer. On the interpretation of coinductive types in intuitionistic type theory. Manuscript, September 1994.

[Dyb94d] Peter Dybjer. On the syntax of dependent types and the coherence problem. Manuscript, September 1994.

[Fio93] M. Fiore. A coinduction principle for recursive datatypes based on bisimulation. In 8th Annual Symposium on Logic in Computer Science, pages 110–119. IEEE Computer Society Press, Washington, 1993.

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

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

[Hof93] Martin Hofmann. Elimination of extensionality and quotient types in Martin-Löf’s type theory. Draft paper, May 1993.

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

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

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

[MH94] Erik Meijer and Graham Hutton. Fold and unfold simplified and extended (working title). Work in progress, Utrecht University and Chalmers University, 1994.

[Pit93a] A. M. Pitts. Relational properties of domains. Technical Report 321, Cambridge Univ. Computer Laboratory, December 1993. 37 pages.

[Pit93b] A. M. Pitts. Relational properties of recursively defined domains. In 8th Annual Symposium on Logic in Computer Science, pages 86–97. IEEE Computer Society Press, Washington, 1993. See PittsAM:relpd for an expanded and revised version of this extended abstract.

[Pit94a] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[Pit94b] A. M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., New Orleans, LA, USA, April 1993, volume 802 of Lecture Notes in Computer Science, pages 72–82. Springer-Verlag, Berlin, 1994.

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

5.4.1 Summary

This report describes work done during Year 2 on Topic D (Subtypes and polymorphism in higher order languages). The topic contributes to the project objectives in the areas of “Type Theory and Semantics of Programming Languages”. The work done address the key issue of “Unification of Formalisms”. The collaborating partners are CAIMENS, Genova, Manchester, and Sussex. It has involved the collaboration of Curien, Hilken, Robinson, Rosolini, and Rydeheard. The results reported here were presented at the following international conferences and workshops: Jumelage meeting on Typed Lambda Calculus, Roma (Italy), December 1993; Peripatetic Seminar on Sheaves and Logic, Sussex (GB), March 1994; 9th LICS Conference, Paris (France), July 1994. The publications which form the deliverables under this Topic are items [ACC93], [RR94], [HJ94], [HR94], and [HR93].

The proposed deliverables for Milestone 2 were: to develop a general theory of parametric models of polymorphism and to study models of subtyping within the same framework. The first deliverable have been essentially achieved in [ACC93] and [RR94]. The second deliverable has been completed but has not yet been presented in print.

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

5.4.2 Work completed

5.4.2.1 Parametric polymorphisms

Study was carried out on parametricity in polymorphism from both the syntactic and the semantic side.

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

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

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

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

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

B [figure] A_{p}

and an embedding of cartesian closed fibrations

A ^{⊂} A_{p}

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

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

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

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

Some initial investigations show that the model of [Has91] provides a categorical model which is parametric, and the model of coherence spaces of [Gir89] is “almost” parametric.

5.4.2.2 Models for subtyping

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

5.4.2.3 Higher order theories of classes and categorical models of computations

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

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

5.4.3 Future plans

More work is needed to test the power of the model construction for parametric polymorphism. We shall try to present the parametric “completions” of some of the known models although we must be aware of the problems generated by the very heavy presentations of these: in abstract it is no difficulty to speak of homomorphisms of graphs, but in specific cases it will be necessary to simplify the presentation. We expect this may lead to improved presentations of the known models by a better understanding of what structural properties are involved in their constructions.

It is necessary to complete the study of parametricity showing that the semantic construction can be adapted to generate models for the system R. First, we shall test with relations on PERs.

We shall continue work on the categorical structures determined by the work on higher order theories for classes trying to develop representation theorems as well.

5.4.4 References and selected publications

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

[FJP92] M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors. Procs. Symposium in Applications of Categories to Computer Science. Cambridge University Press, 1992.

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

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

[HJ94] C. Hermida and B. Jacobs. Fibrations with indeterminates: Contextual and functional completeness of polymorphic lambda calculi. Accepted for MSCS.

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

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

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

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

[Pho92] W. Phoa. Using fibrations to understand subtypes. In Fourman et al. [FJP92], pages 239–257.

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

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

5.5 Report on topics E and F: higher order modal program logics and monadic programming language semantics

5.5.1 Summary

This report describes work done during Year 2 on Topic E (higher order modal program logics) and on Topic F (monadic programming language semantics). It was decided to report on them jointly because of the high degree of interaction between the two topics. These topics contributes to the project objectives in the areas of “Semantics and Logics of Programming Languages” and “Domain Theory”. The work done address the key issue of “Unification of Formalisms”. It has involved the collaboration of Moggi and Rosolini in Genova, Crole at Imperial, Robinson in Sussex, and Paiva, Pitts, Ritter and Stark in Cambridge. The results reported here were presented at the following international conferences and workshops: Canadian Math. Society Winter Meeting, Ottawa (Canada), December 1993; Jumelage meeting on Typed Lambda Calculus, Roma (Italy), December 1993; IFIP WG 2.2, San Miniato (Italy), June 1994; 9th LICS Conference, Paris (France), July 1994; Theory and Formal Methods Workshop, Cambridge, September 1994. The publications which form the deliverables under this Topic are items [Mog94a], [Mog94b], [Rob94a], [Rob94b], [Pit93], [Pit94b], [Sta], and [CG].

The proposed deliverables for Milestone 2 were:

(i) to find sound and complete axiomatizations for the semantics of necessity in Evaluation Logic;

(ii) to incorporate proof principles for inductive and co-inductive types developed by Pitts into Evaluation Logic;

(iii) to experiment with interpreting other program logics in Evaluation Logic;

(iv) develop a monadic semantics for a fragment of Standard ML with higher order function types, recursive datatypes and reference types, and prove computational adequacy;

(v) develop a game semantics for dynamic allocation.

Items (i) and (ii) have been indirectly achieved through the work on general semantics for Evaluation Logic. For item (iii) we have found a very simple interpretation of V T LoE in Evaluation Logic, which overcomes the intensionality problems in [HMSTar]; we expect to find equally simple interpretations for Hoare logic and the modal μ-calculus. For item (iv) we have constructed a monadic semantics via a suitable notion of ‘applicative bisimulation’; this side-steps some of the domain-theoretic difficulties (see below) in favour of a term-model construction based upon operational methods. It was intended that item (v) would draw upon the work being done in project Topics A and G. However that work has taken longer than expected to write up and as a result it has not been possible to investigate applications of it to Topics E and F.

CLICS-II meeting in Paris. During the three day meeting (28-30/06/94) several issues related to monad-based semantics and Evaluation Logic were addressed:

• The possibility of extending the representation of V T LoE (Variable Typed Logic of Effects) into Evaluation Logic to other program logics.

• The difficulties to incorporate in Evaluation Logic relational principles for reasoning about local state, such as those suggested by Tennent/O’Hearn (see [OT93]) and Pitts/Stark (see [PS93]).

• The difficulties in finding good monads for the store calculus caused by the mutual recursion definition of the monad and the domain of storable values, and by the need to take quotients to obtain more fully abstract models.

• The kind of results needed from Synthetic Domain Theory to satisfy the requirements coming from Evaluation Logic and Denotational Semantics.

5.5.2 Work completed

5.5.2.1 General semantics for Evaluation Logic

We have now a general semantics for Evaluation Logic, which drops all additional requirements on monads (see [Mog94a]). Formally, Evaluation Logic can be seen as a definitional extension of higher order predicate logic with dependent types and computational types, i.e. the evaluation modalities and evaluation predicate are definable and axioms for them can be proved sound formally (without referring to the categorical semantics).

Semantically, we need to consider quasi-toposes equipped with a fibred monad (to interpret computational types). From the point of view of Denotational Semantics the main issue is how categories of predomains (such as the category of cpos) should relate to an ambient category (such as a quasi-topos). This issue has been investigated in the setting of Synthetic Domain Theory (see [Hyl91, Tay91]): the category of predomains must form a full reflective sub-fibration of the ambient category.

A model which fits these requirements (and also those for interpreting polymorphic languages) is the quasi-topos of ω-sets with the full reflective sub-fibration of complete extensional PERs (see [FMRS90]). In this model fibred endofunctors have a simple alternative characterization: they correspond to endofunctors realizable by a Turing machine.

Towards LCF ++. The model of Synthetic Domain Theory based on complete extensional PERs suggests a powerful program logic, which could be called LCF ++, obtained by combining an expressive logical framework (such as the Extended Calculus of Constructions) with Axiomatic Domain Theory (as proposed by Freyd) and the Monadic Approach. There is a canonical interpretation of Extended Calculus of Constructions in any quasi-topos, in particular in ω-sets:

• a context Γ is interpreted by an ω-set Ī;

• a type Γ ⊢ τ : T ype is interpreted by an I-indexed family X̄ = (X̄_{i}|i ∈ I) of ω-sets;

• a term Γ ⊢ e : τ is interpreted by a realizable I-indexed family x = (x_{i} ∈ X̄_{i}|i ∈ I);

• the type P rop ∈ T ype of propositions is interpreted by the strong subobject classifier Δ2.

We have not come up with a precise definition of LCF ++, yet. Anyway, as a first approximation it could be presented on top of the Extended Calculus of Constructions as follows (where we indicate also the intended interpretation in the ω-set model):

• A collection Dom ⊂ T ype of predomains, interpreted by the set ExP of complete extensional PERs, which forms a (small) full reflective sub-category;

• A dominance 1_{⊥} ⊂ P rop, interpreted by the r.e.-subobject classifier Σ, s.t. the partial map classifier monad ( )_{⊥} satisfies the following properties:

– ( )_{⊥} maps predomains to predomains,

– every predomain has at most one ( )_{⊥}-algebra structure,

– the Kleisli category Dom_{⊥} is a model of ‘Axiomatic Domain Theory’.

The main unresolved issue is how much to ask for in an Axiomatic Domain Theory without loosing interesting models.

• A monad T which maps predomains to domains, i.e. predomains with ( )_{⊥}-algebra structure.

LCF ++ can provide a common platform for representing program logics, developing the modular approach (to programming languages and program logics) and formulating proof principles for inductive and co-inductive types.

LCF ++ and the modular approach. An important workbench for deciding what axioms should be incorporated in LCF ++ is provided by the modular approach to the specification of programming languages (see [CM93]).

Previous work on the modular approach has identified two polymorphic operations associated to the monad transformer F_{res}T X = μX′.T (X + X′) for adding resumptions (in what follows T′ stand for F_{res}T):

• τ : Πs : Dom.T′s ⇒ T′s and

• C : Πs, t : Dom.(s ⇒ T′t), (T′s ⇒ T′t), T′s ⇒ T′t.

Intuitively, τ(c) is like prefixing the program c with an internal action, while C(f, g, c) is like caseanalysis on the first step of c. In order to prove that T′ is a monad, i.e. there are polymorphic operations val′ : Πs : Dom.s ⇒ T′s and let′ : Πs, t : Dom.(s ⇒ T′t), T′s ⇒ T′t satisfying three equational axioms, it suffices to know that T′X is the initial algebra for the endofunctor T (X + ). This property of T′X suffices also to prove that τ and C satisfy the following properties:

• C(f_{2}, g_{2}, C(f_{1}, g_{1}, c)) = C(lx.C(f_{2}, g_{2}, f_{1}x), lc′.C(f_{2}, g_{2}, f_{2}c′)) ,

C(f, g, val′(x)) = fx and C(f, g, τ(c)) = gc

• existence and uniqueness of f′ : T′s ⇒ T′t s.t. C(f, f′; g) = f′ ,

C(val′, τ, c) = c and (f′ = C(f, f′; τ) iff f′ = let′(f)

But when one wants to use the associated operations τ and C for defining programming language operations (e.g. parallel composition) and deriving formally their properties (e.g. commutativity and associativity of parallel composition), it is essential to have also a fixed point operator Y. When the Kleisli Dom_{⊥} is algebraic compact, there exists a unique uniform fixed point operator. However, it seems that additional properties of Y are needed (which are not derivable from algebraic compactness) to have simple proof techniques. We are currently investigating what additional properties of Y would be convenient to have, for instance:

• Y (⟨f_{1}, f_{2}⟩) = ⟨a, fa⟩ (Bekič), where fx_{1} = Y (λx_{2}.f_{2}(x_{1}, x_{2})) and a = Y (λx_{1}.f_{1}(x_{1}, f′x_{1}));

• strong fixed point induction (∀n : N.ϕ(f^{n}⊥)) ⊃ ϕ(Y f), where ϕ is a regular subobject.

5.5.2.2 Representing program logics in Evaluation Logic

Variable Typed Logic of Effects V T LoE is a program logic proposed in [HMSTar] for reasoning about programs written in λ_{mk}, a call-by-value λ-calculus with references (basically the untyped counterpart of the store calculus). V T LoE is the latest product of an ongoing research effort (especially by Mason and Talcott) in finding powerful reasoning principles for languages with destructive memory operations. The axioms (and reasoning principles) of V T LoE are proved sound w.r.t. a satisfaction relation defined in terms of the operational semantics, and they are powerful enough to prove all test cases proposed in [MS88].

[Mog94b] gives a simple way of representing the contextual assertions of V T LoE into Evaluation Logic. The basic idea is to translate a contextual assertion ϕ, say with one free variable, into a predicate ϕ^{∗} over T V, where V is the type of values for λ_{mk}. This representation validates all logical axioms of V T LoE and avoids the intensionality problem present in [HMSTar], i.e. failure of the substitutivity rule

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

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

Representing other program logics. We have started looking at ways of representing other program logics in Evaluation Logic, by analogy with V T LoE. This seems feasible for Hoare logic and the modal μ-calculus (where formulas are interpreted by sets of states in a labelled transition system).

• Hoare logic. When the monad T is equipped with state operations lkp : T S of lookup and upd : S → T 1 of update, there are four plausible ways of translating a triple {ϕ_{1}}e{ϕ_{2}} (where ϕ_{i} are predicates over S and e ∈ T 1) into Evaluation Logic:

1. ∀s : S.ϕ_{1}(s) ⊃ [s′⇐upd(s); e; lkp]ϕ_{2}(s′)

2. ∀c : T 1.([s⇐c; lkp]ϕ_{1}(s)) ⊃ [s′⇐c; e; lkp]ϕ_{2}(s′)

3. ∀c : T 1.[(s, s′)⇐let s⇐c; lkp in (let s′⇐e; lkp in [(s, s′)])](ϕ_{1}(s) ⊃ ϕ_{2}(s′))

4. [(s, s′)⇐let s⇐lkp in (let s′⇐e; lkp in [(s, s′)])](ϕ_{1}(s) ⊃ ϕ_{2}(s′))

They all agree, when T is the state monad T X = (X × S)^{S}, but it is not clear which one scales up best w.r.t. modifications of T.

• Modal μ-calculus. In this case, it seems that the only change to the translation of V T LoE needed for accommodating the necessity modalities [a]ϕ of the modal μ-calculus is to make more explicit the structure of computational types, e.g. by saying that T X is of the form T′(X + (A × T X)) for some simpler computational monad T′.

On the other hand, it seems that the temporal μ-calculus (where formulas are interpreted by sets of runs) is unlikely to admit a simple representation into Evaluation Logic.

5.5.2.3 Monadic semantics of dynamically allocated local state

As a test of the general methods for program semantics and program logics being developed in this project, we have applied them to study increasingly more complicated fragments of Standard ML involving dynamically allocated local state (ML’s ‘reference types’).

The nu-calculus. This is a simply typed language with higher-order total functions and dynamically created names (which behave like references to the unit value in ML). Continuing work on the nu-calculus earlier in the project, [Sta] investigates monad-based denotational semantics for the nu-calculus. This is formalized in a suitable computational metalanguage, which distinguishes in the type system between values and computations. The general requirements for a categorical model of the metalanguage are presented and two specific examples described in detail. One is based on a simple category of set-valued functors, whilst the second, more refined model makes use of certain kinds of logical relation (drawing upon the work of Tennent and O’Hearn [OT93] and the operationally-based work in [PS93]). Both models provide computationally adequate semantics for the nu-calculus and so can be used to reason about observational equivalence in the language. The second model is shown to be fully abstract for first-order expressions.

Dynamic allocation monads. To extension of the work on the nu-calculus to more complicated fragments of ML with dynamically allocated storage for higher order functions dramatically complicates the construction of suitable monads. One reason is because their construction involves solving complicated, mixed-variance domain equations. Here [Pit93, Pit94b] provides useful techniques for dealing with such domains, and particularly for constructing various logical relations on the domains needed for computational adequacy and arguments involving representation independence of local store.

However, there is a further problem with generalizing the set-based monads for the nu-calculus constructed in [Sta] to domain-based monads for dynamic allocation of local store. All but the simplest monads involve taking quotients by equivalence relations in their construction and such quotients in categories of domains are difficult to deal with (because they involve completion constructions). As we describe next, for the moment we have side-stepped these difficulties in denotational semantics by considering term-models defined directly from the operational semantics.

Applicative bisimilarity for languages with state. Since Milner and Park’s work on CCS, co-inductively defined notions of program equivalence are common in the study of concurrent processes. Abramsky and Ong’s work on the lazy lambda calculus, work of the Cornell school (Allen, Howe, Smith) on the semantics of NuPrl, and Andrew Gordon’s PhD thesis [Gor92] show that such a co-inductive notion of program equivalence, called by Abramsky applicative bisimilarity, can be developed for functional programming languages. As a consequence of Howe’s general congruence result such notions of applicative bisimilarity are sound for establishing Morris-style contextual equivalence of programs. For deterministic, pure functional languages one usually has that the two notions of equivalence coincide. This co-incidence has been termed by Bloom the property of operational extensionality of a language and should be regarded as the proper generalization of Milner’s technically important ‘Context Lemma’ for PCF.

We have extended the notion of applicative bisimilarity to the case of ‘impure’ functional languages, i.e. ones with state-based features such as references. The definition was developed by a process of transfer from domain theory: by looking at the recursive domains involved in a denotational semantics of the language, a definition of applicative bisimilarity can be read off from the co-inductive characterization of equality on recursively defined domains established in [Pit94a, Pit93]. The key property of congruence for this notion of applicative bisimilarity has been established via a (non-trivial) adaptation of Howe’s method for pure functional languages. As a result, this applicative bisimilarity provides a sound method for proving observational equivalence of programs with state. In the case of global storage locations and for block-structured languages (such as idealized Algol) it provides a complete method, i.e. we can prove operational extensionality. However, our previous work on the nu-calculus can be adapted to show that, interestingly (or unfortunately, depending upon one’s attitude!), operational extensionality fails for the case of locally-declared storage locations. Indeed, in this case we have at least two congruent notions of applicative bisimulation, one closer to observational equivalence than the other. (The two notions correspond closely to two dynamic allocation monads considered in our work on the nu-calculus.)

We are using this work on applicative bisimulation to give a semantics to our target fragment of SML with recursive and reference types, as follows. First we have defined a suitable computational metalanguage, called the Monadic Store Calculus, and given it an operational semantics in terms of an inductively defined evaluation relation. From this we define a congruent notion of applicative bisimilarity as discussed above. The closed terms of the Monadic Store Calculus quotiented by applicative bisimilarity comprise our model. One advantage of the monadic approach is seen in the fact that up to bisimilarity, product, function, and recursive types satisfy familiar equational and categorical properties properties (e.g. βη-conversion and surjective pairing hold); in other words the complications in the theory due to the presence of non-termination and side-effects are encapsulated in the computation types. We give a compositional (call-by-value) translation of the target fragment of SML into the model and prove that bisimilarity of translated programs implies observational equivalence between the programs.

An account of this work involving applicative bisimilarity is in preparation [dPS, PR]

A sound metalogical semantics for input/output effects. Crole and Gordon [CG] have studied the long standing problem of semantics for input/output using side-effects. Their vehicle is a small higher-order imperative language O, with operations for interactive character I/O and based on Standard ML syntax. Unlike previous theories, they present both operational and denotational semantics for I/O effects. They use a novel labelled transition system that uniformly expresses both applicative and imperative computation. They make a standard definition of bisimilarity and prove it is a congruence using Howe’s method.

Next, they define a metalogical type theory M in which one may give a denotational semantics to O. M is monadic, and generalizes Crole and Pitts’ FIX-logic [CP92] by adding in a parameterized recursive datatype, which is used to model I/O. M comes equipped with both judgements of equality of terms and an operational semantics; M itself is given a domain-theoretic semantics in the category CPPO of cppos (bottom pointed posets with joins of ω-chains) and Scott continuous functions. They use the CPPO semantics to prove that the equational theory is computationally adequate for the operational semantics, making use of certain ‘formal approximation’ relations in the proof. The construction of such relations uses key ideas from [Pit93].

A monadic-style compositional translation of O into M induces a denotational semantics on O. The final result of [CG] justifies metalogical reasoning: if the denotations of two O programs are equal in M then the O programs are in fact operationally equivalent.

5.5.3 Future plans

According to the Technical Annex work on topic E was expected to finish in year 2. Indeed, the semantics of Evaluation Logic has now reached a satisfactory state, which does not require further work. However, more work is needed under Topic F for testing the usability of Evaluation Logic and for blending it in a coherent way with other strands of the project. In year 3 we intend to pursue the following research:

• To continue the work on representing program logics into Evaluation logic. More specifically, we expect to obtain representation results for Hoare logic and the modal μ-calculus similar to those achieved for V T LoE.

• To work towards LCF ++ by blending contributions from topics B, C, E, and F. It is now clear what additional properties a model of Synthetic Domain Theory must have to interpret Evaluation Logic. Therefore, we will investigate ways of turning categories of domains used in Denotational Semantics into models of Synthetic Domain Theory, that validate additional properties of the fixed point operator Y and are also suitable for Evaluation Logic.

• To investigate whether the model of the Monadic Store Calculus based upon applicative bisimilarity can be extended to interpret Evaluation Logic and how useful this is for proving properties of SML programs. The operational approach has built into it powerful co-inductive and relational invariance properties that involve the program state explicitly. At the moment we do not see how to formulate analogous principles in a modal Evaluation Logic, which describes program state only implicitly.

5.5.4 References and selected publications

[CG] Roy L. Crole and Andrew D. Gordon. A sound metalogical semantics for input/output effects. In Computer Science Logic’94, Kazimierz, Poland, September 26–30, 1994. Proceedings to appear in Springer LNCS.

[CM93] P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In CTCS 1993, 1993. CWI Tech. Report.

[CP92] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations: Fixhyperdoctrines and the fix-logic. Information and Computation, 98:171–210, 1992.

[dPS] V. de Paiva, A. M. Pitts, and I. D. B. Stark. A monadic store calculus. In preparation.

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

[Gor92] A. D. Gordon. Functional Programming and Input/Output. PhD thesis, Cambridge Univ., 1992. To appear in Distinguished Dissertations in Computer Science series, Cambridge University Press.

[HMSTar] F. Honsell, I.A. Mason, S.F. Smith, and C. Talcott. A variable typed logic of effects. Information and Computation, to appear.

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

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

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

[MS88] A.R. Meyer and K. Sieber. Towards fully abstract semantics for local variables: preliminary report. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 191–203, January 1988.

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

[Pit93] A. M. Pitts. Relational properties of domains. Technical Report 321, Cambridge Univ. Computer Laboratory, December 1993. 37 pages.

[Pit94a] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[Pit94b] A. M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., New Orleans, LA, USA, April 1993, volume 802 of Lecture Notes in Computer Science, pages 72–82. Springer-Verlag, Berlin, 1994.

[PR] A. M. Pitts and E. Ritter. A fully abstract translation between a lambda calculus with reference types and a fragment of Standard ML. In preparation.

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

[Rob94a] E.P. Robinson. A note on the presentation of enriched monads. available by ftp from

theory.doc.ic.ac.uk, August 1994.

[Rob94b] E.P. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Computer Science Technical Report 6/94, University of Sussex, April 1994. (submitted to Mathematical Structures in Computer Science).

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

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

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

5.6 Report on topic H: Computational Content of Classical Proofs

5.6.1 Summary

This report describes work done during Year 2 on Topic H (computational content of classical proofs). This topic contributes to the project objectives in the areas of “Type Theory” and “Semantics and Logics of Programming Languages”. It has involved the collaboration of Coquand in Chalmers, and Hugo Herbelin in Paris. Coquand had email exchanges with Abramsky in Imperial College. Some results (in point-free topology) will appear in the Journal of Pure and Applied Algebra and Journal of Symbolic Logic. Some results of Herbelin will be presented at the next Computer Science Logic in Warsaw, september 94. The publications which form the deliverables under this Topic are items [Coq93], [Coq94a] and [Coq94b].

For the work in point-free topology, we have found a formal space, that can be described using only inductive definitions, such that it is possible to build a non-principal ultrafilter in the topos of sheaves over this space. This gives a way to extract a computational content of any proof that uses a non-principal ultrafilter.

For the computational content of classical logic, progress have been made in two directions. First, using heuristically the previous game-theoretical interpretation of proofs, we have given a realizability interpretation of the negative translation of the axiom of choice. Secondly, Hugo Herbelin has precised the connection between the game-theoretical analysis presented in [Coq93] and the work of Felsher [Fel85]. This will appear in Hugo Herbelin’s forthcoming Ph. D. thesis.

5.6.2 Work completed

5.6.2.1 Point-Free Topology

The plan was to analyze the space of non-principal ultrafilters. The hope was that we may learn about impredicativity from such an analysis because, classically, this space has a large cardinality 2^{(2^{ℵ_{0}} )}. Also, it is not clear a priori how to give a formal representation of this space.

We have found that it is possible to describe inductively a boolean algebra and a covering operator over this algebra such that the formal space defined by this operator has the following property: there exists a non-principal ultrafilter in the topos of sheaves over this space. This space is furthermore (in some sense to be precised), the “minimal one” with this property. This gives a systematic way of extracting computational content from any proof that uses a non-principal ultrafilter. We give an example in the note [Coq94c] (proof of Ramsey’s theorem using one nonprincipal ultrafilter).

5.6.2.2 Game Semantics of Proofs

The first result is an heuristic application of the game-theoretic analysis of proofs. It suggests a natural strategy for interpreting the axiom of choice over natural numbers [Coq94a]. While it is yet difficult to analyse directly this interpretation, it has been possible to use it for writing a realizability interpretation of the negative interpretation of the axiom of choice, with a (classical) proof of termination. This result constitutes an improvement of C. Murthy’s work [Mur90], and is somewhat surprising because C. Murthy presented arguments, essentially the fact that the negative interpretation of the axiom of choice contradicts Church’s thesis, which seemed to imply that such a realization was impossible.

The second result has been a clarification of the connection between the work of [Coq93] and [Fel85] by Hugo Herbelin. This analysis will soon appear in his Ph. D. thesis, to be defended next October or November. Hugo Herbelin gives a sequent calculus whose cut-free proofs are in 1-1 correspondence with the E-strategy of Felsher. General strategies, and cut-elimination can then be interpreted as for the previous work [Coq93]. It seems very likely that a similar analysis works for the various game interpretations of PCF. Hugo Herbelin has also presented a system of proof terms for a natural restriction of the sequent calculus LJ [Her94], and gives a proof of strong normalisation for this system.

5.6.3 Future plans

The work on game theoretical interpretation of classical arithmetic should be connected to the work on game interpretation for processes and analysis of sequentiality at higher type done in Cambridge and Imperial College. We think that Hugo Herbelin’s analysis applies to such interpretation.

Also, it will be nice to use this work to give a more direct computational interpretation of proofs in classical analysis with the Axiom of Choice. It is very tempting to look at this computation as a collection of entities that are “conjecturing laws” and try to refine these laws when they discover that they have made a mistake. Thought in this way, the realizability interpretation that we give in [Coq94a] is inefficient because the different entities (lemmas) may forget too much about their previous conjectures. It will be interesting to formalize these intuitive descriptions.

One other direction is to relate the work [Coq94a] to works on sequential algorithms, that seem to constitute a natural framework in which to express this realization of the Axiom of Choice. Here, we hope to use the work of Lamarche and Curien relating games and sequential algorithms. The general idea will be to describe directly in term of sequential algorithms a monad ∇(X) that can be thought of as interpretation of the double negation of X.

5.6.4 References and selected publications

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

[Coq94a] S. Berardi, M. Bezem and Th. Coquand. On the computational content of the Axiom of Choice. technical report n 116 of the university of Utrecht, 1994.

[Coq94b] Th. Coquand. A constructive topological proof of Van der Waerden’s theorem. To appear in the Journal of Pure and Applied Algebra, 1994.

[Coq94c] Th. Coquand. A Formal Space of Ultrafilters. draft paper, August 1994.

[Coq94d] Th. Coquand and H. Herbelin. Some remarks on Novikov’s calculus. draft paper, March 1994.

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

[Her94] H. Herbelin. A lambda-calculus structure isomorphic to sequent calculus structure. paper accepted to Computer Science Logic, september 1994

[Mur90] Ch. Murthy. Extracting Constructive Content from Classical Proofs. Ph. D. Thesis, Cornell, 1990

5.7 Report on topic I: Symbolic Computation

5.7.1 Summary

This report describes work done during Year 2 on Topic I (symbolic computation).

In Marseilles, a new PhD student, Anne Massol, has started to work with Yves Lafont on this project in November 1993. She is implementing tools for manipulating Penrose diagrams.

The publication which form the deliverables under this Topic are [lafont93] and [lafont94b].

5.7.2 Work completed

Many interesting case of symbolic calculus can be presented with planar diagrams called Penrose diagrams. This presentation is easier and quicker to understand than equational terms. But manipulating and drawing diagrams by hand is not very easy. So, this presentation implies the need of computer for computing normal forms (automated reasoning), drawing, editing and manipulating diagrams (interactive reasoning). Anne massol is developing a software (with the functional programming language CAML) for this purpose. she has already implemented the internal representation of diagrams, algorithms such as the computation of normal forms, the automated drawing and the editing (figures 5.1 and 5.1).

Figure 5.1: editing an equation

5.7.3 Future plans

Yves Lafont will present a general theory of rewriting Penrose diagrams, which will be a generalization of word rewriting. The software developed by Anne Massol will include algorithms for testing the confluence of such rewriting systems and also the interactive tools for manipulating diagrams.

CHAPTER 5. DELIVERABLES 53 Figure 5.2: applying equations

5.7.4 References and selected publications

[lafont93] Y. Lafont, A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier) to appear in Journal of Pure and Applied Algebra (North Holland)

[lafont94b] Y. Lafont, Equational Reasoning with 2-dimensional Diagrams, to appear in the proceedings of a summer school on rewriting (Font-Romeu 93, LNCS, Springer-verlag)

Appendix A

A.1 Report on the CLICS meeting in Paris

The meeting was held from June 28 to July 1 at the Ecole Normal Supérieure, Paris. There were 51 participants: 39 came from all the sites contributing to the project, 12 were researchers external to the project. Thomas Ehrhard and Antonio Bucciarelli were in charge of the local arrangements. The program of the scientific sessions was prepared by S.Abramsky, M.Hyland, A.Pitts and P.Rosolini.

The meeting consisted of three scientific sessions (each spanning a day) on specific topics: Dynamic Allocation, Game Semantics, and Synthetic Domain Theory. We invited five prominent researchers in the areas: Simon Peyton-Jones, Peter Freyd, Thomas Streicher, Kurt Sieber, and Dana Scott. At the end of the meeting, there was a briefing session on the status of the project (Thierry Coquand and Yves Lafont were not able to attend the meeting because of other engagements), followed by a discussion on “what to do next”.

Some of the scientific sessions had in-depth presentations (including detailed proofs) and technical discussions. The aim was to provide a “tutorial” on hot subjects relevant to several topics, and to discuss further research. The topics of the scientific sessions were chosen for different reasons (see below). All the scientific sessions provided new directions and problems in the subject treated. As a whole, the meeting has been very valuable for the project.

Dynamic Allocation. The semantics of dynamic allocation and local state is a very challenging problem, and one of those which attracts a large part of very good research in theoretical computer science. Andy Pitts and Ian Stark gave detailed accounts of the work done in Cambridge on this subject. They explained the difficulties encountered in following a monadic approach, and what can be done in a more operational setting. Moreover, it was observed that there are difficulties in applying standard techniques to solve recursive domain equations involving some of the monads for local state. Kurt Sieber reported on the latest achievements in the semantics of ALGOL-like languages using logical relations. Simon Peyton-Jones showed some intriguing use of monads to provide local state in a pure functional language. His contribution was particularly useful to clarify the different points of view.

Game Semantics. Due to the importance of the result, it was felt necessary to understand as thoroughly as possible the constructions of game models for the full abstraction problem of PCF. Therefore in the session on Game Semantics Samson Abramsky and Pasquale Malacaria took as much time as needed to present their work in reasonable details, while Martin Hyland proposed a general way for obtaining extensional models (of PCF) from intensional ones.

During the discussion emerged the need to investigate whether categories of games may provide a better basis for denotational semantics than the usual categories of domains. Moreover, it was felt that even the more intensional categories may have interesting uses in denotational semantics, e.g. to model program complexity. There remains a mathematical challenge to make precise the connections with other constructions of the fully abstract model.

Synthetic Domain Theory. Synthetic domain theory remained quiet for a while after a quick powerful start as a unifying theory for denotational semantics, so the scientific session was designed as a “general summit” of all the researchers in the field to join forces and to determine which new problems should be addressed. Some talks reviewed the basic results and formalisations of Synthetic Domain Theory suggesting possible extensions. Others presented questions to Synthetic Domain Theory or problems in the standard theory of domains which researchers in Synthetic Domain Theory should aim to tackle. For instance, in the talk by Martin Hyland the basic theory was presented in a revised form so as to suggest that there may be different “flavours” of the theory to fit in notions of stability or sequentiality. Some other talks addressed the powerful possibilities of the theory. For instance, in his talk Eugenio Moggi pointed out some useful opportunities that a “reasonable” category of domains which embeds fully into a topos would provide.

At the discussion a few firm points reached in the subject were agreed upon, and new directions were determined. It was clear that there was a large interest on the development of the subject, but dissemination of knowledge in this case seems crucial. It was recalled that the main intent of the theory was to be simple and applicable to many situations. This must be re-established by giving a thorough presentation of the basics of the theory and introducing as many “pet examples” as possible.

Topics Briefing and Planing. At the briefing session, the topic leaders addressed the group about the recent results in each topic and proposed possible goals for the third year. There was also a discussion on the IV Framework document, and various other matters of general interest were discussed at the Business Meeting, including: some complaints about the financial part of the project, the organization of the CLICS-TYPES joint workshop to be held at Chalmers, the Summer School in 1995 to be held in conjunction with the semester on “Semantics of Computation” at the Newton Institute at Cambridge.

Programme of the workshop

Dynamic Allocation Session

Tuesday 28 June organized by A.Pitts

9.00-9.10 Opening
9.10-10.40 I.Stark

Categorical semantics of dynamic allocation

10.40-11.10 Coffee
11.10-12.10 S.Peyton-Jones

Lazy Functional State Threads

12.10-13.00 E.Moggi

Representing VTLoE in Evaluation Logic

13.00-15.00 Lunch
15.00-16.00 K.Sieber

Full abstraction for the second order subset of an ALGOL-like language

16.00-17.00 R.Crole

Observational equivalence via generic adequacy

17.00-17.30 Tea
17.30-18.30 A.Pitts

Applicative bisimulation for dynamic storage locations Game-Semantics Session Wednesday 29 June

organized by S.Abramsky and M.Hyland

9.00-10.30 S.Abramsky

Introduction to game semantics

10.30-11.00 Coffee
11.00-12.00 P.Malacaria

Definability and intensional full abstraction

12.00-12.30 S.Abramsky

Extensional full abstraction

13.00-15.00 Lunch
15.00-15.45 I.Mackie

Games, paths, and geometry of implementation

15.45-16.30 M.Hyland

What is a model of PCF?

16.30-17.00 Tea
17.00-17.45 H.Nickau

TBA

17.45-19.00 Discussion (moderator E.Moggi)

Synthetic Domain Theory Session

Thursday 30 June organized by P.Rosolini and M.Hyland

9.00- 9.50 M.Hyland

Condensed categorical outline

10.00-10.25 T.Streicher

Formalizing elementary SDT

10.30-11.00 Coffee
11.00-11.50 A.Jung

Questions to SDT from the viewpoint of classical domain theory

12.00-12.25 E.Moggi

It would be nice if...

12.30-12.55 J.Longley

Is there a use for the internal logic?

13.00-15.00 Lunch
15.00-15.50 P.Freyd

TBA

16.00-16.25 E.Robinson

Monadicity in the enriched setting: some examples

16.30-17.00 Tea
17.00-17.50 P.Taylor

The Second Order Leibniz Principle

18.00-19.00 Discussion (moderator P.Rosolini)

Topics Briefing Session

Friday 1 July organized by E.Moggi

9.00-10.30 Topics B+E+F

M.Hyland, E.Moggi and A.Pitts

10.30-11.00 Coffee
11.00-11.30 Topic D

P.Rosolini

11.30-12.00 Topic C

P.Dybjer

12.00-13.00 Topics A+G

S.Abramsky and G.Winskel

13.00-15.00 Lunch
15.00-15.45 Discussion (moderator E.Moggi)
15.45-16.30 Business Meeting
16.30-17.00 Tea

List of participants

Samson Abramsky Imperial
Thorsten Altenkirch Chalmers
Daniela Archieri  Genova
Nick Benton  Cambridge
Gavin Bierman  Cambridge
Torben Brauner  Aarhus
Carolyn Brown  Sussex
Antonio Bucciarelli CAIMENS
Roberto Chinnici  Genova
Roy Crole  Imperial
Vincent Danos  Marseille
Paiva DeValeria  Cambridge
Peter Dybjer  Chalmers
Thomas Ehrhard  CAIMENS
Marcelo Fiore  Edinburgh
Peter Freyd  Philadelphia
Andrew Gordon  Cambridge
Edward Hæusler  Aarhus
Claudio Hermida  Aarhus
Barney Hilken  Cambridge
Michael Huth  Darmstadt
Martin Hyland  Cambridge
Achim Jung  Darmstadt
Klaus Keimel  Darmstadt
John Longley  Edinburgh
Ian Mackie  Imperial

Pasquale Malacaria Imperial
Guy McCusker  Imperial
Eugenio Moggi  Genova
Hanno Nickau  Siegen
Luke Ong  Cambridge
Dusko Pavlovic  Imperial
Simon Peyton-Jones Glasgow
Andrew Pitts  Cambridge
John Power  Edinburgh
Bernhard Reus  Munchen
Eike Ritter  Cambridge
Edmund Robinson Sussex
Giuseppe Rosolini Genova
Joshua Ross  Cambridge
David Rydeheard  Manchester
Andrea Schalk  Sussex
Dana Scott  CMU
Kurt Sieber  Saarbrücken
Alex Simpson  Edinburgh
Sergei Soloviev  Aarhus
Ian Stark  Cambridge
Thomas Streicher  Munchen
Paul Taylor  Imperial
Jaap Van Oosten  Aarhus
Glynn Winskel  Aarhus