From rrosebru@mta.ca Mon May 1 19:52:54 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA00721 for categories-list; Mon, 1 May 2000 19:49:38 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Organisation: Faculty of Science University of Amsterdam The Netherlands X-Address: See http://www.science.uva.nl/location Message-Id: <200005012025.WAA00714@Benedictus.wins.uva.nl> To: aiml@mac.com Subject: categories: AiML-ICTL 2000: Final Call for Papers Date: Mon, 1 May 2000 22:25:19 +0200 From: Advances in Modal Logic Reply-To: aiml@mac.com X-Mailer: by Apple MailViewer (2.106) X-Mailer-Extensions: SWSignature 1.3.2 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: [Apologies for multiple copies] FINAL CALL FOR PAPERS AiML-ICTL 2000 Advances in Modal Logic - International Conference on Temporal Logic 2000 October 4-7, 2000, University of Leipzig, Germany Deadline: May 15, 2000 AiML-ICTL 2000 In the year 2000, the Advances in Modal Logic workshop and the International Conference on Temporal Logic will be run as a combined event, bringing together the strongly related modal logic and computer science oriented temporal logic communities to present and share the latest exciting results in all relevant areas. TOPICS Topics of interest include: common-sense temporal reasoning, complexity of modal and temporal logics, deontic logic, description logics, dynamic logic, epistemic logic, modal logics of agency and space, modal logic and game theory, modal logic and grammar formalisms, modal realism and anti-realism, modal and temporal logic programming and theorem proving, model theory and proof theory of modal and temporal logic, representation of time in natural language semantics, non-monotonic modal logics, provability logic, temporal databases. Papers on related subjects will also be considered. SPECIAL SESSION During the workshop there will be a special session on description logics and applications of modal logic in Knowledge Representation. INVITED SPEAKERS Nuel Belnap (Pittsburgh) Stephane Demri (Grenoble) Silvio Ghilardi (Milan) Giuseppe de Giacomo (Rome) Mark Reynolds (Perth) Krister Segerberg (Uppsala) Colin Stirling (Edinburgh) Moshe Vardi (Houston) PAPER SUBMISSION Authors are invited to submit a detailed abstract of a full paper of at most 10 pages (a4paper, 11pt) by e-mail to the programme chair, using `AiML-ICTL Submission' as the subject line. The cover page should include title, names of authors, the coordinates of the corresponding author, and some keywords describing the topic of the paper. Following this it should be indicated whether this is a submission to AiML or ICTL. To be considered, submissions must be received no later than May 15, 2000. Note that at least one author of each accepted paper is required to attend the workshop to present the paper. PUBLICATION DETAILS Preliminary versions of the full papers should be made available at the workshop; two separate proceedings volumes (AiML and ICTL) will be submitted to CSLI Publications. Notification date for the conference is July 15, 2000; for the volumes it is December 1, 2000. Full versions of accepted ICTL papers can be offered fast track journal publication in one of D.M. Gabbay's Oxford Journals. GRANTS There will be a small number of grants available for participants from Eastern Europe. PROGRAM COMMITTEE Franz Baader, Aachen Howard Barringer, Manchester Marcelo Finger, Sao Paulo Nissim Francez, Haifa Dov Gabbay, London Greg Restall, Sydney Maarten de Rijke, Amsterdam Heinrich Wansing, Dresden (chair) Frank Wolter, Leipzig Michael Zakharyaschev, Leeds PROGRAM CHAIR Heinrich Wansing Dresden University of Technology Institute of Philosophy 01062 Dresden, Germany E-mail: Phone: +49 351 463 5489 Fax: +49 351 463 6068 LOCAL ORGANIZERS Frank Wolter, Leipzig Holger Sturm, Leipzig IMPORTANT DATES Submission deadline: May 15, 2000 Notification: July 15, 2000 Workshop: October 4-7, 2000 Preliminary version for workshop volume due: at the workshop Notification of acceptance for publication: December 1, 2000 FURTHER INFORMATION E-mail enquiries about AiML-ICTL 2000 should be directed to . Information about AiML can be obtained on the World-Wide Web at , and about AiML-ICTL 2000 at . -- Advances in Modal Logic - International Conference on Temporal Logic 2000 October 4-7, Leipzig, Germany www.illc.uva.nl/~mdr/AiML/ From rrosebru@mta.ca Wed May 3 14:08:20 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA10825 for categories-list; Wed, 3 May 2000 14:02:55 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <390F9E04.B3035C9F@di.fc.ul.pt> Date: Wed, 03 May 2000 04:33:24 +0100 From: Nuno Barreiro X-Mailer: Mozilla 4.72 [en] (X11; I; Linux 2.0.36 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: LINEAR Summer School (2nd call) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Please forward. We apologize for any duplication of this message in your mailbox. Best regards, Nuno Barreiro ------------------------------------------------------------------ =================================== = SECOND CALL - EXTENDED DEADLINE = =================================== The LINEAR International Summer School (Linear Logic and Applications) August 30 to September 7, 2000 Hotel Terra Nostra, S.Miguel, Azores, Portugal The Linear TMR research network (http://iml.univ-mrs.fr/LINEAR) is proud to announce its first International Summer School on Linear Logic and Applications. The school is directed to everyone doing postgraduate work in Computer Science or Mathematics with an interest in the field of Formal Logic and its applications. The school lasts one week and comprises both lectures and thematic sessions. The lectures are in the tradition of summer schools and cover one topic, from basic material to more advanced issues. The topics and lecturers are the following: Samson Abramsky --- Game Semantics Jean-Yves Girard -- Linear Logic and Ludics Stefano Guerrini -- Proof-Nets and Lambda-Calculus Yves Lafont ------- Phase Semantics and Decision Problems Phil Scott -------- Category Theory and Concrete Models The thematic sessions will cover state-of-the-art research in Linear Logic. Each session has an organiser responsible for inviting speakers who will talk about their work. The themes and organisers are the following: Andrea Asperti ---- Applications Vincent Danos ----- Proof Theory Thomas Ehrhard ---- Semantics Glynn Winskel ----- Concurrency The school will be held in the island of S.Miguel, Azores, amid luxurious vegetation and hot water springs. The entrance to the mythic kingdom of the Atlantis is believed to be located near Hotel Terra Nostra, some say at the bottom of its famous red and hot water swimming pool... Detailed information and application forms are available at http://linear.di.fc.ul.pt Don't forget to check it! From rrosebru@mta.ca Wed May 3 14:08:22 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA01404 for categories-list; Wed, 3 May 2000 14:05:25 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Computer Science Logic 2000 MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Message-ID: <14608.3666.81631.680433@carla.tcs.informatik.uni-muenchen.de> Date: Wed, 3 May 2000 13:32:34 +0200 (CEST) To: csl2000-list@carla.tcs.informatik.uni-muenchen.de Subject: categories: CSL2000 - 1st call for participation X-Mailer: VM 6.72 under 21.1 (patch 8) "Bryce Canyon" XEmacs Lucid Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id IAA27413 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: --------------------------------------------------------------------------- CSL 2000 1st CALL FOR REGISTRATION AND PARTICIPATION 14th Annual Conference of the European Association for Computer Science Logic (EACSL) Fischbachau, Germany, August 21-26, 2000 http://www.tcs.informatik.uni-muenchen.de/csl2000/ 1. ORGANIZATION 4. REGISTRATION 2. SCIENTIFIC PROGRAM 5. GRANTS 3. SOCIAL PROGRAM 6. LOCATION and ACCOMODATION 7. TRAVEL INFORMATON -------------------------------------------------------------------------- 1. ORGANIZATION CSL 2000 is the 14th Annual Conference of the European Association for Computer Science Logic. Program commitee: ----------------- Peter Clote (Muenchen, co-chair), Stephen Cook (Toronto), Kevin Compton (Ann Arbor), Laurent Fribourg (Cachan), Erich Graedel (Aachen), Gerhard Jaeger (Bern), Klaus Keimel (Darmstadt), Jan Willem Klop (Amsterdam), Jan Krajícek (Praha), Daniel Leivant (Bloomington), Tobias Nipkow (Muenchen), Helmut Schwichtenberg (Muenchen, co-chair), Moshe Vardi (Houston) Any questions about the organization should be sent to csl2000-org@tcs.informatik.uni-muenchen.de. 2. SCIENTIFIC PROGRAM: The scientific program includes 28 papers selected from 69 submissions, and 9 invited lectures including those for the symposium in honour of Yuri Gurevich. Preliminary Program: =================== Monday, Aug 21 --------------- Late Afternoon: Arrival and Registration Tuesday, Aug 22 --------------- 8.30 Invited Speaker: Colin Stirling (University of Edinburgh): (title to be announced) 9.30 Break 9.45 Equational Termination by Semantic Labelling Hitoshi Ohsaki, Aart Middeldorp and Juergen Giesl 10.15 Definability over Linear Constraints Michael Benedikt and H. Jerome Keisler 10.45 Coffee break 11.15 Completeness of Higher-Order Duration Calculus Zhan Naijun 11.45 From Programs to Games: Invariance and Safety for Bisimulation Marc Pauly 12.30 Lunch, Nature 15.30 Flatness is not a Weakness Hubert Comon and Veronique Cortier 16.00 On the Complexity of Explicit Modal Logics Roman Kuznets 16.30 Coffee break 17.00 Modal Satisfiability is in Deterministic Linear Space Edith Hemaspaandra 17.30 Independence: Logics and Concurrency J. C. Bradfield 19.00 Dinner Wednesday, Aug 23 ----------------- 8.30 Invited Speaker: Paul Beame (University of Washington): The Complexity of Proving Properties of Random Objects 9.30 Break 9.45 Discreet Games, Light Affine Logic and PTIME Computation A. S. Murawski and C.-H. L. Ong 10.15 On the Complexity of Combinatorial and Metafinite Generating Functions J. A. Makowski and K. Meer 10.45 Coffee break 11.15 The Descriptive Complexity of the Fixed-Points of Bounded Formulas Albert Atserias 11.45 Bounded Arithmetic and Descriptive Complexity Achim Blumensath 12.30 Lunch, Nature 15.30 A Proof-Theoretically Adequate Axiomatization of Intuitionistic Fuzzy Logic Matthias Baaz and Richard Zach 16.00 On the Logic of the Standard Proof Predicate Rostislav Yavorsky 16.30 Coffee break 17.00 Elementary Choiceless Constructive Analysis Peter M. Schuster 17.30 A Theory of Explicit Mathematics Equivalent to ID_1 Reinhard Kahle and Thomas Studer 19.00 Dinner Thursday, Aug 24 ---------------- SYMPOSIUM in honour of YURI GUREVICH on the occasion of his 60th birthday Invited Speakers: 8.30 Yuri Gurevich (Microsoft Research, Redmond): On Abstract State Machines 9.30 Break 9.45 Egon Boerger (University of Pisa, on sabbatical at Microsoft Research, Redmond): Composition and Submachine Concepts for Sequential ASMs 10.45 Coffee break 11.15 Wolfram Schulte (Microsoft Research, Redmond): Translating Theory into Practice - Abstract State Machines within Microsoft 12.30 Lunch, Nature 15.00 Andreas Blass (University of Michigan, Ann Arbor): On Choiceless Polynomial Time Computation and the Zero-One Law 16.00 Coffee break 16.30 Miklos Ajtai (IBM Almaden Research Center): Nonlinear Lower Bounds for Branching Programs 17.45 Saharon Shelah (Hebrew University, Jerusalem): Choiceless Polynomial Time Logic: Inability to express. 19.30 Conference dinner Friday, Aug 25 -------------- 8.30 Continuous Functionals of Dependent Types and Equilogical Spaces Andrej Bauer and Lars Birkedal 9.00 Subtyping with Power Types David Aspinall 9.30 Coffee break 10.00 Interactive Programs in Dependent Type Theory Peter Hancock and Anton Setzer 10.30 Elimination of Negation in a Logical Framework Alberto Momigliano 11.30 Excursion 19.00 Dinner Saturday, Aug 26 ---------------- 8.30 Invited Speaker: Bruno Poizat (University of Lyon): An unsuccessful attempt to construct a structure with fast elimination of quantifiers 9.30 Break 9.45 Finite Models and Full Completeness James Laird 10.15 A Fully Complete PER Model for ML Polymorphic Types Samson Abramsky and Marina Lenisa 10.45 Coffee break 11.15 Logical Relations and Data Abstraction John Power and Edmund Robinson 11.45 Sequents, Frames, and Completeness Thierry Coquand and Guo-Quiang Zhang 12.30 Lunch 15.30 On the Computational Interpretation of Negation Michel Parigot 16.00 Logic Programming and Co-inductive Definitions Mathieu Jaume 16.30 Coffee break 17.00 Axiomatizing the Least Fixed Point Operation and Supremum Zoltan Esik 17.30 Disjunctive Tautologies as Synchronization Schemes Vincent Danos and Jean-Louis Krivine 19.00 Dinner Sunday, Aug 27 -------------- Breakfast, Departure Conference Language: -------------------- The official language of the conference is English. 3. SOCIAL PROGRAM: - An excursion to one of the mountains (1600 m) nearby is planned for Friday afternoon - A conference dinner will be held at the Auracher Hof on Thursday evening 4. REGISTRATION To register for CSL 2000, fill in the registration form on the CSL 2000 homepage and return the signed form by ordinary mail or fax. EARLY CONFERENCE REGISTRATION FEE: The filled registration form must reach us by June 5th, 2000. Full-time students: 180 DM (92,01 EURO), Others: 260 DM (132,91 EURO) LATE CONFERENCE REGISTRATION FEE: (after June 5th, 2000) Full-time students: 260 DM (132.91 EURO), Others: 300 DM (153,36 EURO) Payments can either be made in DM by bank transfer to: (Germany) (from abroad) CSL 2000 CSL 2000 (Dr. M.Ruckert) Account No. 2805571599, BLZ 3002090 Konto 2805571599 SWIFT Code CITIDEF Citibank Muenchen Via: Citibank Privatkunden AG BLZ (Bankleitzahl) 300 209 00 Account No. 2805571599, CSL 2000 (Dr. M.Ruckert) or at the conference by Eurocard/Mastercard, VISA card, Eurocheque, or in cash (DM only). 5. GRANTS: There are some very limited funds to support participation of researchers from Eastern Europe and of students. For students the application needs to be accompanied by a letter of recommendation from their adviser. To apply for a grant, fill in the corresponding form on the CSL 2000 homepage and return it before May 20th. 6. LOCATION AND ACCOMMODATION The conference will be held at the Hotel Auracher Hof Bahnhofstrasse 4 D-83730 Fischbachau phone: +49-80 28 / 903-0 fax: +49-80 28 / 903-199 To reserve your accommodation, fill in the Accommodation Form on the CSL 2000 home page and return it by fax to the hotel. The hotel is closed until April 30, and from June 10 to June 25. Since Fischbachau belongs to a vacation area, we strongly recommend to book for accomodation before June 10th. After June 25, available rooms in the hotel may soon be booked by tourists. The hotel has 75 rooms, and in case that there will be more participants, some may have to share a room. 7. TRAVEL INFORMATION Note that there will be much holiday traffic in August, so we recommend that you >>> book your flight as early as possible <<<. Munich Airport (Muc) is easily accessible from most airports in Europe, the Near East and North America. At the airport, S-Bahn trains are leaving for Munich Central Station (Hauptbahnhof) every 20 minutes, taking about 45 minutes. >From Munich Central Station there are trains to Fischbachau (direction Bayrischzell, platform 27-31) leaving (almost) every hour, taking 70 minutes to Fischbachau Bahnhof. FOR MORE DETAILS, see the CSL 2000 home page http://www.tcs.informatik.uni-muenchen.de/csl2000/ Looking forward to meet you at the conference, the CSL 2000 Local Organization team. From rrosebru@mta.ca Sun May 7 12:22:49 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA00779 for categories-list; Sun, 7 May 2000 12:16:19 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: John MacDonald Date: Wed, 3 May 2000 13:21:59 -0700 (PDT) Message-Id: <200005032021.NAA04894@pascal.math.ubc.ca> To: categories@mta.ca Subject: categories: FMCS2000 Cc: johnm@math.ubc.ca Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: FMCS2000 Foundational Methods in Computer Science JUNE 1st - 4th, 2000 The Department of Mathematics at the University of British Columbia, in cooperation with the Pacific Institute of Mathematical Sciences, is hosting the Foundational Methods in Computer Science workshop from June 1 to June 4, 2000, on the University of British Columbia Campus in Vancouver, B.C., Canada. The workshop is an informal meeting to bring together researchers in mathematics and computer science with a focus on the applications of category theory in computer science. The reception in the evening of June 1, 2000, at Walter Gage Towers, is followed by a day of tutorials aimed at students and newcomers to category theory, followed by a day and a half of research talks. There will be a few invited presentations, but the majority of the talks are solicited from the participants. Student participation is particularly encouraged at FMCS. PARTICIPANT LIST (as of May 1, 2000) Jeremy Bem, University of California, Berkeley David Benson, Washington State University Robin Cockett, University of Calgary Adam Eppendahl, Queen Mary and Westfield College, London Hongge Gao, Northeastern University Michael Johnson, Macquarie University, Sydney John MacDonald, University of British Columbia Ernest Manes, University of Massachusetts at Amherst Stefan Milius, York University Philip Mulry, Colgate University Cristina Pedicchio, University of Trieste Vaughan Pratt, Stanford University Robert Schneck, University of California, Berkeley Robert Seely, McGill University Peter Selinger, University of Michigan Lebelo Serutla, National University of Lesotho Tim Sheard, Oregon Graduate Institute Manuela Sobral, University of Coimbra, Portugal Art Stone, Vancouver Walter Tholen, York University Varmo Vene, Estonia Richard Wood, Dalhousie University Please note that not all of the individuals on the participant list have been confirmed. There still are a few places on the program for research presentations of 20 to 30 minutes. Reduced accommodation and registration rates are available to graduate student participants. Further information about FMCS2000 may be obtained from the conference website at http://www.pims.math.ca/science/2000/fmcs . You may also obtain housing and registration forms by sending email to johnm@math.ubc.ca with subject heading FMCS2000. If you are planning to attend (or might attend) the conference and your name is not on the above list, then please let me know. That way I can keep track of how many people will be attending and also keep you updated. John MacDonald Local organizer, FMCS2000 From rrosebru@mta.ca Sun May 7 12:22:53 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA07745 for categories-list; Sun, 7 May 2000 12:19:36 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200005050934.LAA19091@math.u-strasbg.fr> Date: Fri, 5 May 2000 11:34:37 +0200 (MET DST) From: Philippe Gaucher Reply-To: Philippe Gaucher Subject: categories: derived pasting scheme To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=ISO-8859-1 Content-MD5: w4HYqTJ73B3lYPUag/u3Pw== X-Mailer: dtmail 1.3.0 CDE Version 1.3 SunOS 5.7 sun4u sparc Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id GAA00280 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Bonjour, In Kapranov & Voevodsky, "Combinatorial-geometric aspects of polycategory theory : pasting scheme and higher bruhat orders", Cahiers de topologie et géométrie différentielle catégoriques, Vol XXXII-1 (1991), the authors discuss the problem of the existence of the "derived pasting scheme" of a composable pasting scheme. I would like to know please what have been done on this subject since 1991 ? pg. From rrosebru@mta.ca Sun May 7 12:23:38 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA10008 for categories-list; Sun, 7 May 2000 12:20:26 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 05 May 2000 10:48:58 -0400 From: "Steven R. Costenoble" Subject: categories: Model category structures on Cat To: dmd1@lehigh.edu, categories@mta.ca Message-id: MIME-version: 1.0 X-Mailer: Novell GroupWise 5.5 Content-type: text/plain; charset=US-ASCII Content-disposition: inline Content-transfer-encoding: 7BIT Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Last Fall I asked the Algebraic Topology and Category mailing lists what was known about model category structures on Cat, the category of small categories. For those who are interested, what follows is a summary of what I found. It is, I'm sure, incomplete, and I apologize to anyone whose work I have slighted or missed entirely. The interest and the problem stem from the observation that the nerve functor N induces an equivalence between Cat and the category of simplicial sets, after inverting weak equivalences. The weak equivalences in Cat are, by definition, those maps that become weak equivalences on applying N. This result can be found in the following two sources (but goes back further, to at least Gabriel & Zisman): Thomason, Homotopy colimits in Cat, with applications to algebraic K-theory and loop space theory, Dissertation, Princeton, 1977. Latch, The uniqueness of homology for the category of small categories, J. Pure Appl. Algebra 9, 221-237 (1977). Unfortunately, the left adjoint for N, which is the "categorical realization" functor c, does not give the inverse equivalence. Although the counit cN -> 1 is an isomorphism, the unit 1 -> Nc is far from being a weak equivalence. A related problem is that, if C is a small category, then NC is fibrant iff C is a groupoid. This raises the question: Is there an adjoint pair of functors (L,R): SimpSet -> Cat and a model category structure on Cat with the weak equivalences as above, such that (L,R) induces an adjoint pair of equivalences between the Quillen homotopy categories (i.e., (L,R) is a Quillen equivalence)? Thomason gave an affirmative answer in Thomason, Cat as a closed model category, Cahiers Topologie Geom. Differentielle Categoriques XXI, 305-324 (1980). This followed an attempt by Golasinski in a 1978 preprint which appeared in print as Golasinksi, Homotopies of small categories, Fund. Math. CXIV, 209-217 (1981). Golasinski's proposed structure failed to satisfy the factorization axiom, but does lead to a closed model category on the category of pro-objects in Cat, as shown in Golasinski, On closed models on the precategory of small categories and simplicial schemes, Uspekhi Mat. Nauk 39, 239--240 (1984) (Russian, translated in Russian Math. Surveys 39, 275-276 (1984)). More recently, Heggie defined a class of cofibrations in Cat, in Heggie, Homotopy cofibrations in CAT, Cahiers Topologie Geom. Differentielle Categoriques XXXIII, 291-313 (1992). I haven't had time to compare them, but at first glance these cofibrations appear closely related to Thomason's, if not identical. I also recommend two other papers by Heggie: Heggie, The left derived tensor product of CAT-valued diagrams, Cahiers Topologie Geom. Differentielle Categoriques XXXIII, 33-53 (1992). Heggie, Homotopy colimits in presheaf categories, Cahiers Topologie Geom. Differentielle Categoriques XXXIV, 13-36 (1993). The upshot of all this is that Thomason's is still the only model category structure known (or, at least, published) on Cat making it equivalent to the category of simplicial sets. Besides an aesthetic objection to Thomason's model category structure, I have a practical one: Thomason uses the second subdivision followed by categorical realization as the functor going from simplicial sets to small categories inducing the equivalence of homotopy categories. This functor does not preserve products, as does categorical realization by itself. For various reasons it would be really nice to have a functor that does preserve products and is the left adjoint in a Quillen equivalence. I throw this out as a problem I'd like to work on myself, when I get time. If anyone has any thoughts about it, I'd be happy to hear them. There were other references I came across, answering related but different questions. For example, there is a short, unpublished 1996 manuscript by Charles Rezk giving a very nice model structure on Cat in which the weak equivalences are the equivalences of categories (this was probably folklore for quite a while). There has also been quite a lot of work on model category structures for n-categories and related gadgets; however, when restricted to ordinary categories this work generally gives the homotopy equivalence between the category of simplicial 1-types and the category of small groupoids. --Steve Costenoble From rrosebru@mta.ca Thu May 11 15:34:07 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA03398 for categories-list; Thu, 11 May 2000 15:29:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 11 May 2000 12:26:32 +0100 (BST) From: "T.Porter" Subject: categories: Bangor workshop on orbifolds To: categories@mta.ca Message-ID: MIME-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="-559023410-126398554-958044392=:17056" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. Send mail to mime@docserver.cac.washington.edu for more info. ---559023410-126398554-958044392=:17056 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 Content-Transfer-Encoding: QUOTED-PRINTABLE Dear All, Next September I am organising a small workshop at Bangor on Orbifolds, Groupoids and their Applications. I include an announcement giving some more details. We hope to provide an oportunity to bridge the gap between the categorical(mostly topos theoretic and sheaf theoretic) aspects and the applications (including crystallographic topology, geoemtric group theory etc.). Best wishes, Tim ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: University of Wales, Bangor - School of Informatics, =20 =09=09=09Mathematics Division Workshop on Orbifolds, Groupoids, and their Applications Announcement Workshop Organiser : Prof Tim Porter There will be an informal open workshop at the University of Wales Bangor f= rom 11th - 17th September, 2000, on the interplay between orbifolds and groupoi= ds, together with the application of orbifold methods to problems in crystallography, geometric group theory and equivariant algebraic topology. The aim of the Workshop is to provide a venue for the exchange of information on different aspects of the area and to encourage collaboration across the different subject specialisms that are involved. Some time will = be set aside for examination of the problems where existing techniques seem no= t to be adequate.=20 The workshop is in part to celebrate the work on groupoids, their theory an= d applications, by Ronnie Brown who has recently retired from a full time pro= fessorship a t Bangor. It will also form part of his (belated) 65 birthday celebrations!= =20 The workshop will be informal. Although there will be some survey talks, it= is hoped that the main work will be concentrated on the future in `discussion mode' rather than lecture, (so participants are encouraged to interrupt!!!)= We hope that questions such as to the interpretation of homotopy theoretic information on orbifold, the applicability of current algebraic - topologic= al techniques to problems in `crystallographic topology' and the link between orbifolds and sheaf theory will be addressed. The background of the participants is from various subject areas (crystallography, geometric grou= p theory,=20 category theory etc.) and one task is to find a common language where everyone has a moderate chance of understanding and communicating their questions. There may be some need for quick sketches of background assumptions, theory etc and because of this sessions are likely to be of variable length and the timetable will be (by necessity) flexible.=20 At present the list of participants includes:=20 R.Brown (Groupoids and their applications)=20 A. Haefliger (Geometric group theory, groupoids and geometry)=20 C. Johnson (Crystallographic Topology)=20 I. Moerdijk (Category Theory, orbifolds and toposes)=20 D. Pronk (Sheaves on orbifolds)=20 Various U.K. researchers in differentiable groupoids, equivariant homotopy = and its a pplications and related areas are also expected.=20 Additional participants are very welcome.=20 Accommodation is likely to be in the student village (en-suite facilities) = at a short=20 distance (5 to 10 minutes walk) from the Mathematics building. (Further information about accommodation in and abound Bangor is available.)=20 A small registration fee of =A320 is requested to cover the cost of a works= hop dinner a nd daily coffee/tea etc. We will be seeking some financial support from various organisations so may be able to give limited help to some participa= nts (priority would be given to postgraduates).=20 There will be some space for a display of preprints/ offprints and `posters= '.=20 If you are interested in attending the workshop, contact me by e-mail: t.po= rter@bangor.ac.uk=20 in the first instance. For further information check the workshop home page= =2E=20 =20 ************************************************************ Timothy Porter |tel direct: +44 1248 382492 Mathematics Division,=09=09 |World Wide Web School of Informatics, |home page: http://www.bangor.ac.uk/~mas013/ University of Wales, Bangor |Mathematics and Knots : exhibition Dean St. |http://www.bangor.ac.uk/ma/CPM/ Bangor | Gwynedd LL57 1UT | United Kingdom | ---559023410-126398554-958044392=:17056 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; name="orbifolds.txt" Content-Transfer-Encoding: BASE64 Content-ID: Content-Description: Content-Disposition: attachment; filename="orbifolds.txt" DQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgVW5p dmVyc2l0eSBvZiBXYWxlcywgQmFuZ29yIC0gU2Nob29sIG9mIEluZm9ybWF0 aWNzDQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgIE1hdGhlbWF0aWNzIERpdmlzaW9uDQoNCg0KICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICBXb3Jrc2hvcCBvbg0KICAgICAg ICAgICAgICAgICAgIE9yYmlmb2xkcywgR3JvdXBvaWRzLCBhbmQgdGhlaXIg QXBwbGljYXRpb25zDQoNCg0KDQoNCiAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgQW5ub3VuY2VtZW50DQoNCiAgICAgICAgICAgICAgICAgICAg IFdvcmtzaG9wIE9yZ2FuaXNlciA6IFByb2YgVGltIFBvcnRlcg0KDQpUaGVy ZSB3aWxsIGJlIGFuIGluZm9ybWFsIG9wZW4gd29ya3Nob3AgYXQgdGhlIFVu aXZlcnNpdHkgb2YgV2FsZXMgQmFuZ29yIGZyb20NCjExdGggLSAxN3RoIFNl cHRlbWJlciwgMjAwMCwgb24gdGhlIGludGVycGxheSBiZXR3ZWVuIG9yYmlm b2xkcyBhbmQgZ3JvdXBvaWRzLA0KdG9nZXRoZXIgd2l0aCB0aGUgYXBwbGlj YXRpb24gb2Ygb3JiaWZvbGQgbWV0aG9kcyB0byBwcm9ibGVtcyBpbg0KY3J5 c3RhbGxvZ3JhcGh5LCBnZW9tZXRyaWMgZ3JvdXAgdGhlb3J5IGFuZCBlcXVp dmFyaWFudCBhbGdlYnJhaWMNCnRvcG9sb2d5LiBUaGUgYWltIG9mIHRoZSBX b3Jrc2hvcCBpcyB0byBwcm92aWRlIGEgdmVudWUgZm9yIHRoZSBleGNoYW5n ZSBvZg0KaW5mb3JtYXRpb24gb24gZGlmZmVyZW50IGFzcGVjdHMgb2YgdGhl IGFyZWEgYW5kIHRvIGVuY291cmFnZSBjb2xsYWJvcmF0aW9uDQphY3Jvc3Mg dGhlIGRpZmZlcmVudCBzdWJqZWN0IHNwZWNpYWxpc21zIHRoYXQgYXJlIGlu dm9sdmVkLiBTb21lIHRpbWUgd2lsbCBiZQ0Kc2V0IGFzaWRlIGZvciBleGFt aW5hdGlvbiBvZiB0aGUgcHJvYmxlbXMgd2hlcmUgZXhpc3RpbmcgdGVjaG5p cXVlcyBzZWVtIG5vdCB0byBiZSBhZGVxdWF0ZS4gDQoNClRoZSB3b3Jrc2hv cCBpcyBpbiBwYXJ0IHRvIGNlbGVicmF0ZSB0aGUgd29yayBvbiBncm91cG9p ZHMsIHRoZWlyIHRoZW9yeSBhbmQNCmFwcGxpY2F0aW9ucywgYnkgUm9ubmll IEJyb3duIHdobyBoYXMgcmVjZW50bHkgcmV0aXJlZCBmcm9tIGEgZnVsbCB0 aW1lIHByb2Zlc3NvcnNoaXAgYQ0KdCBCYW5nb3IuIEl0IHdpbGwgYWxzbyBm b3JtIHBhcnQgb2YgaGlzIChiZWxhdGVkKSA2NSBiaXJ0aGRheSBjZWxlYnJh dGlvbnMhIA0KDQpUaGUgd29ya3Nob3Agd2lsbCBiZSBpbmZvcm1hbC4gQWx0 aG91Z2ggdGhlcmUgd2lsbCBiZSBzb21lIHN1cnZleSB0YWxrcywgaXQgaXMN CmhvcGVkIHRoYXQgdGhlIG1haW4gd29yayB3aWxsIGJlIGNvbmNlbnRyYXRl ZCBvbiB0aGUgZnV0dXJlIGluIGBkaXNjdXNzaW9uDQptb2RlJyByYXRoZXIg dGhhbiBsZWN0dXJlLCAoc28gcGFydGljaXBhbnRzIGFyZSBlbmNvdXJhZ2Vk IHRvIGludGVycnVwdCEhISkgV2UNCmhvcGUgdGhhdCBxdWVzdGlvbnMgc3Vj aCBhcyB0byB0aGUgaW50ZXJwcmV0YXRpb24gb2YgaG9tb3RvcHkgdGhlb3Jl dGljDQppbmZvcm1hdGlvbiBvbiBvcmJpZm9sZCwgdGhlIGFwcGxpY2FiaWxp dHkgb2YgY3VycmVudCBhbGdlYnJhaWMgLSB0b3BvbG9naWNhbA0KdGVjaG5p cXVlcyB0byBwcm9ibGVtcyBpbiBgY3J5c3RhbGxvZ3JhcGhpYyB0b3BvbG9n eScgYW5kIHRoZSBsaW5rIGJldHdlZW4NCm9yYmlmb2xkcyBhbmQgc2hlYWYg dGhlb3J5IHdpbGwgYmUgYWRkcmVzc2VkLiBUaGUgYmFja2dyb3VuZCBvZiB0 aGUNCnBhcnRpY2lwYW50cyBpcyBmcm9tIHZhcmlvdXMgc3ViamVjdCBhcmVh cyAoY3J5c3RhbGxvZ3JhcGh5LCBnZW9tZXRyaWMgZ3JvdXAgdGhlb3J5LCAN CmNhdGVnb3J5IHRoZW9yeSBldGMuKSBhbmQgb25lIHRhc2sgaXMgdG8gZmlu ZCBhIGNvbW1vbiBsYW5ndWFnZSB3aGVyZQ0KZXZlcnlvbmUgaGFzIGEgbW9k ZXJhdGUgY2hhbmNlIG9mIHVuZGVyc3RhbmRpbmcgYW5kIGNvbW11bmljYXRp bmcgdGhlaXINCnF1ZXN0aW9ucy4gVGhlcmUgbWF5IGJlIHNvbWUgbmVlZCBm b3IgcXVpY2sgc2tldGNoZXMgb2YgYmFja2dyb3VuZA0KYXNzdW1wdGlvbnMs IHRoZW9yeSBldGMgYW5kIGJlY2F1c2Ugb2YgdGhpcyBzZXNzaW9ucyBhcmUg bGlrZWx5IHRvIGJlIG9mDQp2YXJpYWJsZSBsZW5ndGggYW5kIHRoZSB0aW1l dGFibGUgd2lsbCBiZSAoYnkgbmVjZXNzaXR5KSBmbGV4aWJsZS4gDQoNCkF0 IHByZXNlbnQgdGhlIGxpc3Qgb2YgcGFydGljaXBhbnRzIGluY2x1ZGVzOiAN Cg0KICAgICAgUi5Ccm93biAoR3JvdXBvaWRzIGFuZCB0aGVpciBhcHBsaWNh dGlvbnMpIA0KICAgICAgQS4gSGFlZmxpZ2VyIChHZW9tZXRyaWMgZ3JvdXAg dGhlb3J5LCBncm91cG9pZHMgYW5kIGdlb21ldHJ5KSANCiAgICAgIEMuIEpv aG5zb24gKENyeXN0YWxsb2dyYXBoaWMgVG9wb2xvZ3kpIA0KICAgICAgSS4g TW9lcmRpamsgKENhdGVnb3J5IFRoZW9yeSwgb3JiaWZvbGRzIGFuZCB0b3Bv c2VzKSANCiAgICAgIEQuIFByb25rIChTaGVhdmVzIG9uIG9yYmlmb2xkcykg DQoNClZhcmlvdXMgVS5LLiByZXNlYXJjaGVycyBpbiBkaWZmZXJlbnRpYWJs ZSBncm91cG9pZHMsIGVxdWl2YXJpYW50IGhvbW90b3B5IGFuZCBpdHMgYQ0K cHBsaWNhdGlvbnMgYW5kIHJlbGF0ZWQgYXJlYXMgYXJlIGFsc28gZXhwZWN0 ZWQuIA0KDQpBZGRpdGlvbmFsIHBhcnRpY2lwYW50cyBhcmUgdmVyeSB3ZWxj b21lLiANCg0KQWNjb21tb2RhdGlvbiBpcyBsaWtlbHkgdG8gYmUgaW4gdGhl IHN0dWRlbnQgdmlsbGFnZSAoZW4tc3VpdGUgZmFjaWxpdGllcykgYXQgYSBz aG9ydCANCmRpc3RhbmNlICg1IHRvIDEwIG1pbnV0ZXMgd2FsaykgZnJvbSB0 aGUgTWF0aGVtYXRpY3MgYnVpbGRpbmcuIChGdXJ0aGVyDQppbmZvcm1hdGlv biBhYm91dCBhY2NvbW1vZGF0aW9uIGluIGFuZCBhYm91bmQgQmFuZ29yIGlz IGF2YWlsYWJsZS4pIA0KDQpBIHNtYWxsIHJlZ2lzdHJhdGlvbiBmZWUgb2Yg ozIwIGlzIHJlcXVlc3RlZCB0byBjb3ZlciB0aGUgY29zdCBvZiBhIHdvcmtz aG9wIGRpbm5lciBhDQpuZCBkYWlseSBjb2ZmZWUvdGVhIGV0Yy4gV2Ugd2ls bCBiZSBzZWVraW5nIHNvbWUgZmluYW5jaWFsIHN1cHBvcnQgZnJvbQ0KdmFy aW91cyBvcmdhbmlzYXRpb25zIHNvIG1heSBiZSBhYmxlIHRvIGdpdmUgbGlt aXRlZCBoZWxwIHRvIHNvbWUgcGFydGljaXBhbnRzDQoocHJpb3JpdHkgd291 bGQgYmUgZ2l2ZW4gdG8gcG9zdGdyYWR1YXRlcykuIA0KDQpUaGVyZSB3aWxs IGJlIHNvbWUgc3BhY2UgZm9yIGEgZGlzcGxheSBvZiBwcmVwcmludHMvIG9m ZnByaW50cyBhbmQgYHBvc3RlcnMnLiANCg0KSWYgeW91IGFyZSBpbnRlcmVz dGVkIGluIGF0dGVuZGluZyB0aGUgd29ya3Nob3AsIGNvbnRhY3QgbWUgYnkg ZS1tYWlsOiB0LnBvcnRlckBiYW5nb3IuYWMudWsgDQppbiB0aGUgZmlyc3Qg aW5zdGFuY2UuIEZvciBmdXJ0aGVyIGluZm9ybWF0aW9uIGNoZWNrIHRoZSB3 b3Jrc2hvcCBob21lIHBhZ2UuIA0KDQoNCg0KDQo= ---559023410-126398554-958044392=:17056-- From rrosebru@mta.ca Thu May 11 15:34:07 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA05958 for categories-list; Thu, 11 May 2000 15:28:48 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 11 May 2000 17:36:05 +1000 (EST) From: CATS 01 Conference Message-Id: <200005110736.RAA18755@everest.it.uq.edu.au> Subject: categories: Call for Papers: CATS 2001 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Call for Papers CATS 2001 - Computing: The Australasian Theory Symposium Computing: The Australasian Theory Symposium (CATS) is the premier theoretical computer science conference in Australasia. It is held annually as part of Australasian Computer Science Week (ACSW). CATS 2001 will be the seventh in the series. The symposium will consist of invited speakers and research paper presentations. DATE AND LOCATION CATS 2001 will be held over two days during Australasian Computer Science Week. ACSW 2001 will take place at Bond University, Gold Coast, Queensland, Australia, from 29th January to 2nd February 2001. SCOPE CATS covers all aspects of theoretical computer science. Some representative, but not exclusive, topics include the following: - logic, reasoning and verification - formal specification techniques and program semantics - formal development methods, program refinement, synthesis and transformation - concurrent, parallel and distributed system theory - theory of algorithms and data structures - complexity and computability - automata, number and category theory - tools for automated reasoning, and program analysis and development KEYNOTE ADDRESSES Prof Mathai Joseph, Tata Research Development and Design Centre, Pune, India Prof Carroll Morgan, Software Engineering Research Group, Department of Computer Science and Engineering, University of New South Wales CALL FOR PAPERS Research paper submissions to CATS 2001 should be prepared according to the formatting requirements below and sent to the Programme Chair, to arrive no later than August 4, 2000. Submissions must be original work, not published or submitted elsewhere. All submissions will be refereed. PROCEEDINGS The proceedings of CATS 2001 will be published by Elsevier Science in their series Electronic Notes in Theoretical Computer Science. ENTCS is an electronic series associated with the journal Theoretical Computer Science, and published by Elsevier Science B. V. (Institutions subscribing to TCS can access full papers in ENTCS on-line.) ENTCS offers rapid, worldwide dissemination of research results, an absence of page limits, and long-term accessibility through the electronic archives that Elsevier maintains. (The proceedings of last year's CATS 2000 conference appeared as ENTCS Volume 31.) A hardcopy preliminary proceedings will be provided to conference attendees. Authors of selected papers from the CATS 2001 proceedings will be invited to submit extended versions of their papers to a Special Issue of the journal Theoretical Computer Science. FORMATTING REQUIREMENTS To ensure a uniform format for papers, all submissions to CATS 2001 must be prepared in LaTeX using the ENTCS macros. Papers in other formats cannot be accepted. Further information is available via the ENTCS home page: http://www.elsevier.nl/locate/entcs/. (Follow the links for "Instructions for Submissions" and "Technical Requirements".) Complete papers should be e-mailed as PostScript files, preferably as MIME attachments. Although there is no strict page limit on submissions to CATS 2001, authors are strongly encouraged to be as concise as possible. Papers between 10 and 15 pages are considered ideal. If necessary, definitions and proofs not essential to understanding the paper should be relegated to appendices to appear only in the electronic version. CALL FOR POSTERS A poster session will be arranged to give CATS attendees the opportunity to give informal presentations of their work. Expressions of interest, briefly outlining the poster's topic, should be e-mailed to the Programme Chair by November 10, 2000. IMPORTANT DATES Friday 4 August 2000: Deadline for submissions Friday 6 October 2000: Notification of acceptance Friday 27 October 2000: Final versions of accepted papers due Friday 10 November 2000: Deadline for author registrations Monday 29 January to Friday 2 February 2001: Australasian Computer Science Week, incorporating CATS 2001 PROGRAMME COMMITTEE Mariangiola Dezani-Ciancaglini, Universita di Torino, Italy Rod Downey, Victoria University of Wellington, New Zealand Colin Fidge (Chair), The University of Queensland, Australia Lance Fortnow, NEC Research Institute, USA Joseph Goguen, University of California at San Diego, USA Andrew Martin, Oxford University, United Kingdom Ian Mason, University of New England, Australia Janos Pach, New York University, USA Igor Shparlinski, Macquarie University, Australia Mark Utting, University of Waikato, New Zealand Emo Welzl, ETH Zurich, Switzerland ACSW GENERAL CHAIR Gopal Gupta, Bond University UPDATES AND NEWS Up to date information about the CATS 2001 conference can be found at its web site: http://www.csee.uq.edu.au/~cats01/ ENQUIRIES AND SUBMISSIONS Dr Colin Fidge (CATS 2001 Programme Chair) Software Verification Research Centre The University of Queensland Queensland 4072 Australia Fax: +61 7 3365 1533 Email: cats01@svrc.uq.edu.au From rrosebru@mta.ca Sat May 13 11:28:05 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA29502 for categories-list; Sat, 13 May 2000 11:23:39 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <391B032C.A88C6BF0@kestrel.edu> Date: Thu, 11 May 2000 11:59:56 -0700 From: Lindsay Errington Organization: Kestrel Institute X-Mailer: Mozilla 4.72 [en] (X11; U; Linux 2.2.14-5.0 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: process algebras References: <200004171557.QAA06124@koi-pc.dcs.qmw.ac.uk> <38FEFCD1.A189A453@info.unine.ch> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: > Is there any formalization of process algebras in term of categories? I > would be interested in giving an computational, multi-process semantics > to certain graphs, and I thought it could be done in terms of a functor > to a process category (if this concept exists...) > Is there any literature about this? I have a CTCS99 paper ``On the semantics of message passing processes'' at http://theory.doc.ic.ac.uk/~le which may be relevant. As the title suggests, it looks at categorical semantics for a CSP-like language with assignment. It is related to the work mentioned by Robin and Dusko. Also, the conclusions of my thesis discusses representing process networks as diagrams in a category of processes. This might be related to your comment above. Lindsay From rrosebru@mta.ca Sat May 13 11:29:23 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA29171 for categories-list; Sat, 13 May 2000 11:27:38 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <20000512080536.12502.qmail@hotmail.com> X-Originating-IP: [198.168.191.180] From: "Marta Bunge" To: categories@mta.ca Subject: categories: Preprint: Distribution Algebras and Duality Date: Fri, 12 May 2000 04:05:36 EDT Mime-Version: 1.0 Content-Type: text/plain; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: This is to announce the availability of a paper : M. Bunge, J. Funk, M. Jibladze and T. Streicher, "Distribution Algebras and Duality" (.dvi, .ps) posted at the site: http://www.math.mcgill.ca/~bunge/disalg.dvi http://www.math.mcgill.ca/~bunge/disalg.ps Marta Bunge ________________________________________________________________________ Get Your Private, Free E-mail from MSN Hotmail at http://www.hotmail.com From rrosebru@mta.ca Sun May 14 20:06:04 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA11581 for categories-list; Sun, 14 May 2000 19:59:36 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mailing-List: contact fme2001cfp-help@di.uminho.pt; run by ezmlm X-No-Archive: yes Delivered-To: mailing list fme2001cfp@di.uminho.pt Date: Fri, 12 May 2000 18:56:56 +0100 From: "Jose N. Oliveira" To: fme2001cfp@di.uminho.pt Subject: categories: FME 2001: Call for Papers Message-ID: <20000512185656.A1397@seide.di.uminho.pt> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0pre3i Organization: Univ. do Minho Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: FORMAL METHODS EUROPE FME 2001 "Formal Methods for Increasing Software Productivity" International Symposium and Tutorials 12-16 March 2001 Humboldt-Universitaet zu Berlin, Germany (http://www.informatik.hu-berlin.de/top/fme2001) Call for Submissions ******************** FME 2001 is the tenth in a series of symposia organised by Formal Methods Europe, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. These symposia have been notably successful in bringing together a community of users, researchers, and developers of precise mathematical methods for software development. The theme of FME 2001 is Formal Methods for Increasing Software Productivity. This theme recognizes that formal methods have the potential to do more for industrial software development than enhance software quality--they can also increase productivity at many different points in the software life-cycle. The symposium committee is particularly interested in papers on the use of formal methods to increase productivity, for example on: * Codifying domain knowledge * Re-using components * Automatically generating code and/or documentation * Improving the efficiency of software testing * Enhancing analysis techniques for validation and verification * Exploiting commonalities within product families * Improving the maintainability and modifiability of software * Empirical studies of effects on productivity SCOPE The scope of the symposium, as always in its distinguished history, also includes all other aspects of the use of formal methods, for development of software in all application areas. The scope of the symposium covers the entire range from fundamental theory of description and reasoning to particulars of practice and experience. In addition to presentations of submitted papers, the symposium will also offer tutorials, workshops, invited speakers, and tool demonstrations. PAPERS The symposium committee solicits full-length papers in two broad categories: 1. Use of formal methods, including reports on industrial use, substantial case studies, comparisons among methods, education, and technology transfer. 2. Development of formal methods, including motivating factors, theoretical foundations, extensions, manual procedures, and tool support. Authors are requested to mention the category (1 or 2) of their papers when they submit. Full papers should be submitted in Postscript or PDF format by E-mail to reach fme2001sub@di.uminho.pt by 25th August, 2000. There are no fixed page limits on submissions but authors are warned that papers exceeding twenty A4 pages will be regarded as long, and that the content must justify the length. TUTORIALS Tutorials will be held on 12-13th March. Each tutorial will last one-half or one day. Proposals for tutorials are welcome, and should be directed to the programme chairs. WORKSHOPS Proposals for parallel workshops are welcome, and should be directed to the programme chairs. TOOL DEMONSTRATIONS Tool demonstrations will take place during the symposium, with the opportunity for presentations to be made about each tool. Proposals for tool demonstrations are welcome and should be made to the organising chairs, with whom provision of necessary computing facilities should be discussed. PEOPLE Organising Co-Chairs Stefan Jaehnichen Wolfgang Reisig Organising Committee BWO Marketing Service Birgit Heene Adrianna Foremniak Axel Martens Programme Co-Chairs Jose Oliveira, Dept. Informatica, Universidade do Minho, Campus de Gualtar, 4700-320 Braga, Portugal Tel: +351 253 604 470 E-mail: jno@di.uminho.pt Pamela Zave, AT&T Laboratories, 180 Park Avenue, Florham Park, NJ 07932, USA Tel: +1 973 360 8676 E-mail: pamela@research.att.com Programme Committee Eerke Boiten University of Kent at Canterbury Rick Butler NASA Langley Research Center Lars-Henrik Eriksson Industrilogik L4i AB John Fitzgerald Centre for Software Reliability, Newcastle, UK Peter Gorm Larsen IFAD Yves Ledru Universite Joseph Fourier - Grenoble Dominique Mery Universite Henri Poincare - Nancy Jayadev Misra University of Texas at Austin Richard Moore United Nations University IIST Friederike Nickl F.A.S.T. GmbH Tobias Nipkow Technische Universitaet Muenchen Jose Oliveira (co-chair) Universidade do Minho Paritosh Pandya TIFR Mumbai, India Nico Plat Cap Gemini Amir Pnueli Weizmann Institute Augusto Sampaio Universidade Federal de Pernambuco Steve Schneider Royal Holloway, University of London Jim Woodcock Oxford University Pamela Zave (co-chair) AT&T Laboratories IMPORTANT DATES Deadline for submission of papers, tutorial proposals, and workshop proposals: 25th August, 2000 Notification of acceptance/rejection: 17th November, 2000 Camera ready final version of papers due: 5th January, 2001 From rrosebru@mta.ca Sun May 14 20:06:06 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA32246 for categories-list; Sun, 14 May 2000 20:00:35 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 12 May 2000 10:26:58 +0100 (BST) From: "T.Porter" Subject: categories: URL for workshop To: categories@mta.ca Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear All, OOPS I forgot the URL which got left off. http://www.bangor.ac.uk/ma/news/orbifold/welcome.html Thanks Tim ************************************************************ Timothy Porter |tel direct: +44 1248 382492 Mathematics Division, |World Wide Web School of Informatics, |home page: http://www.bangor.ac.uk/~mas013/ University of Wales, Bangor |Mathematics and Knots : exhibition Dean St. |http://www.bangor.ac.uk/ma/CPM/ Bangor | Gwynedd LL57 1UT | United Kingdom | From rrosebru@mta.ca Tue May 16 01:15:54 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id BAA12903 for categories-list; Tue, 16 May 2000 01:10:15 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: street@hera.mpce.mq.edu.au Message-Id: X-Priority: 1 (Highest) Date: Mon, 15 May 2000 16:56:17 +1000 To: categories@mta.ca From: Ross Street Subject: categories: Kelly Volume Content-Type: text/plain; charset="iso-8859-1" ; format="flowed" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id DAA00867 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear Mathematicians Our colleague Max Kelly turns 70 on 5 June 2000. To commemorate this milestone, and in recognition of Max's significant contribution to mathematics (especially category theory), there will be a special volume of the Journal of Pure and Applied Algebra dedicated him. The appropriateness of this Journal is clear as Max has been on the editorial board since its inception. The Editors for this special volume will be Aurelio Carboni (representing the regular editorial board), George Janelidze and me (as guest editors). We hereby call for submission of papers. We would like those of you have published with Max, worked with him, used his results, or simply respected his work, to consider contributing a research article. The standards of the Journal will be upheld by the usual refereeing procedure. ****The deadline for submission is 28 November 2000.**** Please send your article to one of the editors: A. Carboni Universitŕ degli Studi dell'Insubria Dipartimento di Scienze Chimiche, Fisiche e Matematiche Via Lucini 3 22100 Como ITALY E-mail: , Professor George Janelidze Departamento de Matematica Universidade de Aveiro 3810-193 Aveiro PORTUGAL Email: , Professor Ross Street Mathematics Department Macquarie University N. S. W. 2109 AUSTRALIA Email: Sincerely, Ross From rrosebru@mta.ca Tue May 16 01:15:54 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id BAA04328 for categories-list; Tue, 16 May 2000 01:11:01 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: S.J.Vickers@open.ac.uk Message-ID: To: categories@mta.ca Subject: categories: "maps to" Date: Mon, 15 May 2000 09:17:24 +0100 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2650.21) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: [This is not exclusively category theory, I know, but I think the categories list members are the sort of people who might know the answer.] Does anyone know the origins of "|->" as symbol for "maps to", e.g. defining a function by x |-> 3x + 5 ? Steve Vickers. From rrosebru@mta.ca Tue May 16 09:47:04 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA00955 for categories-list; Tue, 16 May 2000 09:45:52 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39212879.AE40DEF3@tcs.inf.tu-dresden.de> Date: Tue, 16 May 2000 03:52:41 -0700 From: Kai Bruennler X-Mailer: Mozilla 4.72 [en] (X11; U; Linux 2.2.12-20 i586) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: associative product in Set Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Is there a binary product in the category of sets and functions that is "strictly associative", i.e. A x (B x C) = (A x B) x C and the associativity isomorphisms are equal to the identity? Thanks. Kai From rrosebru@mta.ca Tue May 16 12:54:45 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA13372 for categories-list; Tue, 16 May 2000 12:53:50 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: PhD positions in Logics, Types, Rewriting adn Automation Message-Id: From: Fairouz Kamareddine Date: Tue, 16 May 2000 11:21:32 +0100 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: The ULTRA group (Useful Logics, Types, Rewriting and Automation) HERIOT-WATT UNIVERSITY Department of Computing and Electrical Engineering EPSRC PhD Studentships The department has a number of studentships available for UK and EU nationals to undertake research leading to a PhD. We encourage the applications of those interested in any of the areas below: 1. the study and automation of logics, type theories, and rewriting theory 2. the logical/type theoretical foundations of programming languages, the formalization of mathematics, and theorem proving. 3. the design and implementation of programming langauges and theorem provers. 4. The Lambda calculus. Candidates should hold or expect to hold a good honours degree or the equivalent. Further information about applications and research projects we offer at the ULTRA group can be obtained by contacting Professor Fairouz Kamareddine (fairouz@cee.hw.ac.uk) Further details of the ULTRA group can be found on: http://www.cee.hw.ac.uk/ultra/ From rrosebru@mta.ca Tue May 16 12:56:00 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA29580 for categories-list; Tue, 16 May 2000 12:55:57 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: duskin@mail.buffnet.net Message-Id: In-Reply-To: References: Date: Tue, 16 May 2000 10:06:18 -0400 To: categories@mta.ca From: John Duskin Subject: categories: Re: "maps to" Content-Type: multipart/alternative; boundary="============_-1253636508==_ma============" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: --============_-1253636508==_ma============ Content-Type: text/plain; charset="us-ascii" ; format="flowed" >[This is not exclusively category theory, I know, but I think the categories >list members are the sort of people who might know the answer.] > >Does anyone know the origins of "|->" as symbol for "maps to", e.g. defining >a function by > x |-> 3x + 5 ? > >Steve Vickers. I don't know who invented the "vertical bar-arrow" notation but I do have a pretty good idea of how and why it caught on, and it is related to the rise of category theory where the use of arrows proliferates and a real need arises for some notational distinction between using an arrow to denote a mapping X--->F(X) as, for example, the value at an object X of a natural transformation from the the identity functor to some endofunctor F and the correspondence X--->F(X) which defines the functor itself. In the early sixties, Grothendieck started using a "very wiggly arrow" X~~~>F(X) to denote the correspondence (curiously, always drawn in by hand--not with repeated "~" on the typewriter) and this notation caught on, at least with those who studied with him at that time, and even survives today (e.g., in Mike Artin's recent and beautiful "undergraduate" text, Algebra). Moreover, in the early seventies, seeing those very noticeable wiggles in a book or paper immediately provoked attention ("What the hell is that?") and made the book or paper look "very up to date" (or,more derisively, "very trendy"). Undergraduate Calculus texts had already been using arrows (" x--->3x+5" instead of "y=3x+5" ) not only to try to convey the idea of a mapping but also to look "very up to date". Being told that the "correct" notation for this was now "x~~~>3x+5", publishers were faced with the very expensive problem (in those days before Tex) of re-typesetting their heretofore trivially revised ("just mix up the exercise problem numbers and correct a few misprints") 5th and 6th editions with a 7th edition in which every every arrow "--->" would have to be replaced by " ~~~>" if the text were to remain "up to date". Someone--I wish I knew whom-- had the authority and the temerity to suggest that " x|--> 3x+5" would be a less intrusive and certainly less expensive solution to both the logical and the economic problem. It caught on almost immediately and survives to this day. The "very wiggly arrow" would still be a pretty good notation to indicate a " lax" or pseudo-functor, but as far as I can see, it hasn't been adopted even for that purpose. It does survive (if somewhat diminutively) as "\leadsto" in the "arrow and pointers" math fonts of Tex. --============_-1253636508==_ma============ Content-Type: text/enriched; charset="us-ascii" [This is not exclusively category theory, I know, but I think the categories list members are the sort of people who might know the answer.] Does anyone know the origins of "|->" as symbol for "maps to", e.g. defining a function by x |-> 3x + 5 ? Steve Vickers. I don't know who invented the "vertical bar-arrow" notation but I do have a pretty good idea of how and why it caught on, and it is related to the rise of category theory where the use of arrows proliferates and a real need arises for some notational distinction between using an arrow to denote a mapping X--->F(X) as, for example, the value at an object X of a natural transformation from the the identity functor to some endofunctor F and the correspondence X--->F(X) which defines the functor itself. In the early sixties, Grothendieck started using a "very wiggly arrow" X~~~>F(X) to denote the correspondence (curiously, always drawn in by hand--not with repeated "~" on the typewriter) and this notation caught on, at least with those who studied with him at that time, and even survives today (e.g., in Mike Artin's recent and beautiful "undergraduate" text, Algebra). Moreover, in the early seventies, seeing those very noticeable wiggles in a book or paper immediately provoked attention ("What the hell is that?") and made the book or paper look "very up to date" (or,more derisively, "very trendy"). Undergraduate Calculus texts had already been using arrows (" x--->3x+5" instead of "y=3x+5" ) not only to try to convey the idea of a mapping but also to look "very up to date". Being told that the "correct" notation for this was now "x~~~>3x+5", publishers were faced with the very expensive problem (in those days before Tex) of re-typesetting their heretofore trivially revised ("just mix up the exercise problem numbers and correct a few misprints") 5th and 6th editions with a 7th edition in which every every arrow "--->" would have to be replaced by " ~~~>" if the text were to remain "up to date". Someone--I wish I knew whom-- had the authority and the temerity to suggest that " x|--> 3x+5" would be a less intrusive and certainly less expensive solution to both the logical and the economic problem. It caught on almost immediately and survives to this day. The "very wiggly arrow" would still be a pretty good notation to indicate a " lax" or pseudo-functor, but as far as I can see, it hasn't been adopted even for that purpose. It does survive (if somewhat diminutively) as "\leadsto" in the "arrow and pointers" math fonts of Tex. --============_-1253636508==_ma============-- From rrosebru@mta.ca Tue May 16 12:57:02 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA22945 for categories-list; Tue, 16 May 2000 12:56:59 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200005161440.HAA02548@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: associative product in Set Date: Tue, 16 May 2000 07:40:32 -0700 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: >Is there a binary product in the category of sets and functions that is >"strictly associative", i.e. > >A x (B x C) = (A x B) x C and >the associativity isomorphisms are equal to the identity? Categorically speaking this question is undecidable. The question has different answers for equivalent copies of Set. Isbell points out (reported in CTWM, end of VII-1) that if Set (or any subcategory thereof containing a countably infinite set) is skeletal, on-the-nose associativity is impossible. Stacy Finkelstein in her thesis (or at least in a talk on Tau Categories that I recall as being based on her thesis) gave a subcategory of Set consisting of ordinals up to w^w and their (order-ignoring) functions with an on-the-nose product. In the course of the discussion following my question of 3/11/96 to this list about the relative ease of defining set membership and composition in terms of each other, I posted a similar construction (on 3/14/96) for the whole of Set (more precisely, for a subcategory of Set consisting of those sets that can be well-ordered, more precisely yet Ord(inals) and their (order-ignoring) functions). (I learned about Stacy's construction shortly thereafter.) These latter versions of Set are of course not skeletal by virtue of distinct ordinals (w, w+1, etc.) being isomorphic, necessary by Isbell's observation. Whereas my set-membership question and its subsequent lengthy discussion were I gather appreciated by many, the reactions to the on-the-nose product I posted as part of it varied from indifference to outright hostility. On reflection these reactions, coming from category theorists, are entirely consistent with the categorical undecidability of whether Set admits on-the-nose product. Vaughan Pratt From rrosebru@mta.ca Tue May 16 12:57:33 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA07941 for categories-list; Tue, 16 May 2000 12:57:26 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Tue, 16 May 2000 16:55:28 +0100 To: categories@mta.ca From: grandis@dima.unige.it (Marco Grandis) Subject: categories: Finitely presentable presheaves Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Consider the category of presheaves C^ on a small category, C. Plainly, a finite colimit F of representables presheaves is finitely presentable, in the usual sense: C^(F, -) preserves filtered colimits. But the converse is also true and seemingly well known: every finitely presentable presheaf is a finite colimit of representables. Is this proved somewhere? Best regards Marco Grandis Dipartimento di Matematica Universita' di Genova via Dodecaneso 35 16146 GENOVA, Italy e-mail: grandis@dima.unige.it tel: +39.010.353 6805 fax: +39.010.353 6752 http://www.dima.unige.it/STAFF/GRANDIS/ ftp://pitagora.dima.unige.it/WWW/FTP/GRANDIS/ From rrosebru@mta.ca Wed May 17 08:44:39 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA16540 for categories-list; Wed, 17 May 2000 08:35:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: S.J.Vickers@open.ac.uk Message-ID: To: categories@mta.ca Subject: categories: RE: Finitely presentable presheaves Date: Wed, 17 May 2000 09:04:17 +0100 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2650.21) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: > Consider the category of presheaves C^ on a small category, C. > > Plainly, a finite colimit F of representables presheaves is finitely > presentable, in the usual sense: C^(F, -) preserves > filtered colimits. > But the converse is also true and seemingly well known: every finitely > presentable presheaf is a finite colimit of representables. > > Is this proved somewhere? I think this is obvious from the fact that the theory of presheaves over C is many sorted, essentially algebraic (a finite limit theory), with a sort for each object of C and a unary operator for each morphism. Then finitely presentable in the categorical sense is the same as finitely presentable in the algebraic sense, which is equivalent to being a finite colimit of free cyclic (i.e. one generator) algebras. In the case of presheaves, Yoneda's lemma says precisely that the free algebra on a generator of sort X (object of C) is the representable presheaf for X. I have exploited some of these facts in a paper with my PhD student Gillian Hill, "Presheaves as configured specifications". It develops a language for specifying systems by components with sharing. Steve Vickers. From rrosebru@mta.ca Wed May 17 10:10:54 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA05273 for categories-list; Wed, 17 May 2000 09:50:54 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.20000516162516.009e5900@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 16 May 2000 16:26:16 -0400 To: categories@mta.ca From: Charles Wells Subject: categories: Re: Maps to Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Minor observation on Jack Duskin's message: Most American typewriters in the sixties did not have a "~" character. I presume that was true of Grothendieck's as well. Charles Wells, Oberlin, Ohio, USA. email: charles@freude.com. home phone: 440 774 1926. professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm From rrosebru@mta.ca Tue May 16 09:47:04 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA00955 for categories-list; Tue, 16 May 2000 09:45:52 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39212879.AE40DEF3@tcs.inf.tu-dresden.de> Date: Tue, 16 May 2000 03:52:41 -0700 From: Kai Bruennler X-Mailer: Mozilla 4.72 [en] (X11; U; Linux 2.2.12-20 i586) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: associative product in Set Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Is there a binary product in the category of sets and functions that is "strictly associative", i.e. A x (B x C) = (A x B) x C and the associativity isomorphisms are equal to the identity? Thanks. Kai From rrosebru@mta.ca Wed May 17 12:37:22 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA32201 for categories-list; Wed, 17 May 2000 12:33:42 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 17 May 2000 10:46:52 -0400 (EDT) From: Peter Freyd Message-Id: <200005171446.KAA01340@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Bruennler question Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Kai Bruennler asks: Is there a binary product in the category of sets and functions that is "strictly associative", i.e. A x (B x C) = (A x B) x C and the associativity isomorphisms are equal to the identity? The answer is yes if you're willing to use a lot of choice. Perhaps the quickest construction is to assume a well-ordering on the universe with the property that x < y whenever x \in y. Then define the pair l:AxB --> A, r:AxB --> B by stipulating that AxB is a von Neumann ordinal "lexicagraphically ordered" by l and r, that is, (lx < ly) or (lx = ly and rx < ry) whenever (x \in y) and (y \in AxB). From rrosebru@mta.ca Wed May 17 22:41:35 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id WAA31889 for categories-list; Wed, 17 May 2000 22:40:28 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 17 May 2000 16:09:34 -0400 (EDT) From: Peter Freyd Message-Id: <200005172009.QAA20086@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Products redone Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Kai Bruennler asked: Is there a binary product in the category of sets and functions that is "strictly associative", i.e. A x (B x C) = (A x B) x C and the associativity isomorphisms are equal to the identity? I gave a construction using the axiom of choice. Well, we can do better. Fix on an ordered-pair construction, say Weiner's, and denote its values as . Let l be the left-coordinate function, r the right-coordinate function. Fix on a sequence of finite ordinals, say von Neumann's. Define, inductively, an n-TUPLE as something of the form where y is a (n-1)-tuple if n>1 else any old set if n=1. (There are no 0-tuples.) Note that the same set can be an n-tuple for any number of values for n. But if x is an n-tuple and we are given n then each of it's n coordinates is well-defined: x_1 = lx x_2 = l(rx) ... x_{n-1} = l(r(r(...r(rx)...))) x_n = r(r(r(...r(rx)...))) where there are i-1 applications of r used for x_i, one application of l used for x_i if i where x is an n-tuple such that x_i \in a_i each relevant i. If two sets x and y arise as pre-products, that is, if there are positive ordinals m and n and sets a_1, a_2,..., a_m, b_1, b_2, ...,b_n such that x is the pre-product of the a's and y is the product of the b's, then we define their PRODUCT as the (m+n)-fold pre-product of a_1, a_2,..., a_m, b_1, b_2,...,b_n. Define F(x) = x if x is a pre-product else { | y \in x}. Define the product of arbitrary x and y as the product of F(x) and F(y). From rrosebru@mta.ca Fri May 19 14:16:35 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA27641 for categories-list; Fri, 19 May 2000 14:09:43 -0300 (ADT) Date: Sat, 20 May 2000 08:15:05 +0530 Message-Id: <200005200245.IAA07183@cse.iitd.ernet.in> X-Authentication-Warning: localhost.localdomain: sanjiva set sender to sanjiva@sanjiva.cse.iitd.ernet.in using -f From: Sanjiva Prasad To: skapoor@cse.iitd.ernet.in Subject: categories: FSTTCS 2000: revised Call for Papers Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: --text follows this line-- *********************************************************************** * * * FST TCS 2000 * * * * Foundations of Software Technology and Theoretical Computer Science * * December 13--15, 2000 * * New Delhi, India * * * *********************************************************************** * Call for Papers * *********************************************************************** New: Electronic Submission Guidelines Revised list of Invited Speakers ********************************************************************** IARCS, the Indian Association for Research in Computing Science, announces the 20th Annual FST TCS Conference in New Delhi. Tentatively planned satellite events include include two workshops: on Computational Geometry and on Advances in Programming Languages. Authors are invited to submit papers presenting original and unpublished research on **any** theoretical aspects of Computer Science. Papers in applied areas with a strong foundational emphasis are also welcome. The proceedings of the last six years' conferences (Springer-Verlag Lecture Notes in Computer Science volumes 880, 1026, 1180, 1346, 1530, 1738) give an idea of the kind of papers typically presented at FST TCS. Typical areas include (but are not restricted to): Automata, Languages and Computability Randomized and Approximation Algorithms Computational Geometry Computational Biology Combinatorial Optimization Graph and Network Algorithms Complexity Theory Parallel and Distributed Computing New Models of Computation Concurrent, Real-time and Hybrid Systems Logics of Programs and Modal Logics Database Theory and Information Retrieval Automated Reasoning, Rewrite Systems, and Applications Logic, Proof Theory, Model Theory and Applications Semantics of Programming Languages Static Analysis and Type Systems Theory of Functional and Constraint-based Programming Software Specification and Verification Cryptography and Security Protocols For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper at the conference. Important Dates --------------- Deadline for Submission 31 May, 2000 Notification to Authors 15 August, 2000 Final Version of Accepted Papers due 15 September, 2000 Deadline for Early Registration 15 November, 2000 Submission Guidelines - --------------------- Authors may submit drafts of full papers or extended abstracts. Submissions are limited to 12 A4-size pages, with 1.5 inch top margin and other margins 1 inch wide with 11 point or larger font. Authors who feel that more details are necessary may include a clearly marked appendix which will be read at the discretion of the Programme Committee. Each paper should contain a short abstract. If available, e-mail addresses and fax numbers of the authors should be included. Electronic Submissions - -------------------- Electronic submission is very strongly encouraged. You may submit your paper using Rich Gerber's system START by visiting the URL for the conference and following the appropriate links. The URL for submissions is http://www.cse.iitd.ernet.in/~fsttcs20/START/www/submit.html In case you ar eunable to submit using START, self-contained uuencoded gzipped Postscript versions of the paper may be sent by e-mail to fsttcs20@cse.iitd.ernet.in In addition, the following information in ASCII format should be sent to this address in a **separate** e-mail: Title; authors; communicating author's name, address, and e-mail address and fax number if available; abstract of paper. Hard-Copy Submissions - --------------------- If electronic submission is not possible, authors may submit five (5) hard-copies of the paper by post to the following address: FST TCS 2000 Department of Computer Science and Engineering I.I.T., Delhi Hauz Khas New Delhi 110 016 INDIA Invited Speakers ---------------- Invited Speakers who have confirmed participation include: Peter Buneman (U Penn) Bernard Chazelle (Princeton) E. Allen Emerson (U Texas, Austin) Martin Groetschel (ZIB) Jose Meseguer (SRI) Philip Wadler (Bell Labs) Programme Committee ------------------- Pankaj Agarwal (Duke) Manindra Agrawal (IIT, Kanpur) Tetsuo Asano (JAIST) Vijay Chandru (IISc, Bangalore) Rance Cleaveland (Stony Brook) Anuj Dawar (Cambridge) Sampath Kannan (AT&T Research) Sanjiv Kapoor (IIT, Delhi) (Co-chair) Kamal Lodaya (IMSc, Chennai) Madhavan Mukund (CMI, Chennai) Gopalan Nadathur (Loyola) Seffi Naor (Bell Labs and Technion) Tobias Nipkow (TU Munich) Luke Ong (Oxford) C. Pandu Rangan (IIT, Chennai) Paritosh Pandya (TIFR) Benjamin Pierce (U Penn) Sanjiva Prasad (IIT, Delhi) (Co-chair) Sridhar Rajagopalan (IBM, Almaden) Abhiram Ranade (IIT, Mumbai) Dave Sands (Chalmers) A Prasad Sistla (U Illinois, Chicago) Michiel Smid (Magdeburg) Mandayam K. Srivas (SRI) Organized by ------------ Indian Institute of Technology, Delhi Hauz Khas, New Delhi 100 016. Organizing Committee ------------------- Sandeep Sen (chair) Naveen Garg (treasurer) S N Maheshwari Conference Site --------------- The Conference will take place at the India International Centre, 40 Lodhi Estate, Max Mueller Marg, New Delhi 110 003. Correspondence Address ---------------------- All correspondence regarding submissions may be addressed to FST TCS 2000 Department of Computer Science and Engineering I.I.T., Delhi Hauz Khas, New Delhi 110 016, INDIA Email: fsttcs20@cse.iitd.ernet.in Fax: +91 11 686 8765 Phone: +91 11 659 1294 / 659 1286 URL: http://www.cse.iitd.ernet.in/~fsttcs20 -- Sanjiva Prasad Associate Professor Department of Computer Science and Engineering sanjiva@cse.iitd.ernet.in Indian Institute of Technology, Delhi (Off) +91 11 659 1294 Hauz Khas, New Delhi 110016 (Res) +91 11 659 1684 INDIA (Fax) +91 11 686 8765 http://www.cse.iitd.ernet.in/~sanjiva From rrosebru@mta.ca Fri May 19 14:16:35 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA05127 for categories-list; Fri, 19 May 2000 14:11:08 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 18 May 2000 13:30:20 -0400 (EDT) From: Peter Freyd Message-Id: <200005181730.NAA00788@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: More products Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Once again let me respond to Kai Bruennler's query: Is there a binary product in the category of sets and functions that is "strictly associative", i.e. A x (B x C) = (A x B) x C and the associativity isomorphisms are equal to the identity? With the axiom of choice it's possible to construct such a product for most categories that arise in nature. The needed condition (besides having finite products) is that each isomorphism class be large enough to accommodate the construction in the next sentence. Given a category with a binary products let O be its objects and O* the finite strings of objects and choose a bijection P:O* --> O that sends a string to a product thereof. (The condition, therefore, reduces to the condition that each isomorphism class be at least as large as the class of finite strings whose product is in that isomorphism class.) Define a new binary product on objects by taking P x P = P. As written, this construction does not work for the category of sets. The problem is the empty set. The construction, though, continues to work if the bijection condition is understood only for those strings whose products are non-empty. The same trick works for any category with strict initial object. Note that 1 x A = A = A x 1 where 1 denotes P<>. From rrosebru@mta.ca Fri May 19 14:16:36 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA08147 for categories-list; Fri, 19 May 2000 14:10:37 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39247952.ED779DDC@di.fc.ul.pt> Date: Fri, 19 May 2000 00:14:26 +0100 From: Nuno Barreiro X-Mailer: Mozilla 4.72 [en] (X11; I; Linux 2.0.36 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: LINEAR Summer School References: <390F9E04.B3035C9F@di.fc.ul.pt> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Please forward. We apologize for any duplication of this message in your mailbox. Best regards, Nuno Barreiro ------------------------------------------------------------------ ================================ ONLY ONE MONTH LEFT TO APPLY Don't miss it! ================================ The LINEAR International Summer School (Linear Logic and Applications) August 30 to September 7, 2000 Hotel Terra Nostra, S.Miguel, Azores, Portugal The Linear TMR research network (http://iml.univ-mrs.fr/LINEAR) is proud to announce its first International Summer School on Linear Logic and Applications. The school is directed to everyone doing postgraduate work in Computer Science or Mathematics with an interest in the field of Formal Logic and its applications. The school lasts one week and comprises both lectures and thematic sessions. The lectures are in the tradition of summer schools and cover one topic, from basic material to more advanced issues. The topics and lecturers are the following: Samson Abramsky --- Game Semantics Jean-Yves Girard -- Linear Logic and Ludics Stefano Guerrini -- Proof-Nets and Lambda-Calculus Yves Lafont ------- Phase Semantics and Decision Problems Phil Scott -------- Category Theory and Concrete Models The thematic sessions will cover state-of-the-art research in Linear Logic. Each session has an organiser responsible for inviting speakers who will talk about their work. The themes and organisers are the following: Andrea Asperti ---- Applications Vincent Danos ----- Proof Theory Thomas Ehrhard ---- Semantics Glynn Winskel ----- Concurrency The school will be held in the island of S.Miguel, Azores, amid luxurious vegetation and hot water springs. The entrance to the mythic kingdom of the Atlantis is believed to be located near Hotel Terra Nostra, some say at the bottom of its famous red and hot water swimming pool... Detailed information and application forms are available at http://linear.di.fc.ul.pt Don't forget to check it! From rrosebru@mta.ca Fri May 19 14:18:36 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA07388 for categories-list; Fri, 19 May 2000 14:15:07 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: IFIP TCS2000 X-Mailer: Mew version 1.94.1 on XEmacs 20.4 (Emerald) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20000517160208N.miyakawa@ito.ecei.tohoku.ac.jp> Date: Wed, 17 May 2000 16:02:08 +0900 From: Shinya MIYAKAWA X-Dispatcher: imput version 990905(IM130) Lines: 627 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: [Apologies for multiple copies] IFIP TCS2000 PROGRAM AND REGISTRATION INFORMATION ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -------------------------------------------------------------------------- IFIP International Conference on Theoretical Computer Science (IFIP TCS2000) --- Exploring New Frontiers of Theoretical Informatics --- August 17 - 19, 2000 Aoba Memorial Bldg., Tohoku University, Sendai, Japan Further Information about IFIP TCS2000 can be obtained on the Web, at http://tcs2000.ito.ecei.tohoku.ac.jp/tcs2000/ Any inquiry on IFIP TCS2000 Program and Registration may be directed to TCS2000@ito.ecei.tohoku.ac.jp -------------------------------------------------------------------------- PRELIMINARY PROGRAM ^^^^^^^^^^^^^^^^^^^ [Outline] AUGUST 16: 15:00 Registration at Sendai Tokyu Hotel till 20:00 18:00 Welcome at Sendai Tokyu Hotel till 19:00 AUGUST 17: 9:30 Opening Session 10:00 Keynote Plenary Talk 1 ----------------------------------------- 11:10 - 17:30 TRACK (1) || TRACK (2) ----------------------------------------- AUGUST 18: 9:10 Keynote Plenary Talk 2 ----------------------------------------- 10:20 - 15:30 TRACK (1) || TRACK (2) ----------------------------------------- 15:50 Panel Discussion till 17:10 ----------------------------------------- 18:30 Banquet at Sendai Tokyu Hotel AUGUST 19: 9:10 Keynote Plenary Talk 3 ----------------------------------------- 10:20 - 14:20 TRACK (1) || TRACK (2) ----------------------------------------- 14:30 Closing Session till 14:40 ----------------------------------------- 15:00 Open Lectures till 17:00 ----------------------------------------- 18:30 Japanese Dinner Party till 20:00 ----------------------------------------- AUGUST 16 WEDNESDAY ^^^^^^^^^^^^^^^^^^^ 15:00 REGISTRATION at Sendai Tokyu Hotel till 20:00 18:00 WELCOME with light snack at Sendai Tokyu Hotel till 19:00 AUGUST 17 THURSDAY ^^^^^^^^^^^^^^^^^^ 9:30 OPENING SESSION Giorgio Ausiello (TC1 Chair and IFIP TCS2000 Co-Chair) Takayasu Ito (IFIP TCS2000 Co-Chair) 10:00 KEYNOTE PLENARY TALK Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption) Martin Abadi (Bell Labs, Lucent)*, Phillip Rogaway (UC Davis) (*: speaker) 10:50 Break [TRACK (1)] SESSION (1.1), 11:10 - 12:00 11:10 Approximation Algorithms for String Folding Problems Giancarlo Mauri, Giulio Pavesi 11:35 An Index for Two Dimensional String Matching Allowing Rotations Kimmo Fredriksson, Gonzalo Navarro, Esko Ukkonen 12:00 Lunch Break SESSION (1.2), 13:30 - 14:20 13:30 Parallel Edge Coloring of a Tree on a Mesh Connected Computer Chang-Sung Jeong, Sung-Up Cho, Sun-Chul Whang, Mi-Young Choi 13:55 Parallel Approximation Algorithms for Maximum Weighted Matching in General Graphs Ryuhei Uehara, Zhi-Zhong Chen 14:20 Break 14:40 TRACK (1) INVITED TALK It is on the Boundary: Complexity Considerations for Polynomial Ideals Ernst Mayr (TU Muenchen) 15:30 Break SESSION (1.3), 15:50 - 17:30 15:50 An Efficient Parallel Algorithm for Scheduling Interval Ordered Tasks Yoojin Chung, Kunsoo Park, Hyuk-Chul Kwon 16:15 Task Distributions on Multiprocessor Systems Evgeny V. Shchepin, Nodari N. Vakhania 16:40 Fast Interpolation using Kohonen Self-Organizing Neural Networks Olivier Sarzeaud, Yann Stephan 17:05 Steganography Using Modern Arts Carlo Blundo, Clemente Galdi 17:30 Break -----------// [TRACK (2)] SESSION (2.1), 11:10 - 12:00 11:10 Ambient Groups and Mobility Types Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon 11:35 An Asynchronous, Distributed Implementation of Mobile Ambients Cedric Fournet, Jean-Jacques Levy, Alan Schmitt 12:00 Lunch Break 13:30 TRACK (2) INVITED TALK Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness Naoki Kobayashi (U. Tokyo) 14:20 Break SESSION (2.2), 14:40 - 15:30 14:40 Local pi-Calculus at Work: Mobile Objects as Mobile Processes Massimo Merro, Josva Kleist, Uwe Nestmann 15:05 An Interpretation of Typed Concurrent Objects in the Blue Calculus Silvano Dal Zilio 15:30 Break SESSION (2.3), 15:50 - 17:30 15:50 A Higher-Order Specification of the pi-Calculus Joelle Despeyroux 16:15 Open Ended Systems, Dynamic Bisimulation, and Tile Logic Roberto Bruni, Ugo Montanari, Vladimiro Sassone 16:40 Fibred Models of Processes: Discrete, Continuous, and Hybrid Systems Marcelo P. Fiore 17:05 On the Complexity of Bisimulation Problems for Pushdown Automata Richard Mayr 17:30 Break AUGUST 18 FRIDAY ^^^^^^^^^^^^^^^^ 9:10 KEYNOTE PLENARY TALK Theory and Construction of Molecular Computers Masami Hagiya (U. Tokyo) 10:00 Break [TRACK (1)] SESSION (1.4), 10:20 - 12:00 10:20 Trade-offs between Density and Robustness in Random Interconnection Graphs P. Flajolet, K. Hatzis, S. Nikoletseas, P. Spirakis 10:45 The ($\sigma$+1)-Edge-Connectivity Augmentation Problem without Creating Multiple Edges of a Graph Satoshi Taoka, Toshimasa Watababe 11:10 On the Hardness of Approximating Some NP-optimization Problems Related to Minimum Linear Ordering Problem Sounaka Mishra, Kripasindhu Sikdar 11:35 Maximum Clique and Minimum Clique Partition in Visibility Graphs Stephan Eidenbenz, Christoph Stamm 12:00 Lunch Break SESSION (1.5), 13:30 - 14:20 13:30 Real-Time Language Recognition by Alternating Cellular Automata Thomas Buchholz, Andreas Klein, Martin Kutrib 13:55 Damage Spreading and $\mu$-Sensitivity on Cellular Automata Bruno Martin 14:20 Break 14:40 TRACK (1) INVITED TALK Discrepancy Theory and its Applications to Finance Shu Tezuka (IBM Tokyo Research Lab) 15:30 Break -----------// [TRACK (2)] SESSION (2.4), 10:20 - 12:00 10:20 A Type-theoretic Study on Partial Continuations Yukiyoshi Kameyama 10:45 Partially Typed Terms between Church-Style and Curry-Style Ken-etsu Fujita, Aleksy Schubert 11:10 Alternating Automata and Logics over Infinite Words Christof Loeding, Wolfgang Thomas 11:35 Hypothesis Support for Information Integration in Four-Valued Logics Yann Loyer, Nicolas Spyratos, Daniel Stamate 12:00 Lunch Break 13:30 TRACK (2) INVITED TALK Masaccio: A Formal Model for Embedded Components Thomas A. Henzinger (UC Berkeley) 14:20 Break SESSION (2.5), 14:40 - 15:30 14:40 A Single Complete Refinement Rule for Demonic Specifications Karl Lermer, Paul Strooper 15:05 Reasoning about Composition using Property Transformers and their Conjugates Michel Charpentier, K. Mani Chandy 15:30 Break ----------------------- 15:50 PANEL DISCUSSION on "New Challenges for TCS" Panelists: Giorgio Ausiello (U. Roma "La Sapienza") Jozef Gruska (Masaryk U.) Ugo Montanari (U. Pisa) Takao Nishizeki (Tohoku U.) Yoshihito Toyama (Tohoku U.) Jiri Wiedermann (Inst. Informatics, Prague) 17:10 Break 18:30 BANQUET at Sendai Tokyu Hotel till 20:45 BANQUET SPEECH Non-Random Thoughts about Randomization Michael O. Rabin (Harvard U.) AUGUST 19 SATURDAY ^^^^^^^^^^^^^^^^^^ 9:10 KEYNOTE PLENARY TALK List Decoding: Algorithms and Applications Madhu Sudan (MIT) 10:00 Break [TRACK (1)] SESSION (1.6), 10:20 - 12:00 10:20 Fully Consistent Extensions of Partially Defined Boolean Functions with Missing Bits Endre Boros, Toshihide Ibaraki, Kazuhisa Makino 10:45 Characterization of Optimal Key Set Protocols Takaaki Mizuki, Hiroki Shizuya, Takao Nishizeki 11:10 On the Complexity of Integer Programming in the Blum-Shub-Smale Computational Model Valentin E. Brimkov, Stefan S. Dantchev 11:35 On Logarithmic Simulated Annealing A. Albrecht, C. K. Wong 12:00 Lunch Break 13:30 TRACK (1) INVITED TALK Hierarchical State Machines Mihalis Yannakakis (Bell Labs, Lucent) 14:20 Break -----------// [TRACK (2)] 10:20 TRACK (2) INVITED TALK Some New Directions in the Syntax and Semantics of Formal Languages Gordon D. Plotkin (Edinburgh U.) 11:10 Break 11:20 DEMO SESSION (1) on Verification Tools 12:00 Lunch Break 13:30 DEMO SESSION (2) on Verification Tools 14:20 Break ------------------------ 14:30 CLOSING SESSION till 14:40 Giorgio Ausiello (TC1 Chair and IFIP TCS2000 Co-Chair) Takayasu Ito (IFIP TCS2000 Co-Chair) ------------------------ [OPEN LECTURES] 15:00 On the Power of Interactive Computing Jan van Leeuwen (U. Utrecht)*, Jiri Wiedermann (Acad. Sciences, Czech) (*: speaker) 16:00 The Varieties of Programming Language Semantics Peter D. Mosses (U. Aarhus) 17:00 Break ------------------------ 18:30 JAPANESE DINNER PARTY till 20:00 ========================================================================== GENERAL INFORMATION ^^^^^^^^^^^^^^^^^^^ IFIP TCS2000 is the first International Conference on Theoretical Computer Science organized by IFIP TC1 on Foundations of Computer Science, and it consists of two tracks: TRACK (1) on Algorithms, Complexity and Models of Computation, and TRACK (2) on Logic, Semantics, Specification, and Verification. The conference proceedings will be published as a volume of Lecture Notes in Computer Science, Springer-Verlag. IFIP TCS2000 will be held on the campus of Tohoku University, Sendai, Japan. The invited talks and contributed talks will be presented at the Aoba Memorial Building and Engineering Conference Hall, Faculty of Engineering located on the Aoba Hill about 3 km west of downtown Sendai. The conference welcome reception and banquet will be held at Sendai Tokyu Hotel, located at downtown Sendai. Please, register and make reservations by returning the completed form by email and fax, following the instructions below. There will also be on-site registration at: * Sendai Tokyu Hotel, 15:00 - 20:00, August 16 * Aoba Memorial Bldg., Tohoku Univ., 9:00 - 17:00 on August 17 - 19. Transportation Conference participants arriving at the new Tokyo International (Narita) Airport are advised to take the JR Narita Express train from Narita Airport to Tokyo Station. Then, take the Yamabiko super express train of Tohoku Shinkansen (Tohoku Bullet Train) to Sendai from Tokyo Station. The Yamabiko runs every 20 - 30 min. and takes about 2 hours from Tokyo to Sendai. Making reservation at Narita Station for the Yamabiko is recommended, since it will be the summer tourist season. Those arriving at the new Osaka International Airport (Kansai Airport) can fly to Sendai Airport, and take Limousine Bus service to Sendai Station. The bus takes about 30 min. to go from the Airport to Sendai Station. You can also take a shuttle bus service from Kansai Airport to the Osaka-Itami Airport to fly from there to Sendai Airport. Alternatively, you can take a local train from the Kansai Airport to JR Shin Osaka Station, then take the Tokaido Shinkansen from Osaka to Tokyo Station and change at Tokyo Station to Tohoku Shinkansen. Some details on transportation will be available on the TCS2000 Web page, at http://tcs2000.ito.ecei.tohoku.ac.jp/tcs2000/ Note: (1) In Japan, mid-August is the busiest tourist time during summer, including domestic and international flights. (2) No flight service is available from Narita to Sendai Airport, since the train service is convenient. There is another train service from Narita Airport to downtown Tokyo (Ueno) by Skyliner of the Keisei-Narita Line. At Ueno you can take the Yamabiko super express of Tohoku Shinkansen to Sendai, but you have to walk about 10 min. from Keisei-Ueno Station to JR Ueno Station to take Tohoku Shinkansen. (3) If you are going to travel in Japan by JR lines before/after the IFIP TCS2000 conference, it will be convenient and economical to get a JR PASS before your departure. Contact your travel agent for more information on JR PASS (Japan Rail Pass). Hotels Two hotels are arranged to offer special discount rates to IFIP TCS2000 participants: Sendai Tokyu Hotel and Sendai Washington Hotel. They are 1.2 km west of Sendai Station and about 800 Yen by taxi from the station. These hotels are located within 5 min. walk from each other. The conference welcome reception and banquet will be held at Sendai Tokyu Hotel. Sendai and Climate Sendai is the largest city in the northern part of the Honshu Island of Japan, with a population of about a million. The City is known in Japan as "City of Trees". Sendai is a modern, safe city with a temperate climate blessed by four distinct seasons; even in mid August it is quite seldom that the highest temperature exceeds 30 C (86 F). Usually, the weather in mid August would be mostly sunny with temperatures ranging from 20 C (68 F) to 30 C (86 F), and rain, if any, would rarely be heavy. Note: Average temperatures in August at Sendai, Tokyo and Osaka are about 23.5 C, 26.5 C and 27.5, respectively. REGISTRATION AND RESERVATION INFORMATION ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ REGISTRATION FEES Registration fees cover attendance in all sessions, a copy of the proceedings, refreshments, the welcome reception and banquet, but not the Japanese dinner party on August 19. The reduced author rate applies to all authors of the accepted papers, and the reduced committee member rate applies to all TC1 members and to all members of the Program Committee and the Organizing Committee. The student rate applies to full time students. Registrants paying reduced rates have full privileges at the conference. The companion rate covers the reception and banquet only. Through July 1st, 2000 From July 2nd, 2000 Regular 40,000 Yen 50,000 Yen Author 30,000 Yen 40,000 Yen Committee Member 30,000 Yen 40,000 Yen Student 25,000 Yen 30,000 Yen Companion 5,000 Yen 7,000 Yen HOTELS Two convenient Western Style hotels offer special IFIP TCS2000 discount rates. Rates are per person, per night, and include service charge and tax (not including breakfast). Single Room Twin Room Sendai Tokyu Hotel 10,500 Yen 8,400 Yen Sendai Washington Hotel II 8,400 Yen 7,350 Yen Sendai Washington Hotel I 7,350 Yen --------- Note: Twin room reservations are available for two persons. No roommate matching service is available, so that twin room reservations remain the registrant's responsibility. JAPANESE DINNER PARTY A Japanese dinner party for participants from abroad will be arranged at SHOZANKAN in the evening of August 19. The invited speakers, some Steering Committee members, PC members and conference organizers will attend. A limited number of reservations will be available for this dinner party. The rates are as follows. Conference registrant: 10,000 Yen Companion: 7,000 Yen ============================================================================= Cut here to send your registration form after filling in the required items. ============================================================================= IFIP TCS2000 REGISTRATION AND RESERVATION FORM ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Please register and make reservations by completing the form below and returning it by email to tcs02@thk.jtb.co.jp Registrants are advised to email a copy of their completed form to TCS2000@ito.ecei.tohoku.ac.jp They are also encouraged to send a signed, printed copy of their completed form by fax to 022-262-5002 (domestic) +81-22-262-5002 (from abroad) which is the fax number of the following agent to take care of the conference registration and reservation. JTB (Japan Travel Bureau) Tohoku Communications Inc. Kotsukosha Bldg 3F, 3-6-Chuo Aoba-Ku, Sendai 980-0021, Japan (Fax) 022-262-5002 (domestic) +81-22-262-5002 (from abroad) (Phone) 022-262-5055 (domestic) +81-22-262-5055 (from abroad) (Email) tcs02@thk.jtb.co.jp Registration and reservations will be completed by your payment, whose method is described below. IMPORTANT NOTE: As described below, from the standpoint of the safety, registrants are advised to pay fees by Bank Transfer. When the payment is made by a credit card, they are advised to send the required information including Credit Card numbers by FAX; that is, do NOT send Credit Card numbers by email. REGISTRATION FOR IFIP TCS2000 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Last (Family) Name: First (Given) Name: Middle: Affiliation: Postal Address: City/State/Zip: Country: Phone: Fax: Email: Registration Status : Number of Companions: Companions' names (if applicable): (A) Total Registration Fee(s) in Yen: HOTEL RESERVATION Hotel First Choice: Hotel Second Choice: Number of Single Room(s): Number of Twin Room(s): Roommate's Name(s) for Twin Room(s): Check-in Date: Check-out Date: Number of Nights: Special Room or other Request: JAPANESE DINNER PARTY A limited number of reservations are available for the Japanese dinner party at SHOZANKAN on August 19 to be arranged for participants from abroad. (B) 10,000 Yen x [ ] conference registrant(s): (C) 7,000 Yen x [ ] companion(s): TOTAL FEE IN YEN (A) + (B) + (C): Signature (not needed for email): METHOD OF PAYMENT FOR IFIP TCS2000 From the standpoint of the safety and security, participants are encouraged to pay via Bank Transfer. When they pay via credit card, they are advised to send the required information (in particular, Credit Card numbers) by FAX; that is, do NOT send your Credit Card numbers by email. In credit card payment Visa card, MasterCard, and Diners card will be accepted. Personal checks cannot be accepted. All payments must be made in Japanese Yen. Indicate method of payment below: [ ] Bank Transfer to Bank: Tokyo Mitsubishi Bank, Sendai Branch Account Name: IFIP TCS2000 Chair Takayasu Ito Account No. 1108671 From : Date of transfer: Payer's name: Note: In Japan the bank number of Tokyo Mitsubishi Bank is 0005, and the number of its Sendai Branch is 320. [ ] Payment by Credit Card Credit Card Type : Card Number: Expiration Date: Signature (not needed for email): : When your payment is via Credit Card, send the above information by FAX to +81-22-262-5002, the fax no. of JTB Communications Inc. Even when you send the above form by fax, send it by EMAIL without filling in Credit Card number for safety. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Registration and reservations will be confirmed upon receipt of payment. Refunds will be made upon written request received through July 31st, 2000 by JTB Tohoku Communications Inc. From rrosebru@mta.ca Sat May 20 10:10:37 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA24485 for categories-list; Sat, 20 May 2000 10:07:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: "Walter Tholen" Message-Id: <1000519165650.ZM56082@pascal.math.yorku.ca> Date: Fri, 19 May 2000 16:56:50 -0400 X-Mailer: Z-Mail (4.0.1 13Jan97) To: categories@mta.ca Subject: categories: AMS Special Session: Toronto, September 2000 Cc: tholen@pascal.math.yorku.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: SECOND ANNOUNCEMENT AMS Regional Meeting #957 in Toronto, September 22 - 24, Special Session on Applied Categorical Structures Thanks to everybody who responded to our first announcement. With 19 talks scheduled we have already exhausted the time slots available to us and are not able to accommodate any further talks, unless we receive cancellations in the very near future. Here is the current list of speakers: Steve Awodey, David Benson, Lars Birkedal, Marta Bunge, Robin Cockett, Jack Duskin, Marco Grandis, Andre Joyal, Jim Lambek, Bill Lawvere, James Madden, Michael Makkai, M.M. Mawanda, Bob Pare, Nico Pumpluen, Jiri Rosicky, Myles Tierney, Enrico Vitale, and Richard Wood. All talks are 25-minute talks. Speakers are asked to provide us with the titles of their talks by June 15. Furthermore, speakers must provide abstracts, to be sent directly to the AMS, in accordance with AMS regulations, via web, email or hard copy. The absolute deadline for receipt of abstracts by the AMS is July 14. We shall give further details in a subsequent mailing to speakers. Here is the block schedule for the Session: Friday, September 22, 8pm: Welcome Party for all participants in the Session Saturday, September 23, 9-11:30 am (5 talks) 3-5:30 pm (5 talks) Sunday, September 24, 9-11:30 am (5 talks) 2-4 pm (4 talks) A detailed schedule will be contained in our final announcement, to be communicated at the beginning of September. All other relevant information (accommodation, fees, other sessions, invited addresses) will be published in a forthcoming issue of the Notices of the AMS. Please follow the registration/reservation procedures given there. We regret not to be able to assist you with that. In making travel arrangements, please note particularly that the Session will continue until 4 pm Sunday afternoon. While the list of speakers is by necessity very limited, there is no limit to the number of participants! We hope to see you in Toronto in the (very early) fall. Joan Wick Pelletier Walter Tholen From rrosebru@mta.ca Mon May 22 14:07:08 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA16298 for categories-list; Mon, 22 May 2000 14:02:34 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Baumgartner MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Message-ID: <14633.8642.599242.823009@nostromo.uni-koblenz.de> Date: Mon, 22 May 2000 14:02:10 +0200 (CEST) Subject: categories: FTP 2000 and TABLEAUX 2000 - Call for Participation X-Mailer: VM 6.75 under 21.1 (patch 8) "Bryce Canyon" XEmacs Lucid X-MIME-Autoconverted: from 8bit to quoted-printable by mailhost.uni-koblenz.de id OAA23918 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id JAA11797 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ------------------------------------------------------------------------- FTP 2000 and TABLEAUX 2000 Call for Participation University of St Andrews St Andrews, Scotland July 3-7, 2000 FTP 2000: http://www.uni-koblenz.de/ftp00/ TABLEAUX 2000: http://www-theory.dcs.st-and.ac.uk/~rd/tab2000/ --------------------------------------------------------------------- Contents: 1 - Scope 2 - Registration 3 - Contact 4 - Technical Program (including list of accepted contributions) --------------------------------------------------------------------- 1 - Scope FTP 2000 (First-Order Theorem Proving), July 3-5, is the third in a series of workshops intended to focus effort on First-Order Theorem Proving as a core theme of Automated Deduction, and to provide a forum for presentation of very recent work and discussion of research in progress. TABLEAUX 2000, July 4-7, is a continuation of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods held since 1992. The conference brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods. FTP 2000 is held in conjunction with TABLEAUX 2000. The FTP 2000 and TABLEAUX 2000 sessions will be partly in series, partly shared and partly in parallel. --------------------------------------------------------------------- 2 - Registration To register for FTP 2000 and/or TABLEAUX 2000 please use the online registration form at http://www.dcs.st-and.ac.uk/~tab2000/register.html Joint registration at reduced rate is possible. Early registration ends at May, 31. --------------------------------------------------------------------- 3 - Contact FTP 2000 related: ftp00@cs.uiowa.edu TABLEAUX 2000 related: rd@dcs.st-and.ac.uk Local Organisation: rd@dcs.st-and.ac.uk --------------------------------------------------------------------- 4 - Technical Program FTP 2000 and TABLEAUX 2000 schedule: http://www.dcs.st-and.ac.uk/~tab2000/schedule.html Invited Talks ------------- FTP 2000 TABLEAUX 2000 -------- ------------- David Crocker Melvin Fitting (CUNY) (Intelligent Micro Modality and Databases Software Ltd) First Order Theorem Proving in Software Verification Deepak Kapur (New Mexico) Alasdair Urquhart (Toronto) 'Hardware Verification' Local Symmetries in (exact title to be announced) Propositional Logic Franz Baader (Aachen) (Joint invited speaker) Tableau Algorithms for Description Logics FTP 2000 accepted contributions: -------------------------------- J. Avenhaus, T. Hillenbrand, B. Loechner On Using Ground Joinable Equations in Equational Theorem Proving Johan Belinfante The Unifying Concept of Subvariance Domenico Cantone The decision problem in graph theory with reachability related constructs Michael Dierkes Defining a Unique Herbrand Model for Sets of Guarded Clauses Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt Hyperresolution for Guarded Formulae Martin Giese A First-Order Simplification Rule with Constraints Koji Iwanuma, Katsumi Inoue, Ken Satoh Completeness of Pruning Methods for Consequence Finding Procedure SOL James J. Lu, Jeffrey S. Rosenthal, Andrew Shaffer Crossword Puzzles: A Case Study in Compute-Intensive Meta-Reasoning Nicolas Peltier Combining Resolution and Enumeration for Finite Model Building Reinhard Pichler Equational Problems over a Finite Domain Regimantas Pliuskevicius On \omega­decidability for a restricted FTL with Unless J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, F. Martin A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2) Nicolas Peltier Model Building with Ordered Resolution Cesare Tinelli Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing Bernhard Gramlich Extending First-Order Unification by Tractable Second-Order Features Kahlil Hodgson, John Slaney Semantic Guidance for Saturation­Based Theorem Proving Bernhard Beckert Depth­first Proof Search without Backtracking for Free Variable Clausal Tableaux Jens Otten, Wolfgang Bibel leanCoP: Lean Connection­Based Theorem Proving (system description) Position Papers Chris Fermueller Automated Model Building for Non-Classical Logics Martin Giese Proof Search without Backtracking using Instance Streams Markus Moschner Towards Finite Model Building for Propositional Gödel-Logics TABLEAUX 2000 accepted contributions ------------------------------------ Comparison of Theorem Provers for non-classical logics: Fabio Massacci and Francesco M. Donini Design and results of TANCS-2000 non-classical (modal) systems comparison Volker Haarslev and Ralf Möller Consistency testing: the RACE experience Ian Horrocks Benchmark analysis with FaCT Ullrich Hustadt and Renate Schmidt MSPASS Modal reasoning by translation and first-order resolution Peter F. Patel-Schneider TANCS-2000 results for DLP Armando Tacchella Evaluating *SAT on TANCS 2000 benchmarks Research Papers: Alberto Artosi, Guido Governatori and Antonino Rotolo A labelled tableau calculus for nonmonotonic (cumulative) consequence relations Arnon Avron A tableau system for Gödel-Dummett logic based on a hypersequent calculus Matthias Baaz, Christian Fermüller and Helmut Veith An analytic calculus for quantified propositional Gödel logic Diderik Batens and Joke Meheus A tableau method for inconsistency-adaptive logics Domenico Cantone and Calogero G. Zarba A tableau calculus for integrating first-order reasoning with elementary set theory reasoning Agata Ciabattoni and Mauro Ferrari Hypertableau and path-hypertableau calculi for some families of intermediate logics Marta Cialdea Mayer and Serenella Cerrito Variants of first-order modal logics Stéphane Demri Complexity of simple dependent bimodal logics Uwe Egly Properties of Embeddings from Int to S4 Melvin Fitting, Lars Thalmann and Andrei Voronkov Term-modal logics Enrico Giunchiglia and Armando Tacchella A subset-matching size-bounded cache for satisfiability in modal logics Rajeev Goré Dual intuitionistic logic revisited Ray Gumb Model sets in a nonconstructive logic of partial terms with definite descriptions Ortrun Ibens Search space compression in connection tableau calculi using disjunctive constraints Christoph Kreitz and Brigitte Pientka Matrix-based inductive theorem proving Pedro J. Martín and Antonio Gavilanes Monotonic preorders for free variable tableaux Maarten Marx, Szabolcs Mikulás and Mark Reynolds The mosaic method for temporal logics Linh Anh Nguyen Sequent-like tableau systems with the analytic superformula property for the modal logics KB, KDB, K5, KD5 David Pearce, Inmaculada P. de Guzmán and Agustín Valverde A tableau calculus for equilibrium entailment Carla Piazza and Alberto Policriti Towards tableau-based decision procedures for non-well-founded fragments of set theory Riccardo Rosati Tableau calculus for only knowing and knowing at most Stephan Schmitt A tableau-like representation framework for efficient proof reconstruction Dan Willard The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q System Descriptions: Joachim Draeger Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO Gernot Stenz and Andreas Wolf E-SETHEO: An automated3 theorem prover --------------------------------------------------------------------- -- Peter Baumgartner phone: +49 261 287 2777 mail: peter@uni-koblenz.de fax: +49 261 287 2731 WWW: http://www.uni-koblenz.de/~peter/ From rrosebru@mta.ca Sun May 28 14:29:18 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA06712 for categories-list; Sun, 28 May 2000 14:23:13 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Martin Escardo MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14638.49628.646225.340217@mosstowie.dcs.st-and.ac.uk> Date: Fri, 26 May 2000 19:26:36 +0100 (BST) To: categories@mta.ca Subject: categories: Pataraia's fixed-point theorem X-Mailer: VM 6.71 under 21.1 (patch 3) "Acadia" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: An intuitionistic version (in the sense of topos logic) of Tarski's fixed-point theorem, by Dmitri Pataraia, was discussed in this list some years ago. (I think it was presented in the PSSL in November 1997, but I didn't attend that.) I've written a paper that uses this, and I would like to cite it appropriately. Does anyone know if it has been published? (I didn't find anything in MathSciNet or Zentralblatt MATH.) (Maybe someone knows his e-mail address? I failed to find his whereabouts using search engines.) Thanks. From rrosebru@mta.ca Mon May 29 07:19:38 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id HAA22041 for categories-list; Mon, 29 May 2000 07:14:46 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Andrei Voronkov To: pmaenpaa@cs.hut.fi MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14638.45333.377476.317398@voronkov.cs.man.ac.uk> Date: Fri, 26 May 2000 18:15:01 +0100 (BST) To: categories@mta.ca Subject: categories: CFP: LPAR'2000, Reunion Island, France X-Mailer: VM 6.71 under 21.1 (patch 7) "Biscayne" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14638.45333.377476.317398@voronkov.cs.man.ac.uk> Date: Fri, 26 May 2000 18:15:01 +0100 (BST) To: amast@cs.utwente.nl, asci@twi.tudelft.nl, bra-types@cs.chalmers.se, calculemus-ig@dist.unige.it, categories@mta.ca, ccl@dfki.uni-sb.de, compunode@compulog.org, concurrency@cwi.nl, coq-club@pauillac.inria.fr, cs-logic@cs.indiana.edu, dataloger@cs.chalmers.se, eacsl@dimi.uniud.it, facs@lboro.ac.uk, formal-methods@cs.uidaho.edu, fsdm@it.uq.edu.au, ftp@logic.at, info-hol@jaguar.cs.byu.edu, isabelle-users@cl.cam.ac.uk, kgs@logic.tuwien.ac.at, lics-request@research.bell-labs.com, linear@cs.stanford.edu, logic-ml@logic.jaist.ac.jp, lprolog@central.cis.upenn.edu, mizar-forum@mizar.uwb.edu.pl, mop@cs.ruu.nl, ozsl-list@fwi.uva.nl, protagonist@cs.kun.nl, qed@mcs.anl.gov, rewriting@ens-lyon.fr, theorem-provers@ai.mit.edu, theorynt@listserv.nodak.edu, types@cis.upenn.edu, uitp%dcs.gla.ac.uk.nqthm-users%cli.com.nuprllist%cs.cornell.edu.pvs%csl.sri.com.tmr-linear%iml.univ-mrs.fr.vdm-forum@mailbase.ac.uk Subject: CFP: LPAR'2000, Reunion Island, France X-Mailer: VM 6.71 under 21.1 (patch 7) "Biscayne" XEmacs Lucid Subject: CFP: LPAR'2000, Reunion Island, France X-Mailer: VM 6.71 under 21.1 (patch 7) "Biscayne" XEmacs Lucid Sender: pmaenpaa@mappi.helsinki.fi X-Originating-IP: 130.233.193.43 Subject: CFP: LPAR'2000, Reunion Island, France [Apologies for receiving multiple copies ] LPAR'2000 7th International Conference on LOGIC for PROGRAMMING and AUTOMATED REASONING Reunion Island, November 6-10, 2000 CALL FOR PAPERS http://www.cs.man.ac.uk/~voronkov/LPAR/2000/general.html Location: LPAR'2000 will be held November 6-10, 2000, on Reunion Island, a small french island in the Indian Ocean, to the east of Madagascar. It will be followed by a "Workshop on Implementations of Logic", November 11-12. Topics: * automated reasoning * lambda and combinatory calculi * interactive theorem proving * constructive logic and type theory * implementations of logic * computional interpretations of logic * design of logical frameworks * logical foundations of programming * program & system verification * logical aspects of concurrency * model checking * program extraction from proofs * rewriting * linear logic * logic programming * modal and temporal logics * constraints programming * knowledge representation & reasoning * logic and databases * reasoning about actions * logic & computational complexity * description logics * specification using logics * nonmonotonic reasoning Invited speakers: * BrunoCourcelle (Bordeaux-1 University) * Georg Gottlob (Technische Universitaet Wien) * Erich Graedel (RWTH Aachen) * Michael Rusinowitch (LORIA-INRIA-Lorraine) Programme Committee: * Stefano Berardi, Torino * Leonid Libkin, Bell Labs * Manfred Broy, Munich * Patrick Lincoln, SRI * Maurice Bruynooghe, Leuven * David McAllester, AT&T Labs * Hubert Comon, Cachan * Robert Nieuwenhuis, Barcelona * Gilles Dowek, INRIA * Mitsuhiro Okada, Tokyo * Harald Ganzinger, MPI * Catuscia Palamidessi, Penn State * Mike Gordon, Cambridge * Leszek Pacholski, Wroclaw * Yuri Gurevich, Microsoft Res. * Michel Parigot, Paris (co-chair) * Neil Jones, Copenhagen * Frank Pfenning, Pittsburgh * Teodor Knapik, Reunion * Helmut Schwichtenberg, Munich * Yves Lafont, Marseille * Jan Smith, Goteborg * Daniel Leivant, Bloomington * Wolfgang Thomas, Aachen * Maurizio Lenzerini, Roma * Pascal van Hentenryck, Providence * Giorgio Levi, Pisa * Andrei Voronkov, Manchester (co-chair) Organizing Committee: * Teodor Knapik, University of Reunion * Pascal Manoury, University of Paris VI * Andrei Voronkov, University of Manchester Submission of papers: Submitted papers must be original and not submitted concurrently for publication to a journal or to another conference. Submission by members of the Program Committee is not allowed. The proceedings of LPAR'2000 will be published by Springer-Verlag in the LNAI series and available at the conference. Both "theoretical" papers and "experimental" papers are welcome. The first category is intended to contain new theoretical results, the second one to describe implementations of systems, to report experiments with implemented systems, or to compare implemented systems. Submitted "theoretical" papers should not be longer than 15 proceedings pages. Submitted "experimental" papers should not be longer than 10 proceedings pages. The proceedings of LPAR'2000 will be published by Springer-Verlag in the LNAI series. Papers in the postscript or PDF format, preferably uuencoded and zipped or gzipped, should be sent by email to lpar00-submission@cs.man.ac.uk. Title, abstract, and the list of authors with their email addresses should be sent to the same address in a separate message. --------------------------------------------- All questions related to submission should be sent to the program chairs: Michel Parigot and Andrei Voronkov Important dates: Submission: June 1 Notification: July 15 Final version: August 10 Conference: November 6-10 Worskhop: November 11-12 More information: http://www.cs.man.ac.uk/~voronkov/LPAR/2000/general.html From rrosebru@mta.ca Wed May 31 05:34:30 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id FAA02529 for categories-list; Wed, 31 May 2000 05:32:42 -0300 (ADT) Message-Id: <200005310832.FAA02529@mailserv.mta.ca> X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca From: Chikoidze Date: Wed, 31 May 0 11:47:59 +0500 X-Mailer: BML [MS/DOS Beauty Mail v.1.36] Subject: categories: announcement Lines: 216 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: To whom it may concern, Dear Sir, Please, be so kind as to include the Announcement of the Tbilisi Summer School in your e-mail list. I hope, you will find all necessary information in the Announcement itself. Best regards, George Chikoidze Contact Person of the Centre on Language, Logic, Speech at the Tbilisi State University Address: Dpt. of Language Modelling Inst. of Control Systems Georgian Academy of Sciences 34, Gamsakhurdia Av. 380060 Tbilisi Georgia Phone: + 995 32 38 21 36 Fax: + 995 32 94 23 91 E-mail: chiko@contsys.acnet.ge ANNOUNCEMENT Tbilisi Summer School in Language, Logic, and Computation 29th August - 8 September 2000 Tbilisi, Georgia The Georgian Centre for Language, Logic, and Speech, based at the Tbilisi State University, will host Tbilisi Summer School, the main purpose of which is to make the students and young scholars acquainted with the modern state of affairs in the mentioned fields of science, and - at the same time - to further contacts and scientific collaboration between Western and Eastern Scholars. LECTURERS Jurij Apresjan, Moscow Matthias Baaz, Vienna Pascal Boldini, Paris Marina Glavinskaja, Moscow Michel Parigot, Paris Carl Vogel,Dublin Andrej Voronkov, Manchester COURSES - Foundations of linguistic semantics (Ju.Apresjan) - On the generalisation of proofs and calculations (M.Baaz) - Type theories for semantics and cognition (P.Boldini) - Semantics of aspect (M.Glavinskaja) - Proofs as programs (M.Parigot) - Cognitive constraints on linguistic theory. (C.Vogel) - Logical foundations of deductive databases. (A.Voronkov). SCHEDULE Tuesday, August 29 12.00 - 13.00 Opening of the School 18.00 - Banquet Wednesday, August 30 10.00 - 13.00 M. Parigot. Proofs as programs 13.00 - 14.00 Lunch 14.00 - 17.00 Ju. Apresjan. Foundations of linguistic semantics Thursday, August 31 10.00 - 13.00 M. Parigot. Proofs as programs. 13.00 - 14.00 Lunch 14.00 - 17.00 Ju. Apresjan. Foundations of linguistic semantics. Friday, September 1 10.00 - 13.00 M. Glavinskaja. Semantics of aspect. 13.00 - 14.00 Lunch 14.00 - 17.00 C. Vogel. Cognitive constraints on linguistic theory. Saturday, September 2 Recreation (sight-seeing in Tbilisi and environs, Sunday, September 3 excursion). Monday, September 4 10.00 - 13.00 M. Glavinskaja. Semantics of aspect. 13.00 - 14.00 Lunch 14.00 - 16.00 C. Vogel. Cognitive constraints on linguistic theory. Tuesday, September 5 10.00 - 14.00 A. Voronkov. Logical foundations of deductive databases. 14.00 - 15.00 Lunch 15.00 - 17.00 C. Vogel. Cognitive constraints on linguistic theory. Wednesday, September 6 10.00 - 12.00 A. Voronkov. Logical foundations of deductive databases. 12.00 - 14.00 M. Baaz. On the generalization of proofs and calculations. 14.00 - 15.00 Lunch 15.00 - 17.00 P. Boldini. Type theories for semantics and cognition. Thursday, September 7 10.00 - 12.00 M. Baaz. On the generalisation of proofs and calculations. 12.00 - 14.00 P. Boldini. Type theories for semantics and cognition. 14.00 - 15.00 Lunch Friday, September 8 10.00 - 12.00 M. Baaz. On the generalization of proofs and calculations. 12.00 - 14.00 P. Boldini. Type theories for semantics and cognition. 14.00 - 15.00 Lunch 15.00 - 16.00 Closing of the School. 18.00 Banquet STUDENTS Besides local students, the School also welcomes students from abroad. The Participation fee for these students will be $120 (wich includes excursion, banquet, reprints, etc.).Foreign students will be comfortably accommodated with Georgian families (with two meals) for $40 per day. LOCATION AND SIGHTSEEING TOURS Georgia is the ancient country situated between Black and Caspian seas, the Caucasus and Turkey. It is the country of the Golden Fleece, the myth of Argonauts, Jason and Medea, and Prometheus, chained to the Caucasus mountains. Tbilisi - capital of Georgia - has more than 1 million in habitant. It is situated some 100-150 km to the south of main Caucasus ridge, in the beautiful valley of the river Mtkvari, surrounded by the green slopes of the Caucasus spurs. The city has a long (1500 year old) history and abounds in historical and cultural memorials. Georgia is famous for its high quality wines, exquisite cuisine and cordial hospitality. The main site of the Symposium, Tbilisi State University, is the chief centre of education in the country, and has several outstanding scholars in science, art and politics among its graduates. During the School there will be an excursion over the famous Georgian Military Road, which leads us through the ancient capital of Georgia - Mtskheta, with its abundant architectural and historical monuments - and which brings us across the main ridge of the Caucasus by the Cross Pass. The destination of the envisaged trip is the mountain resort Kazbegi with its Trinity Church situated on the top of high peak facing the second mountain (after Elbrus), the peak of the Caucasus - Mkinvarcveri (Glacier - mountain). TRAVEL INFORMATION Tbilisi can only be reached by air. If there are no direct trip between your point of departure and Tbilisi, the most convenient connections are via Istambul, Frankfurt or Moscow. ORGANISING COMMITTEE: T.Khurodze (Chair, Pro-rector of Tbilisi State University) R.Asatiani (Institute of Oriental Studies) N.Chanishvili (Tbilisi State University) G.Chikoidze (Institute of Control Systems) K.Pkhakadze (Institute of Applied Mathematics) Kh.Rukhaja (Institute of Applied Mathematics). For additional information, please, use the following address: George Chikoidze Dept. of Language Modelling Inst. of Control Systems Georgian Academy of Sciences 34, K. Gamsakhurdia 380060 Tbilisi Georgia Phone: +9 9532 382136 E- mail: chiko@contsys.acnet.ge From rrosebru@mta.ca Wed May 31 06:11:37 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id FAA28442 for categories-list; Wed, 31 May 2000 05:24:10 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <20000531020850.2130.qmail@nw178.netaddress.usa.net> Date: 30 May 00 20:08:50 MDT From: adrian duma To: categories@mta.ca Subject: categories: question X-Mailer: USANET web-mailer (34FM1.4.02C) Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id XAA17749 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear Experts in Category Theory, I am very interested in the following problem. Let us consider the category Cat of small categories. I need for a "topology" on Morph(Cat) (i.e., the functors between small categories), with the following property: For each u in Morph(Cat) and each D in Ob(Cat) there exist v C------------>D in Morph(Cat), a functor F:Cat----->Cat with F(u) = v, and two "open neighbourhoods" U and V of u and v, respectively, such that F (acting on Morph(Cat)) is a "homeomorphism" between U and V. I would be very grateful to you for any related comment. With my best regards, I remain Truly Yours Adrian Duma. ____________________________________________________________________ Get free email and a permanent address at http://www.netaddress.com/?N=1 From rrosebru@mta.ca Wed May 31 06:26:38 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id FAA24539 for categories-list; Wed, 31 May 2000 05:22:12 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: Date: Tue, 30 May 2000 18:53:31 +0100 (BST) From: "Roy L. Crole" To: categories@mta.ca, types@cis.upenn.edu Subject: categories: Lectureships in Computer Science Mime-Version: 1.0 (generated by tm-edit 7.106) Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear Colleagues, I would like to announce three Lectureships in Computer Science, which may be of interest to CATEGORIES and TYPES readers. Leicester has a research group working in Categories and Semantics which includes Simon Ambler, Neil Ghani, Vincent Schmitt, Nobuko Yoshida and myself. Current research areas include Operational Semantics, Mechanized Reasoning, Categorical Models of Programming Languages including Concurrency, Categorical Term Rewriting, and Enriched Category Theory. These areas are directly or indirectly connected with the theory and practice of categories and types. Roy Crole. --------------------- %< ---------------------------------------- UNIVERSITY OF LEICESTER DEPARTMENT OF MATHEMATICS & COMPUTER SCIENCE Lecturer A in Computer Science (3 posts) Available from 1 September 2000 Ref: A5365/GD Applications are invited for three open-ended Lectureships in Computer Science in the Department of Mathematics and Computer Science at the University of Leicester. There is no restriction regarding the area of research and applicants with expertise in any area of Computer Science are welcomed. All three lectureships are tenable from 1 September 2000 or as soon as possible thereafter. The Department of Mathematics and Computer Science is divided into three groups: Computer Science, Pure Mathematics and Applied Mathematics. The Computer Science Group is firmly research oriented and these lectureships are intended to strengthen the Group with regard to both teaching and research. The successful applicants will be ambitious, able to develop their own research within a multi-faceted environment, and have a strong research record and potential. The new lecturers will be required to teach at undergraduate and postgraduate level, and to perform administrative duties as directed by the Head of Department. This is a superb opportunity for persons of energy, drive and ambition to assume rewarding roles and to establish themselves in a young, dynamic and rapidly developing department. Initial salary, dependent upon qualifications and experience, will be on the Lecturer Grade A scale UKpounds 17,238 to UK pounds 22,579 p.a. Candidates who are interested in the lectureships are invited, if they so wish, to contact Professor Iain Stewart, Head of Department telephone (+44) (0)116 252 3885, e-mail i.a.stewart@mcs.le.ac.uk or Professor Rick Thomas, Deputy Head of Department telephone (+44) (0)116 252 3411, email rmt@mcs.le.ac.uk, who will be pleased to discuss the Lectureships further. Information about all aspects of the Department is available from its World Wide Web pages [http://www.mcs.le.ac.uk]. Further particulars and application forms are available, by quoting the reference A5365/GD, from Personnel Office, University of Leicester, University Road, Leicester LE1 7RH, U.K telephone (+44) (0)116 252 2439 email jobs@le.ac.uk, or via http://www.le.ac.uk/personnel/jobs The closing date for applications is 16 June 2000. From rrosebru@mta.ca Thu Jun 1 09:44:02 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA20358 for categories-list; Thu, 1 Jun 2000 09:38:54 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Martin Escardo MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14645.699.672815.431918@mosstowie.dcs.st-and.ac.uk> Date: Wed, 31 May 2000 13:16:59 +0100 (BST) To: categories@mta.ca Subject: categories: Pataraia X-Mailer: VM 6.71 under 21.1 (patch 3) "Acadia" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Thanks to all of you who replied to my query. Dito Pataraia has kindly sent me a copy of his manuscript. Here are the details of the short note I've written based on that. ---------------------------------------------------------------------- On the nuclear reflection of a prenucleus ---------------------------------------------------------------------- There are at least three ways of obtaining the nuclear reflection of a prenucleus. We describe a fourth, based on an intuitionistic version of Tarski's fixed-point theorem due to Pataraia. As an illustration of the technique, we offer a simple intuitionistic proof of Johnstone's localic version of the Hofmann-Mislove theorem, which says that the compact fitted sublocales of any locale are in order-reversing bijection with the Scott open filters of opens. ---------------------------------------------------------------------- Available as http://www.dcs.st-and.ac.uk/~mhe/papers/nuclei.ps (and also gzipped, dvi etc.) From rrosebru@mta.ca Thu Jun 1 09:44:14 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA15881 for categories-list; Thu, 1 Jun 2000 09:44:09 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: John MacDonald Date: Wed, 31 May 2000 09:58:25 -0700 (PDT) Message-Id: <200005311658.JAA15008@pascal.math.ubc.ca> To: categories@mta.ca Subject: categories: FMCS2000 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: FMCS2000 Foundational Methods in Computer Science JUNE 1st - 4th, 2000 The Department of Mathematics at the University of British Columbia, in cooperation with the Pacific Institute of Mathematical Sciences, is hosting the Foundational Methods in Computer Science workshop from June 1 to June 4, 2000, on the University of British Columbia Campus in Vancouver, B.C., Canada. The workshop is an informal meeting to bring together researchers in mathematics and computer science with a focus on the applications of category theory in computer science. The reception in the evening of June 1, 2000, at Walter Gage Towers, is followed by a day of tutorials aimed at students and newcomers to category theory, followed by a day and a half of research talks. There will be a few invited presentations, but the majority of the talks are solicited from the participants. Student participation is particularly encouraged at FMCS. PARTICIPANT LIST (as of May 26, 2000) Jeremy Bem, University of California, Berkeley David Benson, Washington State University Robin Cockett, University of Calgary Bridget Gilbride, University of British Columbia Eraldo Giuli, University of L'Aquila, Italy Dana Harrington, University of Calgary John MacDonald, University of British Columbia Ernest Manes, University of Massachusetts at Amherst Stefan Milius, York University Philip Mulry, Colgate University James Otto, Illinois Cristina Pedicchio, University of Trieste Vaughan Pratt, Stanford University Robert Seely, McGill University Peter Selinger, University of Michigan Lebelo Serutla, National University of Lesotho Robert Schneck, University of California, Berkeley Manuela Sobral, University of Coimbra, Portugal Art Stone, Vancouver Walter Tholen, York University Varmo Vene, Estonia Min Zeng, University of Calgary AGENDA Thursday, June 1, 2000 after 3:00p.m. Gage residence rooms available for check-in 6:00p.m. Welcome Reception - Mary Murrin Lounge -Gage Residence Friday, June 2, 2000 Tutorial Sessions - Room 216 - 1933 West Mall 9:00-10:30a.m. Ernie Manes - Monads of Sets: The Threefold Way 10:30-11:00a.m. Break 11:00-12:30p.m. Robin Cockett - Partial Map Categories, Partial Map Classification and Restriction Categories 12:30-2:00p.m. Lunch 2:00-3:30p.m. Peter Selinger - Categorical Models of Communication 3:30-4:00p.m. Break 4:00-4:30p.m. John MacDonald - Kleisli structures 4:30-5:30p.m. David Benson - Accessible Categories and Sketches Saturday, June 3, 2000 9:00-10:30a.m. Vaughan Pratt - Modeling Higher Dimensional Automata with Chu Spaces 10:30-11:00a.m. Break 11:00-11:45a.m. Robert Seely - The Logic of Finite Sums and Products 11:45-12:30p.m. Walter Tholen - Exponentiability 12:30-2:00p.m. Lunch 2:00-2:30p.m. Stefan Milius - TBA 2:30-3:00p.m. Varmo Vene - Mendler-style Recursion Schemes for Inductive Types 3:00-3:30p.m. Lebelo Serutla - Automated Handling of Grammatically Incorrect Sentences in MT 3:30-4:00p.m. Break 4:00-4:30p.m. Jeremy Bem -"Utopias", or Categories whose Codomain Fibration is Small: Another Foundation for Mathematics? 4:30-5:30p.m. Philip Mulry - TBA 6:30p.m. Banquet - Ponderosa Bldg. Sunday, June 4, 2000 9:00- 9:30a.m. Eraldo Giuli - Zariski Closure and Algebraic Objects 9:30-10:00a.m. Manuela Sobral - Reiterman-Tholen Maps for Finite Topological Spaces 10:00-10:30a.m. Robin Cockett - TBA 10:30-11:00a.m. Break 11:00-11:30a.m. Dana Harrington - TBA 11:30-12:00 James Otto - Abstract and Concrete Computation Categories 12:00-12:30p.m. Ernie Manes - Submonads Determined by Shape Further information about FMCS2000 may be obtained from the conference website at http://www.pims.math.ca/science/2000/fmcs . You may also obtain housing and registration forms by sending email to johnm@math.ubc.ca with subject heading FMCS2000. Those faculty, teachers and students from the local area with some graduate level training in mathematics or computer science or with an interest in logic and foundations are encouraged to attend some or all of the talks. If you think you may attend any of the talks, then please send email to johnm@math.ubc.ca so that we can estimate the number of those attending.