Subject:     LICS'91 Program
Date: Wed, 3 Apr 91 00:47:53 EST
From: LICS.DATABASE@B.GP.CS.CMU.EDU

                     Sixth Annual IEEE Symposium on
                   LOGIC IN COMPUTER SCIENCE (LICS'91)
                July 15-18, 1991
        Vrije Universiteit, Amsterdam, The Netherlands

   Sponsored by the IEEETC on Mathematical Foundations of Computing; CWI
   Amsterdam; and the Vrije Universiteit, Amsterdam; in cooperation with the
   Association for Computing Machinery--SIGACT, the Association for Symbolic
   Logic, and the European Association for Theoretical Computer Science.


      Below is the Technical Program and Conference Events for LICS 91.
      Registration, hotel and travel information will be broadcasted
      within a few days.  If you expect to attend LICS 91, the organizers
      would be grateful if you would immediately email the following reply
      to   lics91@cwi.nl  ( *NOT* to the sender of the present message):
                 I HOPE TO ATTEND LICS 91 IN AMSTERDAM.
      In case price is a factor, note that early registration for authors and
      members of sponsoring organizations is expected to be about NLG 375
      ($215) including 6+ meals, and middle price single hotel room per night
      is about NLG 100 ($60).

             LICS '91 ADVANCE PROGRAM

CONFERENCE EVENTS
=================
SUNDAY WELCOME AND REGISTRATION.  On July 14 there will be a welcome
reception from 19:00 to 22:00, at the  Grand Caf'e Waterloo.
The Waterloo is on the Opera and City Hall complex, at Zwanenburgwal 15.

MONDAY RECEPTION AND INVITED LECTURE.  On July 15 there will be a
reception by the City Mayor and Aldermen in the  Stedelijk Museum,
from 18:00 to 19:30.  A light dinner buffet will be served.
Following the reception, N.G. de Bruijn will deliver an invited lecture
at the Lutheran Church historic building, from 20:00 to 21:00.

TUESDAY BUSINESS MEETING.  On July 16, following the scientific program,
a business meeting will take place at the Free University, from 17:30 till
about 19:00.

WEDNESDAY BANQUET.  A Conference Banquet will take place on July 17
at the Dutch Maritime Museum, preceded by an aperitif on board
the tallship  Amsterdam.


CONFERENCE PROGRAM
******************
All talks at the Vrije Universiteit main building's Aula

SUNDAY, July 14
---------------
WELCOME RECEPTION  (19:00--22:00)

MONDAY, July 15
---------------
SESSION 1.  9:30--10:45.  Chair: Giuseppe Longo (LIENS, Paris)
 9:30  A Foundational Delineation of Computational Feasibility,
    Daniel Leivant (Carnegie Mellon)
 9:55  Toward a Semantics for the QUEST Language,
    Fabio Alessi and Franco Barbanera (Turin)
10:20  Term Declaration Logic and Generalised Composita,
    Peter Aczel (Manchester)

SESSION 2.  11:15-12:55. Chair: Samson Abramsky (Imperial College)
11:15  Logic Programming in a Fragment of Intuitionistic Linear Logic,
    Joshua Hodas (U Penn) and Dale Miller (Edinburgh)
11:40  Games Semantics for Linear Logic,
    Yves Lafont (LIENS Paris) and Thomas Streicher (Passau)
12:05  Linearizing Intuitionistic Implication,
    Patrick Lincoln (Stanford), Andre Scedrov (U Penn),
    and Natarajan Shankar (SRI)
12:30  Some results on the Interpretation of Lambda Calculus in
       Operator Algebras,
    Pasquale Malacaria (Turin) and Laurent Regnier (Paris VII)

SESSION 3.  14:15-15:30. Chair: Val Breazu-Tannen (U Penn)
14:15  Unification and Anti-Unification in the Calculus of Constructions,
    Frank Pfenning (Carnegie Mellon)
14:40  Partial Objects in the Calculus of Constructions,
    Philippe Audebaud  (Bordeaux)
15:05  An Evaluation Semantics for Classical Proofs,
    Chetan Murthy (Cornell)

SESSION 4.  16:00-17:15.  Chair: Bernhard Steffen (Aachen)
16:00  A Theory of Testing for Real-Time,
    Rance Cleaveland (North Carolina State) and Amy Zwarico (Johns Hopkins)
16:25  Complexity Bounds of Hoare-style Proof Systems,
    Hardi Hungar (Oldenburg)
16:50  Semantics of Pointers, Referencing and Dereferencing
       with Intensional Logic,
    Hin-Kai Hung (AGS Information Services) and Jeffery Zucker (McMaster)

RECEPTION  (18:00-19:30) light dinner buffet (at the Stedelijk Museum)

EVENING LECTURE  (20:00-21:00)     N.G. de Bruijn:  Can People Think?
          (at the Lutheran Church historic building)

TUESDAY, July 16
----------------
SESSION 5.  9:30-10:45.  Chair: Pierre-Louis Curien (LIENS Paris)
 9:30  Sequentiality and Strong Stability,
    Antonio Bucciarelli (Pisa and LIENS Paris) and Thomas Ehrard (Paris 7)
 9:55  Parallel PCF has a Unique Extensional Model,
    Allen Stoughton (Sussex)
10:20  The Fixed Point Property in Synthetic Domain Theory,
    Paul Taylor (Imperial College)

SESSION 6.  11:15-12:55.  Chair: Robert Constable (Cornell)
11:15  INVITED TALK: Thierry Coquand (Goteborg)
12:05  On Computational Open-Endedness in Martin-Lof Type Theory,
    Douglas Howe (Cornell)
12:30  Predicative Type Universes and Primitive Recursion,
    Nax-Paul Mendler (Manchester)

SESSION 7.  14:15-15:30.  Chair: Simona Ronchi Della Rocca (Turin)
14:15  Freyd's Hierarchy of Combinator Monoids,
    Rick Statman (Carnegie Mellon)
14:40  Equational Programming in Lambda Calculus,
    Enrico Tronci (Carnegie Mellon)
15:05  An Inverse of the Evaluation Functional for Typed Lambda Calculus,
    Ulrich Berger and Helmut Schwichtenberg (U. of Munich)

SESSION 8.  16:00-17:15.  Chair: Serge Abiteboul (INRIA)
16:00  A Completeness Theorem for Kleene Algebras and the Algebra
       of Regular Events,
    Dexter Kozen (Cornell)
16:25  On First Order Database Query Languages,
    Arnon Avron and Joram Hirshfeld (Tel Aviv)
16:50  Specifying and Proving Serializability in Temporal Logic,
    Doron Peled and Shmuel Katz (Technion) and Amir Pnueli (Weizmann)

BUSINESS MEETING  (17:30-19:00)

WEDNESDAY, July 17
------------------
SESSION 9.  9:30-10:45.  Chair: Jan Bergstra (University of Amsterdam)
 9:30  CCS with Priority Choice,
    Juanito Camilleri (Cambridge) and Glynn Winskel (Aarhus)
 9:55  Rabin Measures and their applications to Fairness and Automata Theory,
    Nils Klarlund (IBM) and Dexter Kozen (Cornell)
10:20  Specification and Refinement of Probabilistic Processes,
    Bengt Jonsson (Swedish Inst. for CS) and Kim Larsen (Aalborg)

SESSION 10.  11:15-12:55.  Chair: Ehud Shapiro (Weizmann Inst.)
11:15  INVITED TALK:
    Jeff Paris (Manchester): Modelling Belief.
12:05  On the 0-1 Law for the Class of Existential Second-Order,
       Minimal Godel Sentences with Equality
    Leszek Pacholski and Wieslaw Szwast (IM PAN Wroclaw)
12:30  On the Deduction Rule and the Number of Proof Lines,
    Samuel Buss (UC San Diego) and Maria-Luisa Bonet (Berkeley)

SESSION 11.  14:15-15.55.  Chair: Krzysztof Apt (CWI Amsterdam)
14:15  Logic Programs as Types for Logic Programs,
    Thom Fruhwirth (Tech. U. Vienna), Ehud Shapiro (Weizmann),
    Moshe Vardi (IBM-Almaden), and Eyal Yardeni (Weizmann)
14:40  A First-Order Theory of Types and Polymorphism in Logic Programming,
    Michael Kifer and James Wu (Stony Brook)
15:05  Prop revisited: Propositional Formulas as Abstract Domain
       for Groundness Analysis,
    Agostino Cortesi (Padova), Gilberto File (Padova),
    and William Winsborough (Penn State)
15:30  Constructive Negation for Constraint Logic Programming,
    Peter Stuckey (Melbourne)

BANQUET  at the Maritime Museum

THURSDAY, July 18
-----------------
SESSION 12.  9:30-10:45.  Chair: Masahiko Sato (Tohoku)
 9:30  Higher-Order Critical Pairs,
    Tobias Nipkow (Cambridge)
 9:55  Executable Higher-Order Algebraic Specification,
    Jean-Pierre Jouannaud (Paris XI) and Mitsuhiro Okada (Concordia)
10:20  Defaults and Revision in Structured Theories,
    Mark Ryan (Imperial College)

SESSION 13.  11:15-12:55.  Chair: Ursula Goltz (GMD)
11:15  Actions Speak Louder than Words: Proving Bisimilarity for
       Context-Free Processes,
    Hans Huttel and Colin Stirling (Edinburgh)
11:40  On the Relationship between Process Algebra and Input/Output Automata,
    Frits Vaandrager (MIT)
12:05  A Compositional Proof System for Dynamic Process Creation,
    Frank de Boer (Eindhoven)
12:30  A Partial Approach to Model Checking,
    Patrice Godefroid and Pierre Wolper (Liege)

END OF CONFERENCE

CONFERENCE ORGANIZATION
=======================
LICS General Chair: Albert R. Meyer
1991 Conference Co-Chairs: Jan Willem Klop and Roel de Vrijer
1991 Program Chair: Gilles Kahn
Publicity Chair: Daniel Leivant
Local Organizers: Mieke Brune and Frans Snijders

PROGRAM COMMITTEE:
G. Kahn (chair), S. Abiteboul, S. Abramsky, K. Apt, J. Bergstra,
V. Breazu-Tannen, S. Buss, R. Constable, P.-L. Curien, N. Dershowitz,
P. Dybjer, U. Goltz, G. Longo, G. Mints, A. Pitts, S. Ronchi Della Rocca,
M. Sato, U. Shapiro, B. Steffen.

ORGANIZING COMMITTEE:
A. Meyer (chair), M. Abadi, J. Barwise, M. Blum, A. Chandra,
R. Constable (chair elect), E. Engeler, J. Gallier, J. Goguen,
Y. Gurevich, S. Hayashi, D. Johnson, G. Kahn, J.W. Klop, D. Kozen,
D. Leivant, Z. Manna, G. Mints, J. Mitchell, Y. Moschovakis,
R. Parikh, G. Plotkin, G. Rozenberg, D. Scott, J. Tiuryn, R. de Vrijer.

Subject:     LICS'91 Registration
Date: Mon, 8 Apr 91 23:49:29 EDT
From: LICS@B.GP.CS.CMU.EDU

                         LICS 91 REGISTRATION
                              AND PROGRAM

                     Sixth Annual IEEE Symposium on
                   LOGIC IN COMPUTER SCIENCE (LICS'91)
                            18, 1991
              Vrije Universiteit, Amsterdam, The Netherlands

   Sponsored by the IEEETC on Mathematical Foundations of Computing; CWI
   Amsterdam; and the Vrije Universiteit, Amsterdam; in cooperation with the
   Association for Computing Machinery--SIGACT, the Association for Symbolic
   Logic, and the European Association for Theoretical Computer Science.


(We apologize if you receive a bothersome number of copies
of LICS announcements. We are trying to coordinate our broadcasts
among the multiple mail lists and newsgroups reaching the LICS
community, but these efforts may not be effective for a while.)


GENERAL INFORMATION
===================
Register and reserve hotel rooms by sending the completed form below by
EMAIL to
      lics91@cwi.nl <LICS'91 Secretariat>
or by REGULAR MAIL to:
          LICS'91 Secretariat
          c/o CWI
          Kruislaan 413
          P.O. Box 4079
          1009 AB Amsterdam
          The Netherlands

          Phones:  (country 31)(city 20) 592 4171,  592 4058
          Fax:     (31) (20) 592 4199
          Telex:   12571 matctr.nl
Note, however, that no registration or reservation will be effective
UNTIL FULL PAYMENT IS RECEIVED, as explained below.

Participants may register at the Sunday reception, and then at the
conference site in the Free University, 8:00-17:00 Monday and 9:00-17:00
through Wednesday.  The conference brochure with some additional
information will be mailed upon request by the Conference Secretariat.
The postscript source of the conference brochure is available by anonymous
ftp in file lics91.ps in the directory  /usr/lics/public on
b.gp.cs.cmu.edu.

REGISTRATION FEE
================
Registration fee covers attendance in all sessions, a copy of the
proceedings, lunches, refreshments, receptions, and the conference banquet.

            through June 10       from June 11
Regular            NLG 475 ($ 270)     NLG 610 ($ 350)
Member/Author        NLG 375 ($ 215)     NLG 480 ($ 275)
Student             NLG 200 ($ 115)     NLG 245 ($ 140)
Companion           NLG 150 ($ 85)      NLG 175 ($ 100)

The reduced member/author rate applies to authors of accepted papers,
members of a sponsoring organization, members of institutional sponsors,
and members of the organizing and program committees.
The student rate applies to full time students, including PhD students and
Dutch AIO's and OIO's.  Full participation and privileges are extended to
registrants paying reduced rates.  The companion rate covers the social events
only (two receptions and banquet).

The LICS organizers have limited funds available for support of attendees
unable to obtain travel grants. Persons desiring such subsidy should contact
the Conference Secretariat, indicating their circumstances and the amount of
subsidy desired.


Subject:     FIRST ANNOUNCEMENT
Date: Sat, 06 Apr 91 12:55:55 -0500
From: mwpl@concour.cs.concordia.ca

             Montreal Workshop on Programming Languages
      -Algebraic and Logical Approaches in Programming Languages-
                        April 29-30, 1991
                            Montreal

Organized by the Montreal Programming Languages Group in cooperation
with the Montreal Interuniversity Category Theory-Logic Seminar and
the Queen's Workshop on Programming Languages.

Supported by the Center for Pattern Recognition and Machine Intelligence
of Montreal and the Ministere d'enseignement superieure et recherche de Quebec
under the Quebec-Ontario Cooperation Program.

The purpose of the workshop is to discuss together the various research
activities in programming languages and related fields from some
universities and research laboratories in Quebec, Ontario and northern
New York State. Participation from other area is also welcome.  Our intention
is to hold workshops in this series twice a year in cooperation with
several research groups in the Quebec and Ontario area.

Algebraic and logical approaches in programming languages are becoming
increasingly important both in the theoretical and the practical levels.
The first workshop will be focused on algebraic and logical aspects of
programming languages, including new generation programming language design,
semantics of programming languages, algebraic specification languages,
formal program verification, logical framework of the object-oriented paradigm,
and other issues related to algebraic or logical approaches to language theory.

WORKSHOP LOCATION:

          Faculty Club
          7th Floor
          Hall Building
          Concordia University
          1455 boul. de Maisonneuve Ouest
          Montreal, Quebec

WORKSHOP TIME:

          Monday afternoon, April 29 to Tuesday afternoon, April 30.
          A detailed program will follow soon upon your request.

TENTATIVE PROGRAM:

          Keynote lectures:

                     Nachum Dershowitz (U. Illinois)
                     Jim Lambek (McGill U.)
                     Maurice Nivat (U. Paris VII, visiting Concordia U.)
                     Bob Tennent (Queen's U.)

          Other speakers include:

                     M. Barr (McGill U.)
                     P. J. Scott (U. Ottawa)
                     M. Okada (Concordia U.)
                     P. Panangaden (McGill U.)
                     A. Podelski (DEC-Paris)
                     H. Mili (UQAM)
                     J. Seldin (Concordia U.)
                     J. Zucker (McMaster)
                     (and some others are under negotiation.)


          In order to provide a suitable atmosphere for interaction
          among the participants, the number of participants will
          be limited.  Please send e-mail to mwpl@concour.cs.concordia.ca
          for participation information.

          There is no registration charge.  Tuesday lunch will be
          served in the Workshop with a reasonable charge,
          as well as a Monday night cash-bar reception.

ACCOMMODATION:

          Unfortunately, the University dormitory is not available
          during this period.

          The following are some hotels very close to the workshop
          location (within a few minutes walk):

                     Hotel Chateau Versailles
                     $85 for single/double (Concordia rate)
                     514-933-3611

                     Maritime Hotel
                     $77 for single/double (Concordia rate)
                     514-934-1411

                     Hotel Europa
                     $70 for single, $80 for double.
                     514-866-6492

                     YWCA (female only)
                     $43 (single with semi-private bath)
                     $47 (single with private bath)
                     $58 (double)
                     514-866-9941

                     YMCA (both male and female)
                     $30 (single)
                     $28 (student)
                     514-849-8393


ORGANIZING COMMITTEE (Tentative):

          M. Barr       (McGill U.)
          G. Bochmann   (U. Montreal and CRIM) (Under negotiation)
          P. Grogono    (Concordia U.)
          B. Hodgson    (U. Laval)
          H. Mili       (UQAM)
          M. Nivat      (U. Paris VII, visiting Concordia U.)
          M. Okada      (Concordia U.)(chair)
          P. Panangaden (McGill U.)
          P. J. Scott   (U. Ottawa)
          J. Seldin     (Concordia U.)
          B. Tennent    (Queen's U.)
          J. Zucker     (McMaster U.)

For further information, send e-mail to

          mwpl@concour.cs.concordia.ca

or write to

          MWPL, c/o Dr. M. Okada
          Department of Computer Science
          Concordia University
          1455 boul. de Maisonnneuve Ouest
          Montreal, Quebec H3G 1M8


Subject:     CT91 reminder
Date: Tue, 9 Apr 91 11:45:58 EDT
From: fox@triples.Math.McGill.CA (Thomas F. Fox)

CATEGORY THEORY 1991: REMINDER

June 23-30, 1991, McGill University, Montreal, Canada


We are making final arrangements for the international meeting this
summer, and we would like to have a firm count of the participants
as soon as possible.  Over seventy of our colleagues from outside
North America have indicated they will come to Montreal, so this
could be the biggest category theory meeting ever.

Please send us your registration fee ($150 CAN, $175 after May 1) as
soon as possible, along with your housing deposit.  Dorm rooms
(singles) are only $32/night.  Tourist rooms (doubles) are available
for $38 (shared bath) or $48 (with bath), while a hotel room is $100.
Please make your checks payable to "CATEGORY THEORY 1991".

We have tourist information available for those who want to take a
vacation in Canada before or after the meeting.  If you have any
other questions, please contact us at the address below.


CATEGORY THEORY 1991                        Email:  mt16@musica.mcgill.ca
Math Dept, McGill University                Fax:    (1-514) 398-3899
805 Sherbrooke St W                         Tel:    (1-514) 398-3806
Montreal, Quebec
CANADA  H3A 2K6

Subject:     algebras on graph sets
Date: Thu, 11 Apr 91 10:33:33 EDT
From: "Joanna A Ellis-Monaghan"     <JJE%UNC.BITNET@ncsuvm.ncsu.edu>

Does anyone have any information on past or present
work with bialgebra/Hopf algebra structures (or any
coalgebra structures even )
on sets of graphs?  I am a grad student working on my
dissertation and I would be very grateful for any
referrence or contacts anyone could give me.
Thank you. Jo Ellis-Monaghan.

Subject:     RE: algebras on graph sets
Date: Fri, 12 Apr 91 18:42 GMT
From: MAS010@vaxa.bangor.ac.uk

With regard to the question from Joanna A Ellis-Monaghan, I don't know if it is
quite what was wanted, but John Shrimpton's thesis here was first on
the cartesian closed category (actually, topos) of directed graphs, but then
applying this to say that the automorphism structure for a (directed ) graph
is an internal group in directed graphs and so is a graph-group. This structure
is also known as a `pre-cat^1 group' (Brown-Loday, Topology, 26 (1987)),
which is equivalent to a pre-crossed module. This has an associated crossed
module. So the automorphism structure of a directed graph is a crossed module.
This leads to the notion of inner automorphism , and centre of a graph.
The paper on this is to appear in the JPAA, and a preprint is available from
Bangor (if we print some more!). The aim is to relate the inner autos and
centre of a graph to properties of the graph. E.g., in the finite case, the
centre is a Z_2 vector space, and its dimension is related to properties of the
graph.
Ronnie Brown

Subject:     question on set theory
Date: Sun, 14 Apr 91 20:19:52 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

This question is not category theory, but I am sure there are people on
the net who know much more set theory than me.  If you assume the
generalized continuum hypothesis, it is evident that any power cardinal
$\kappa$ has the property that $\lambda < \kappa$ implies $2^\lambda <=
\kappa$.  Otherwise, that property is obvious to me only for
inaccessible cardinals.  My question is whether there are a large class
of cardinals for which that is true even without the GCH?

Michael

Subject:     Re: question on set theory
Date: Monday, 15 April 1991 10:48:38 EST
From: Daniel.Leivant@B.GP.CS.CMU.EDU

Let
(beth)_0 = (aleph)_0,
(beth)_(a+1) = 2^(beth)_a,
(beth)_l = lim { (beth)_a | a < l }  for  l  a limit ordinal

Then for any cardinal  k = (beth)_l (l limit)
  m < k  ==>  2^m < k

Note that by Replacement there are as many such cardinals k  as
there are (limit) ordinals, whereas ZFC does not prove the
existence of even one inaccessible cardinal.

Date:     Tue, 16 Apr 91 10:35:02 EDT
From:     "Andreas R. Blass" <USERGC4C@UMICHUB.BITNET>
Subject:  question on set theory

This is in reply to Mike Barr's question about cardinals kappa such
that, for all lambda<kappa, the power set of lambda has cardinality
<= kappa.  (I assume that I've correctly reconstituted the question
after Bitnet revised the TeX codes in it.)  There are lots (i.e., a
closed unbounded class) of such cardinals kappa.  To get one (as
large as you like), start with any cardinal, iterate exponentiation
(with base 2) to produce a countable sequence of larger cardinals,
and take the supremum of this sequence.  This clearly has the desired
property (in fact with < in place of <=).  Furthermore, this property
is preserved by suprema.  So you get lots of such cardinals, without
needing any assumptions (like inaccessibles) that go beyond ZFC.
     Andreas Blass

Subject:     Re: question on set theory
Date: Mon, 15 Apr 91 23:43:16 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

Thanks!  Two different people misconstrued my question as asking if
m < k is 2^m <= 2^k.  You actually answered an even more exigent
question since I asked only that m < k imply 2^m <= k, but your
answer is even better, since the strict inequality is preserved.
You can't make beth in tex, can you?  Not without Hebrew fonts.

Anyway, thanks again.

Michael
+++++++++++++++++++++++++++++++++++++++++
Date: Tue, 16 Apr 91 08:27:39 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)
Subject: My question

After thinking about Daniel Leivant's answer for 10 seconds, I realized
that these beths aren't regular and I need regular cardinals with this
property.  Given GCH power cardinals have this property, so it is
certainly known consistent with ZF(C), so it is certainly less
problematic than assuming inaccessibles.  But that about exhausts my
knowledge of the subject.

Michael

Subject:     beth in TeX
From:       Paul Taylor <pt@doc.ic.ac.uk>
Date:       Tue, 16 Apr 91 18:14:20 BST

You can do \beth in TeX, but you need the AMS symbol fonts (msym10 or msbm10)
and associated macros (mssymb.tex or some similar name).

As a general comment (since I frequently get complaints about mssymb.tex and
a4.sty in relation to my diagram macros) if your local TeX system doesn't
have these things then you should COMPLAIN LOUDLY to your system manager as
they are part of the standard TeX  distribution. The same applies if you're
still running TeX version 2.993 (I've even seen systems with 2.0 still!):
3.1 is current.  TeX is public domain and available from several fileservers;
there is really no excuse for having defective systems, especially if you're
a unix user.

Subject:     A final answer from Leivant to my question
Date: Tue, 16 Apr 91 09:53:50 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

Date: Tuesday, 16 April 1991 07:52:30 EST
From: Daniel.Leivant@B.GP.CS.CMU.EDU
To: Michael Barr <barr@triples.Math.McGill.CA>
Subject: Re: question on set theory

okay, then how about taking a regular (beth)_l with l limit.
say

f(0) = (beth)_0
f(a+1) = (beth)_{f(a)}
f(l) = lim_{a < l} (beth)_a

and take a fixpoint of f.

again, this depends on Replacement and Choice, but not
GCH or the existence of inaccessibles.

Subject:     re: question on set theory
Date:     Fri, 19 Apr 91 16:15:52 EDT
From:     "Andreas R. Blass" <USERGC4C@UMICHUB.BITNET>

This is in reply to Mike Barr's revised question, requiring regularity,
and Dan Leivant's reply.  Unfortunately, regular beths with limit
subscript are inaccessible, which Mike wanted to avoid.  Even more
unfortunately, I believe it is known to be consistent (relative to very
large cardinals) that there are no cardinals of the sort Mike wants.
Specifically, it is consistent that GCH fails everywhere, a result of
Foreman and Woodin.  In such a universe, the requirement "for all lambda
< kappa, 2^lambda<=kappa " implies that kappa is a limit cardinal; if
you also require kappa to be regular, then it is weakly inaccessible.
I believe that the violations of GCH in the Foreman-Woodin model are
mild enough so that such kappas must actually be strongly inaccessible,
but I'm not certain about this.
     Incidentally, the fact that the Foreman-Woodin model requires
large cardinals for its construction does not mean that this model
has any inaccessibles.  It does mean that there are cardinals that are
inaccessible (and measurable, and much more) in certain submodels.
     Andreas Blass

Subject:     Categories of separated presheaves
Date: Mon, 22 Apr 91 10:57:29 pdt
From: dbenson@yoda.eecs.wsu.edu (David B. Benson)

 Let E be the category of presheaves on space X and
S the category of sheaves on the same space, clearly the category
of separated presheaves on X, call it P, is between E and F.
?In more detail, P is the full subcategory of E determined by the
separated presheaves on X.?
 I suppose that P is not a topos in general, but I am wondering
if anyone knows of a nice characterization of it, or indeed whether there
are any papers on this topic.  Neither Barr and Wells' TTT nor
Peter Johnstone's book says enough about separated presheaves
for my current explorations of the connections between sheaf-theoretic
ideas and some questions in software systems theory that I am
working on with Rakesh Dubey.
 Any suggestions will be most appreciated.

Thanks,
David

Subject:     separated presheaves
Date: Mon, 22 Apr 91 21:06:42 CDT
From: koslowj@math.ksu.edu (Juergen Koslowski)

David B. Benson asked for a characterization of the category P
of presheaves on a space X, which is sandwiched between the categories
S of sheaves and E of presheaves.

P is just the epi-reflective hull of S in E. (All epis in E are regular.)

J"urgen Koslowski
Department of Mathematics
Kansas State University
Manhattan, KS 66502
koslowj@math.ksu.edu

Subject:     set theory question
Date: Mon, 22 Apr 91 21:37:38 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

Dear Bob:

Here is a distillation of the answers I got from several people on my
question on set theory.  What I was asking for (eventually) is called a
weakly inaccessible cardinal.  What Dan Leivant constructed was actually
not regular either (Les Nelson).  If it was it was inaccessible.  There
are models of set theory with no cardinals that satisfy the GCH and
probably (Blass wasn't certain) had no weakly inaccessibles either.
Oddly enough those models were constructed using some large cardinals.
No stranger, actually, than Freyd's construction of models lacking
choice that start from ZFC and build an elementary topos lacking choice
and then a model of set theory also lacking choice.

So the upshot is that what I wanted is indeed weaker than the existence
of inaccessibles, but still fairly strong.  Fortunately, it is only a
peripheral to what I was doing.  It clarified a side issue that had no
effect on the main result, which is that you certainly don't have to
delve into the mysteries of non-well-founded sets in order to show that
the coalgebras for an inaccessibly accessible functor have a terminal
model no larger than the inaccessible provided the functor takes smaller
cardinals to smaller cardinals.

Michael

Subject:     Re: Categories of separated presheaves
Date:         Tue, 23 Apr 91 07:57:20 MEX
From:         Leopoldo Roman <IMATE@UNAMVM1>


You can see, for instance, the monograph by Kock and Wraith,
sincerely yours
                                L. Roman.

Subject:     Categorical view of loop invariants
From:          C Barry Jay <cbj@lfcs.ed.ac.uk>
Date:          Wed, 24 Apr 91 11:12:28 bst

Program loops have a very simple categorical interpretation, as loop
diagrams, i.e. as diagrams with one object C and one morphism f,
necessarily an endomorphism of C.


   --
        /    \
       |      |
       |      \/
       |
     f |      C
       |
       |      |
        \    /
          --

Of course, the limit of the loop is its fixpoints. The colimit,
however, is even more interesting. A cocone for the diagram is a
morphism g:C-->Q such that f;g = g. That is, an *invariant* for the
loop. Thus the colimit is the universal invariant of the loop.

Definition
A loop *converges* if it has an object of invariants Inv(f)
which is also an object of fixpoints such that the canonical composite

  Inv(f) --> C --> Inv(f)

is the identity.

This property captures the desirable property of a loop that its
iteration approaches a fixpoint. The simplest way to achieve this is
if the loop always terminates after a finite number of steps. While
such *termination* is equivalent to convergence in the category of
Sets, the topological nature of domain theory allows convergence
without termination.

There are two technical reports available which exploit such loops.


 Fixpoint and loop constructions as colimits
and
   Tail recursion via universal invariants

The first shows how to interpret while-loops in domains, and give
termination conditions. The second gives a categorical account of tail
recursion, and establishes conditions under which a tail recursive
characterisation of finite lists is equivalent to the usual intial
algera construction.

Copies of the latex code for either paper can be obtained by e-mail
request (sorry - no ftp here yet!). Please specify if you need a copy
of Paul Taylor's diagrams package: diagrams3.

Barry Jay


Subject:     Program of MWPL
Date: Wed, 24 Apr 91 21:32:34 -0400
From: mwpl@Concour.cs.Concordia.CA

                         Program of the
             Montreal Workshop on Programming Languages
      -Algebraic and Logical Approaches in Programming Languages-
                        April 29-30, 1991
                            Montreal

Organized by the Montreal Programming Languages Group.

In cooperation with the Montreal Interuniversity Category Theory-Logic
Seminar, the Queen's Workshop on Programming Languages, and the McMaster
International Workshops on Programming Languages.

Supported by the Center for Pattern Recognition and Machine Intelligence
of Montreal and the Ministere d'enseignement superieure et recherche de Quebec
under the Quebec-Ontario Cooperation Program.

There is no registration charge.  Tuesday lunch will be served in the
Workshop with a reasonable charge, as well as a Monday night cash-bar
reception.

WORKSHOP LOCATION:

          Faculty Club
          7th Floor
          Hall Building
          Concordia University
          1455 boul. de Maisonneuve Ouest
          Montreal, Quebec

WORKSHOP TIME:

          1:00PM Monday, April 29 to 5:10PM Tuesday, April 30.

PROGRAM:

          All events, including lectures, reception (Monday),
          coffee, breakfast (Tuesday) and lunch (Tuesday), will take
          place in the Faculty Club.

          Monday (April 29)

          Pre-Workshop Departmental Open Seminar:

 11:00 AM Dominique Sotteau (U. Paris-Sud & CNRS)
          "Embeddings of Interconnection Networks -
          The Graph Embedding Problem"

          Formal Program of MWPL
          ----------------------

  1:00 PM Opening Address
          Keynote Lecture
          Maurice Nivat (U. Paris VII)
          "Tree Languages"

  2:00 PM D. Therien (McGill U.)
          "Regular Languages and Parallel Computation"

  2:40 PM coffee

  3:00 PM A. Podelski (DEC - Paris Lab)
          "The Logic, Inheritance, Functional and Equational
          Language - LIFE"

  3:40 PM M. Okada (Concordia U.)
          "Executable Higher Order Algebraic Specification
          Languages"

  4:10 PM break

  4:20 PM D. Craigen and M. Saaltink (Odyssey Research, Ottawa)
          "Simple Type Theory in EVES"

  4:50 PM P. J. Scott (U. Ottawa)
          "Uniqueness Conditions for Typed Functional Languages"

  5:30 PM break

  5:40 PM G. Butler (U. Sydney)
          "Cayley: A Language for Computation with Algebraic
          Structures"

  6:10 PM G. Pottinger (Odyssey Research, Ithaca, NY)
          "Defining Unification for Descriptions of Lambda-terms"

  6:40 PM Workshop Reception
          (light meal and cash bar)

  8:30 PM Committee Meeting

          Tuesday (April 30)

  8:30 AM coffee and doughnuts

  9:10 AM Keynote lecture
          J. Lambek (McGill U.)
          "Least Fixpoints in Cartesian Closed Categories"

 10:10 AM J. Zucker (McMaster U.)
          "Application of Intensional Logic to Program Semantics"

 10:50 AM break

 11:00 AM P. Panangaden (McGill U.)
          "Semantic Foundations of Concurrent Constraint Programming"

 11:40 AM H. Mili (U. Quebec - Montreal)
          "Constraints in Object-Oriented Programming"

 12:10 PM Workshop Lunch

  2:00 PM Keynote Lecture
          R. D. Tennent (Queen's U.)
          "Possible World Semantics for Algol-like Programming
          Languages"

  3:00 PM M. Barr (McGill U.)
          "Terminal Coalgebras in Well-Founded Set Theory"

  3:40 PM J. Seldin (Concordia U.)
          "Excluded Middle Without Definite Descriptions
           in the Theory of Constructions"

          End of Formal Program of MWPL

          Post-Workshop Departmental Open Seminar:

  4:10 PM Maurice Nivat (U. Paris VII)
          "Mathematics of Tiling Games"


ORGANIZING COMMITTEE:

          M. Barr       (McGill U.)
          P. Grogono    (Concordia U.)
          B. Hodgson    (U. Laval)
          P. Lauer      (McMaster U.)
          H. Mili       (UQAM)
          M. Nivat      (U. Paris VII, visiting Concordia U.)
          M. Okada      (Concordia U.)(chair)
          P. Panangaden (McGill U.)
          P. J. Scott   (U. Ottawa)
          R. Seely      (McGill U.)
          J. Seldin     (Concordia U.)
          R. D. Tennent (Queen's U.)

For further information, send e-mail to

          mwpl@concour.cs.concordia.ca

or write to

          MWPL, c/o Dr. M. Okada
          Department of Computer Science
          Concordia University
          1455 boul. de Maisonnneuve Ouest
          Montreal, Quebec H3G 1M8

Subject:     Tex 3.0
Date: Thu, 25 Apr 91 03:31:37 PDT
From: Vaughan Pratt <pratt@cs.stanford.edu>

Don't worry too much about Tex 3.1, all the systems I'm aware of are
only up to 3.0 (Paul's included, he confesses!).  If you want to
upgrade to 3.0, here are some places to look.  Except for the first I
found these by sending mail to archie@quiche.cs.mcgill.ca (a program)
with subject "prog tex" and picking out those that referred to tex3.0.
(I should have said "prog tex3.0").  Many more don't so identify
themselves with the 3.0 suffix but may well carry tex3.0.

For those not used to using anonymous ftp to fetch things with I
include a copy of the README from Boole.Stanford.EDU, whose
"Instructions" section explains the procedure.

        Vaughan Pratt


Host labrea.stanford.edu  (36.8.0.47)
    Location: /pub/tex
Host ccadfa.cc.adfa.oz.au   (131.236.1.2)
    Location: /tex/tex-3.0
Host emx.utexas.edu   (128.83.1.33)
    Location: /pub/mnt/source/tex/tex-3.0
Host freja.diku.dk   (129.142.96.1)
    Location: /TeX/TeX-3.0
Host psuvax1.cs.psu.edu   (130.203.1.6)
    Location: /pub/src/TeX3.0/TeX3.0
Host ugle.unit.no   (129.241.1.97)
    Location: /pub/tex/tex-3.0
Host uxc.cso.uiuc.edu   (128.174.5.50)
    Location: /text/TeX3.0/TeX3.0
Host walhalla.informatik.uni-dortmund.de   (129.217.64.63)
    Location: /pub/comp/msdos/emtex3.0




               The Sun Garage Cache Prepublication Medium

                   Papers on Parallel Software Theory
                       Available by Anonymous FTP
                         from Boole.Stanford.EDU


This file is README in the /pub directory of Boole.Stanford.EDU,
36.8.0.65, accessible by anonymous ftp.

The /pub directory is for FTP distribution of prepublications in the
area of parallel software theory.  It is run by the Boole group, a
subgroup of the Mathematical Theory of Computation group, Computer
Science Department, Stanford University.  The group consists of the
following people.

        Ross Casley                     casley@cs.stanford.edu  (SYS)
        Roger Crew                      crew@cs.stanford.edu    (SYS)
        Rob van Glabbeek                rvg@cs.stanford.edu
        Vineet Gupta                    vgupta@cs.stanford.edu
        Vaughan Pratt (group leader)    pratt@cs.stanford.edu   (SYS)
        Pat Simmons (secretary)         simmons@cs.stanford.edu
        Orli Waarts                     orli@cs.stanford.edu

==========================Instructions=================================

FTP LOGIN.  Give the following commands.

        ftp boole.stanford.edu
Login:  anonymous                       (if you don't have an account on boole)
Paswd:  yoursurname                     (though any string will work)
        bin                             (if you are retrieving a .dvi file)
        prompt off                      (if you want no ? prompts from mget)
        cd pub                          (change directory to ^ftp/pub
        ls -lt                          (see what's there, most recent first)
        mget filename-1 ... filename-n  (e.g.   mget cg.tex logic.bib)
        quit                            (exit from FTP)

SOURCE.  To retrieve the source to paper foo, get foo.tex and
logic.bib.  The source should be compiled using

        latex foo; bibtex foo; latex foo; latex foo

DVI.  If you wish to print paper foo without having to compile with
latex, retrieve just foo.dvi.  You must first give the bin command to
ftp since .dvi files are not text files.  Print foo.dvi on your host
using

        lpr -d foo.dvi.

PROBLEMS.  If you have problems in either retrieving or compiling
papers, please contact a systems person (flagged SYS on the list
above).

===========================Available papers=================================

TITLES

casthes.tex On the Specification of Concurrent Systems
es.tex      Event Spaces and their Linear Logic (in preparation)
catl.tex    Concurrent Automata and Their Logic (old es.tex, temporary)
cg.tex      Modeling Concurrency with Geometry
jelia.tex   Action Logic and Pure Induction
man.tex     Temporal Structures
pp2.tex     Teams Can See Pomsets
am4.tex     Enriched Categories and the Floyd-Warshall Connection
iowatr.tex  Dynamic Algebras as a well-behaved fragment of Relation Algebras
ijpp.tex    Modelling Concurrency with Partial Orders

-----------------------------------------------------------------------

ABSTRACTS


casthes.tex On the Specification of Concurrent Systems
            Ross Casley
            Ph.D. Thesis, January, 1991

In models of concurrent processes constraints on the order of events are
often represented by partial orders, and schedules of events are then
defined using an algebra of standard operations such as sequential and
parallel composition.

In this dissertation the notion of partial order is replaced by that of a
set with a metric which takes values in a given ordered monoid.  Partial
orders are the simple case of a monoid whose two elements represent the
presence or absence of a constraint.

An ordered monoid can be seen as a monoidal category, and schedules based
on it are categories enriched in the monoid.  Algebraic operations on
schedules can then be defined as constructions in the category of
schedules.

These definitions rely on certain properties of a category of schedules,
such as closure and completeness.  To simplify proofs of these properties,
two constructions are defined.  The first creates a category of unlabeled
schedules from a system of constraints.  The second adds labels to
unlabeled schedules.  Many categories of interest can be constructed from
simple categories using these two methods.  The main results of the
dissertation derive the required properties of categories so constructed
from similar, more easily verified properties of the base categories.

Several notions of timing constraint can be viewed in a uniform way in
this framework.  An example is the Gaifman-Pratt system, essentially the
partial order model with additional specification as to whether two events
may occur simultaneously.  It corresponds to a monoid whose three elements
represent strict precedence, lax precedence (simultaneity is permitted),
and absence of constraint.  Real-valued timing constraints correspond to
the additive monoid of the real numbers.


es.tex    Event Spaces and their Linear Logic
            V. Pratt

Boolean logic treats disjunction and conjunction symmetrically and
algebraically.  The corresponding operations for computation are
respectively nondeterminism (choice) and concurrency.  Petri nets treat
these symmetrically but not algebraically, while event structures treat
them algebraically but not symmetrically.

Here we achieve both via the notion of an event space as a poset with
all nonempty joins representing concurrences and a top representing the
unreachable event.  The symmetry is with the dual notion of state
space, a poset with all nonempty meets representing choices and a
bottom representing the start state.  The algebra is that of a parallel
programming language expanded to the language of linear logic, Girard's
axiomatization of which is satisfied by the event space interpretation
of this language.

Event spaces resemble vector spaces in distinguishing tensor product
from direct product and in being isomorphic to their double dual, but
differ from them in distinguishing direct product from direct sum and
tensor product from tensor sum.


catl.tex    Concurrent Automata and Their Logic
            V. Pratt
            Superseded by es.tex

A concurrent automaton is a poset with a top (the global initial state)
and all nonempty sups (the local initial states).  A schedule is
defined identically.  These form dually isomorphic categories Aut and
Sched admitting universally definable operations constituting a
concurrent programming language, and additional operations constituting
a linear logic of concurrency in which $!a$ and $?a$ are respectively a
free choice automaton and a free concert schedule.  The linear theory
Th(CSLat) of complete semilattices strictly extends Th(Aut) with
$\query a=\bang a$, an unwanted isomorphism of free and cofree
semilattices (both being Boolean algebras) found only in CSLat.  Both
theories contain such howlers as 0=1.  Intersection with classical
logic (multiplication by 2) removes the howlers, but not usefully so
for CSLat, and moreover $\query a=\bang a$ remains.  The self-duality
of these categories permits a non-categorical account requiring only
elementary lattice theory.


cg.tex          Modeling Concurrency with Geometry
                V. Pratt
                To appear in POPL-91.

Branching time and causality find their respective homes in the
Birkhoff-dual models of automata and schedules.  This creates a
puzzle:  if the duality is supposed to make the models completely
equivalent then why does each phenomenon have a preferred side?  We
identify dimension as the culprit:  1-dimensional automata are
skeletons permitting only interleaving concurrency, true n-fold
concurrency resides in transitions of dimension n.  The Birkhoff dual
of a poset then becomes a simply-connected space.  We distinguish
Birkhoff duality from Stone duality and treat the former in detail from
a concurrency perspective.  We introduce true nondeterminism and define
it as monoidal homotopy; from this perspective nondeterminism in
ordinary automata arises from forking and joining creating nontrivial
homotopy.  We propose a formal definition of higher dimensional
automaton as an n-complex or n-category, whose two essential axioms are
associativity of concatenation within dimension and an interchange
principle between dimensions.


jelia.tex       Action Logic and Pure Induction
                V. Pratt
                To appear in Proceedings of JELIA-90, European Workshop on
                Logics in AI (ed. J. van Benthem and Jan Eijck),
                held Amsterdam, Sept. 1990

In Floyd-Hoare logic programs are dynamic while assertions are static
(hold at states).  In action logic the two notions become one, with
programs viewed as on-the-fly assertions whose truth is evaluated along
intervals instead of at states.  Action logic is an equational theory
ACT conservatively extending the equational theory REG of regular
expressions with operations preimplication a -> b (HAD a THEN b) and
postimplication b <- a (b IF-EVER a).  Unlike REG, ACT is finitely
based, makes a* reflexive transitive closure, and has an equivalent
Hilbert system.  The crucial axiom is that of pure induction,
(a -> a)* = a -> a.


man.tex         Temporal Structures
                R. Casley, R. Crew, J. Meseguer, V. Pratt

                To appear in Mathematical Structures in Computer
                Science, inaugural issue, 1990.  Revision of
                proceedings version in Category Theory and Computer
                Science, LNCS 389, Manchester, 1989.  Formerly called
                "Dynamic Types."

We combine the principles of the Floyd-Warshall-Kleene algorithm,
enriched categories, and Birkhoff arithmetic, to yield a useful class
of algebras of transitive vertex-labeled spaces.  The motivating
application is a uniform theory of abstract or parametrized time in
which to any given notion of time there corresponds an algebra of
concurrent behaviors and their operations, always the same operations
but interpreted automatically and appropriately for that notion of
time.  An interesting side application is a language for succinctly
naming a wide range of datatypes.


pp2.tex         Teams Can See Pomsets
                G. Plotkin and V. Pratt
                Draft in preparation

Strings may serve as both specifications and observations of behavior.
However partial strings or pomsets, superior to strings in certain
respects for the representation of concurrent behavior, are provably
unobservable and hence apparently suitable only for specifying
behavior.  The proof however tacitly assumes that observers are
isolated individuals.  We show that observations by a cooperating team
of sequential observers agreeing on *what* happened but not
*when* can distinguish all pomsets.  The resolving power of a finite
team increases strictly with its size k, permitting it to distinguish
all pomsets of dimension (not width) k but not all of k+1.  These
results extend to observation of augment closed processes.  As expected
we depend on the now standard technique of refinement of atomic events
to complex events; what is not expected is that their complexity need
be only that of nondeterminism, in that we refine one atomic event to a
set of alternative atomic events, not to a set of sequences.


am4.tex         Enriched Categories and the Floyd-Warshall Connection
                V. Pratt
                Proceedings, AMAST-88

We give a correspondence between enriched categories and the
Gauss-Kleene-Floyd-Warshall connection familiar to computer
scientists.  This correspondence shows this generalization of
categories to be a close cousin to the generalization of transitive
closure algorithms.  Via this connection we may bring categorical and
2-categorical constructions into an active but algebraically
impoverished arena presently served only by semiring constructions.  We
illustrate these techniques by applying them to Birkoff's poset
arithmetic, interpretable as an algebra of ``true concurrency.''


iowatr.tex   Dynamic Algebras as a well-behaved fragment of Relation Algebras
             V. Pratt
             Algebraic Logic and Universal Algebra in Computer Science,
             LNCS 425, ed. C.H. Bergman, R.D. Maddux, D.L. Pigozzi,
             Springer-Verlag, 1990.

The varieties RA of relation algebras and DA of dynamic algebras are
similar with regard to definitional capacity, admitting essentially the
same equational definitions of converse and star.  They differ with
regard to completeness and decidability.  The RA definitions that are
incomplete with respect to representable relation algebras, when
expressed in their DA form are complete with respect to representable
dynamic algebras.  Moreover, whereas the theory of RA is undecidable,
that of DA is decidable in exponential time.  These results follow from
representability of the free intensional dynamic algebras.


ijpp.tex        Modelling Concurrency with Partial Orders
                V. Pratt
                International Journal of Parallel Programming,
                15:1, 33-71, Feb. 1986.

Concurrency has been expressed variously in terms of formal languages
(typically via the shuffle operator), partial orders, and temporal
logic, inter alia.  In this paper we extract from these three
approaches a single hybrid approach having a rich language that mixes
algebra and logic and having a natural class of models of concurrent
processes.  The heart of the approach is a notion of partial string
derived from the view of a string as a linearly ordered multiset by
relaxing the linearity constraint, thereby permitting partially ordered
multisets or pomsets.  Just as sets of strings form languages, so
do sets of pomsets form processes.  We introduce a number of operations
useful for specifying concurrent processes and demonstrate their
utility on some basic examples.  Although none of the operations is
particularly oriented to nets it is nevertheless possible to use them
to express processes constructed as a net of subprocesses, and more
generally as a system consisting of components.  The general benefits
of the approach are that it is conceptually straightforward, involves
fewer artificial constructs than many competing models of concurrency,
yet is applicable to a considerably wider range of types of systems,
including systems with buses and ethernets, analog systems, and
real-time systems.

Date: Thu, 25 Apr 91 18:00:16 PDT
From: Vaughan Pratt <pratt@cs.stanford.edu>
Subject: Event spaces paper

"Event Spaces and Their Linear Logic," which I promised way back in
February, is now a more or less complete 19-page paper, see abstract
below.  It is available as pub/es.tex from Boole.Stanford.EDU by
anonymous ftp, and will appear in the AMAST'91 proceedings (AMAST is in
Iowa City late next month, May 22-25).  It supersedes "Concurrent
Automata and Their Logic".  See pub/README on Boole for abstracts of
related papers.

The intended application of event spaces is to modelling concurrency.
In January I claimed that they were incidentally "the best model of
linear logic to date".  The guardians of posterity were understandably
shocked.  Let me try to attenuate my obvious proprietor's bias a bit by
listing the criteria for "best" that I have in mind.  Only criterion 2
has the force of a theorem, but the other two are surely clear enough
that one could reasonably hope for some sort of consensus.

Event spaces are

   1.   simple: the category is just posets with all nonempty joins and
        a top, and their homomorphisms.

   2.   nondegenerate: the sums and products are four distinct operations;

   3.   useful: their primary raison d'etre is not as a model of linear
        logic but as a model of concurrency that in comparison to event
        structures is more general and has a cleaner algebraic
        structure, namely that of full linear logic.

If you have a model of full linear logic that meets all three criteria
as well or better I am likely to be among your first and most
enthusiastic customers (unless it turns out to require inaccessible
cardinals).

The closest competitor seems to be Girard's original model, coherent
spaces and their linear morphisms.  However the objects are a very
special case of state spaces (dual to event spaces), while the
morphisms require the conditions of monotonicity, continuity,
stability, and linearity, whereas event space morphisms are merely
homomorphisms.

Those models of full linear logic that purport to model concurrency all
seem very complicated to me, though I'd be very happy to be set
straight if I've overestimated the complexity of someone's model.

Other features of the paper: What linear logic is about (answer: it
combines elementary and categorical logic in the one system).
Applications of event spaces to family planning (no connection with
risque computers).

Herewith the abstract.

ABSTRACT

Boolean logic treats disjunction and conjunction symmetrically and
algebraically.  The corresponding operations for computation are
respectively nondeterminism (choice) and concurrency.  Petri nets treat
these symmetrically but not algebraically, while event structures treat
them algebraically but not symmetrically.

Here we achieve both via the notion of an event space as a poset with
all nonempty joins representing concurrence and a top representing the
unreachable event.  The symmetry is with the dual notion of state
space, a poset with all nonempty meets representing choice and a bottom
representing the start state.  The algebra is that of a parallel
programming language expanded to the language of full linear logic,
Girard's axiomatization of which is satisfied by the event space
interpretation of this language.

Event spaces resemble vector spaces in distinguishing tensor product
from direct product and in being isomorphic to their double dual, but
differ from them in distinguishing direct product from direct sum and
tensor product from tensor sum.

Subject:     Re: Categorical view of loop invariants (& diagrams)
From:       Paul Taylor <pt@doc.ic.ac.uk>
Date:       Mon, 29 Apr 91 12:24:05 BST

By "diagrams3", Barry Jay means the same version as was quite widely
distributed last year; it hasn't changed significantly since then.
It would be better to ask me for it than him, though.
(It was temporarily called diagrams3 whilst version 2 was still in service
and I wasn't confident about version 3)
