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 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" 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" Subject: question on set theory This is in reply to Mike Barr's question about cardinals kappa such that, for all lambda 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 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" 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 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 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 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 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 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)