From rrosebru@mta.ca Sat Apr 1 19:51:50 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id TAA13002 for categories-list; Sat, 1 Apr 2000 19:43:14 -0400 (AST) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Sat, 1 Apr 2000 14:44:04 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Curious fact Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Has anyone seen this before, or can anyone give a principled explanation. Begin with the following observation. Suppose del del ... -----> (C_n,d) -----> (C_{n-1},d) ---> ... ---> (C_0,d) --> 0 is a chain complex of differential abelian groups, except that we assume d.del = -del.d. Suppose (C_n,d) is exact for each n. Let C be the direct sum of the C_n with boundary given by the matrix ( d 0 0 ... ) ( del d 0 ... ) ( 0 del d ... ) ( . . . . ) ( . . . . ) ( . . . . ) The finite truncations F^n = C_0 +...+ C_n are readily shown to be exact: F^0 = C_0 is by hypothesis and there is an exact sequence 0 --> F^{n-1} --> F^n --> C_n --> 0. AB5 now shows that the direct limit, which is C, is exact. Of course, this is going to be false for a category, such as compact abelian groups, that is not AB5. Except it is true. Using duality, we can translate it to the following statement for abelian groups. Suppose del del ... <----- (C_n,d) <----- (C_{n-1},d) <--- ... <--- (C_0,d) <-- 0 is a cochain complex of differential abelian groups, except that we assume d.del = -del.d. Suppose (C_n,d) is exact for each n. Let C be the direct product of the C_n with boundary given by the matrix ( d del 0 ... ) ( 0 d del ... ) ( 0 0 d ... ) ( . . . . ) ( . . . . ) ( . . . . ) then C is exact. The proof is by using elements and although AB4 (at least countable) is clearly a necessary condition for this (it is the case that all the del's are 0), it sure doesn't look sufficient. BTW, both are false if you change direct sum to product in the first or product to sum in the second. Michael From rrosebru@mta.ca Mon Apr 3 10:22:13 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA04185 for categories-list; Mon, 3 Apr 2000 10:12:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mailing-List: contact mpc2000cfp-help@di.uminho.pt; run by ezmlm X-No-Archive: yes Delivered-To: mailing list mpc2000cfp@di.uminho.pt Date: Mon, 3 Apr 2000 08:42:20 +0100 (WET) From: Jose Bernardo Barros X-Sender: jbb@lmf.logica.di.uminho.pt To: categories@mta.ca Subject: categories: MPC2000: call for participation Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id IAA13186 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: [Apologies for any duplicates you may receive] CALL FOR PARTICIPATION MPC 2000 5th International Conference on MATHEMATICS OF PROGRAM CONSTRUCTION ----------------------------------- http://www.di.uminho.pt/mpc2000 3--5 July, 2000 Ponte de Lima, Portugal Welcome to the Fifth International Conference on MATHEMATICS OF PROGRAM CONSTRUCTION which will take place in Ponte de Lima, a little historical town in the province of Minho, North of Portugal, in the first week of July 2000. Detailed information including the conference's on-line registration form is available from the above website. INVITED SPEAKERS Cliff Jones (Newcastle, UK) Jan Rutten (CWI, The Netherlands) Mark Jones (Oregon, USA) CONFERENCE PROGRAMME Monday July 3 2000 8.50 - 9.00 Welcome Session 1. Chair: Roland Backhouse (University of Nottingham) 9.00 - 10.00 Invited talk: Integrating Programming, Properties, and Validation Mark Jones (Oregon Graduate Institute, USA) 10.00 - 10.30 Break Session 2. Chair: Johan Jeuring (Utrecht University) 10.30 - 11.15 Polytypic values possess polykinded types Ralf Hinze (Institute für Informatik III, Universität Bonn) 11.15 - 12.00 The Zip Calculus Mark Tullsen (Department of Computer Science, Yale University) 12.00 - 14.00 Lunch Session 3. Chair: Lindsay Groves (Victoria University of Wellington) 14.00 - 14.45 Separation and Reduction Ernie Cohen (Telecordia Technologies) 14.45 - 15.30 Using Deadline Commands to Reason about Non-Terminating Loops Ian Hayes (Dept. of Computer Science and Electrical Engineering, The University of Queensland, Brisbane) 15.30 - 16.00 Break Session 4. Chair: Christian Lengauer (Universität Passau) 16.00 - 16.45 Quantum Programming J. Sanders and P. Zuliani (PRG, Oxford University Computing Laboratory, Oxford) 16.45-17.30 «Hot topic » Session. Coordination: Richard Bird (Oxford University Computing Laboratory) 18.00-19.30 Reception at the Old Prision Tower Tuesday July 4 2000 Session 5. Chair: Lambert Meertens (Kestrel Institute, USA) 9.00 - 10.00 Invited talk: Regular Expressions Revisited: a Coinductive Approach to Streams, Automata, and Power Series Jan Rutten (CWI, The Netherlands) 10.00 - 10.30 Break Session 6. Chair: Bernhard Möller (Universität Augsburg) 10.30 - 11.15 Pointer aliasing in Hoare Logic Richard Bornat (Department of Computer Science, Queen Mary and Westfield College,University of London) 11.15 - 12.00 On Guarded Commands with Fair Choice Emil Sekerinski (Department of Computing and Software, McMaster University, Hamilton, Ontario) 12.00 - 14.00 Lunch 15.00-19.00 Sight-seeing Tour 19.30- Banquet at the Monastery of Refóios do Lima Wednesday July 5 2000 Session 7. Chair: J.N. Oliveira (Universidade do Minho) 9.00 - 10.00 Invited talk: Formal Methods and Dependability Cliff Jones (University of Newcastle, UK) 10.00 - 10.30 Break Session 8. Chair: Oege de Moor (Oxford University Computing Laboratory) 10.30 - 11.15 Liberating Data Refinement Eerke Boiten and John Derrick (Computing Laboratory, University of Kent, Canterbury) 11.15 - 12.00 Theorems about composition Michel Charpentier (Computer Science Department, University of New Hampshire, Durham) and K. Mani Chandy (Computer Science Department, California Institute of Technology, Pasadena) 12.00 - 14.00 Lunch Session 9. Chair: Jeremy Gibbons (Oxford University Computing Laboratory) 14.00 - 14.45 The Universal Resolving Algorithm: Inverse Computation in a Functional Language Sergei Abramov (Program Systems Institute, Russian Academy of Sciences) and Robert Glueck (Department of Information and Computer Science, Waseda University, Tokyo) 14.45 - 15.30 Metacomputation-based Compiler Architecture William L. Harrison (Department of Computer Science, Indiana University, Bloomington) and Samuel N. Kamin (Department of Computer Science, University of Illinois, Urbana) 15.30 - 16.00 Break Session 10. Chair: Eugenio Moggi (DISI, Univ. di Genova) 16.00 - 16.45 A Meta Language for Programming with Bound Names Modulo Renaming (Preliminary Report) Andrew M. Pitts (Cambridge University Computer Laboratory, Cambridge) and Murdoch J. Gabbay (Department of Pure Mathematics and Mathematical Statistics, Cambridge University) 16.45-17.30 «Hot topic » Session. Coordination: Richard Bird (Oxford University Computing Laboratory) 17.30- Closing session CO-LOCATED WORKSHOPS Four workshops are taking place in the same week co-located with the conference: CMPP 2000 - 2nd International Workshop on Constructive Methods for Parallel Programming; WGP 2000 - 2nd International Workshop on Generic Programming; DTP 2000 - International Workshop on Subtyping and Dependent Types in Programming; and WAGA 2000 - 3rd International Workshop on Attribute Grammars and their Applications. REGISTRATION Registration is available on-line from the conference website. For any questions concerning the venue, accommodation, registration etc please get in touch with Ms. Carla Oliveira (mpc2000@di.uminho.pt) or any member of the Organizing Committee. ORGANIZING COMMITTEE P.R. Henriques (prh@di.uminho.pt), L.S. Barbosa (lsb@di.uminho.pt), J.B. Barros (jbb@di.uminho.pt) PROGRAMME COMMITTEE Roland Backhouse (cochair, UK) Richard Bird (UK) Eerke Boiten (UK) Dave Carrington (Australia) Jules Desharnais (Canada) Jose Fiadeiro (Portugal) Jeremy Gibbons (UK) Lindsay Groves (New Zealand) Zhenjiang Hu (Japan) John Hughes (Sweden) Johan Jeuring (The Netherlands) Burghard von Karger (Germany) Dick Kieburtz (USA) Carlos Kloos (Spain) K. Rustan M. Leino (USA) Christian Lengauer (Germany) Lambert Meertens (The Netherlands) Sigurd Meldal (Norway) Eugenio Moggi (Italy) Bernhard Moeller (Germany) Oege de Moor (UK) Dave Naumann (USA) Jose Oliveira (cochair, Portugal) Kaisa Sere (Finland) Mark Utting (New Zealand) Phil Wadler (USA) FURTHER INFORMATION Please refer to the web page for further details. http://www.di.uminho.pt/mpc2000 Alternatively, email: mpc2000@di.uminho.pt or contact a member of the Organizing Committee. From rrosebru@mta.ca Mon Apr 3 20:02:43 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA23577 for categories-list; Mon, 3 Apr 2000 20:00:08 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Mon, 3 Apr 2000 18:12:19 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: AB4.5 Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: A day after I sent my previous note, I realized the (or an) answer. In fact, I seem to have discovered a new infinite exactness condition that is between AB4 and AB5 and, inevitably, I call AB4.5. So far I know only that it is implied by AB5, implies AB4 and, since module categories satisfy both AB5 and AB4.5*, it is definitely weaker than AB5. I do not, at this time, know that it is stronger than AB4. Here is how it works. Call a poset superdirected if it is directed and all down segments are finite. The natural numbers is one example and the set of finite subsets of any set is another. If I is superdirected, A an abelian category and F,G: I --> A are two diagrams, say that a natural transformation alpha: F --> G is supernatural (OK, suggestions for better names welcome) if for any i in I, the following: Look at the diagram consisting of all the Fj for j =< i and all the Gj for j < i. The arrows in the diagram are all the alpha j, for j =< i, as well as all the arrows from the restrictions of F and G. The diagram has a cocone to Gi and that cocone is monic (meaning the natural map from the colimit to Gi is monic) for each i in I, call alpha supernatural. Now the condition is that whenever alpha is supernatural, the induced colim F --> colim G is monic. To see that this implies AB4, suppose for all x in X, A_x >--> B_x. Let I consist of all the finite subsets of X. For i in I, let Fi be the direct sum of all the A_x, x in i and Gi be the direct sum of the correspnding B_x. The supernaturality is satisfied and hence the sum of the A_x maps monically to the sum of the B_x. The application to my question comes as follows. To recall, I am supposing that del del ... -----> (C_n,d) -----> (C_{n-1},d) ---> ... ---> (C_0,d) --> 0 is a chain complex of differential abelian groups, except that we assume d.del = -del.d. Suppose (C_n,d) is exact for each n. Let C be the direct sum of the C_n with boundary given by the matrix ( d 0 0 ... ) ( del d 0 ... ) ( 0 del d ... ) ( . . . . ) ( . . . . ) ( . . . . ) The finite truncations F^n = C_0 +...+ C_n are readily shown to be exact: F^0 = C_0 is by hypothesis and there is an exact sequence 0 --> F^{n-1} --> F^n --> C_n --> 0. Thus each F^n is exact. Now let Z^n and B^n be the kernel and image, resp. of the boundary operator on F^n. Then the rows of 0 ----> Z^n -------> F^n -------> B^n ----> 0 | | | | | | | | | v v v 0 --> Z^{n+1} ---> F^{n+1} ---> B^{n+1} --> 0 Since the right hand vertical arrow is monic, it follows that the left hand square is a pullback, which in turn implies that the induced map F^n +_{Z^n} Z^{n+1} ---> F^{n+1} is monic. Taking colimits, and using this Ab4.5 condition together with the right exactness of colimits implies that 0 --> colim Z^n --> C --> B --> 0 is exact, so that Z = colim Z^n and then B^n = Z^n for all n implies B = Z. As for AB4.5* on module categories (for which it is sufficient to prove it for Ab), it is a bit complicated notationally for this medium, but not hard. The point is that when you try to construct an element in the inverse limit, the crucial thing is that you can do it one index at a time and no choice you make at an earlier stage ever has to be changed at a later one, so you can just continue. Of course, AC is involved. This might a way to find a category that satisfies AB4*, but not AB4.5*; the trouble is that AC is also used to show AB4*. Michael From rrosebru@mta.ca Tue Apr 4 17:14:20 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA21947 for categories-list; Tue, 4 Apr 2000 16:14:28 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Tue, 4 Apr 2000 11:08:32 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: just to be sure (fwd) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Of course, Peter is correct below, since Gi is not part of the diagram (although Fi is). One more thing. The reason that B^n --> B^{n+1} is monic (which is crucial) is that they are subgroups of F^n and F^{n+1} resp. One thing I found curious is that in any commutative diagram with exact rows 0 ----> A -----> B -----> C -----> 0 | | | | | | | | | v v v 0 ----> A' ----> B' ----> C' ----> 0 if C ---> C ' is monic, then so is A' +_A B ---> B'. Well it turns out that there is an exact sequence 0 ---> ker (C --> C') ---> A' +_A B ---> B' I don't see this as coming from the snake lemma, but who knows. ---------- Forwarded message ---------- Date: Tue, 4 Apr 2000 09:33:34 -0400 (EDT) From: Peter Freyd To: barr@barrs.org Subject: just to be sure The first inequality below should be j < i? The arrows in the diagram are all the alpha j, for j =< i, as well as all the arrows from the restrictions of F and G. The diagram has a cocone to Gi and that cocone is monic (meaning the natural map from the colimit to Gi is monic) for each i in I, call alpha supernatural. Now the condition is that whenever alpha is supernatural, the induced colim F --> colim G is monic. From rrosebru@mta.ca Wed Apr 5 10:45:19 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA29740 for categories-list; Wed, 5 Apr 2000 10:44:36 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Tue, 4 Apr 2000 21:18:03 -0400 (EDT) From: "Robert A.G. Seely" To: Categories List Subject: categories: Categories with finite products and coproducts Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: We wish to announce the following paper, which has been placed on the triples web and ftp site (urls given below). Finite sum - product logic J.R.B. Cockett R.A.G. Seely University of Calgary and McGill University robin@cpcs.ucalgary.ca rags@math.mcgill.ca Brief Abstract: In this paper we describe a deductive system for categories with finite products and coproducts, prove decidability of equality of morphisms via cut elimination, and prove a "Whitman theorem" for the free such categories over arbitrary base categories. This result provides a nice illustration of some basic techniques in categorical proof theory, and also seems to have slipped past unproved in previous work in this field. Notes: Since this material might seem rather close to the sort of categorical proof theory done in the past 2-3 decades, we feel we ought to point out some features which distinguish it from what others have done. Some comments concerning its novelty might help the reader attune himself to some points that otherwise might slip past unnoticed. We present a correspondence between the doctrine of categories with finite sums and products (without any assumption of distributivity), and a "Lambek style" deductive system. But note that unlike the work of Joyal's on the bicompletion of categories, our construction of the free category does not use an inductive chain of constructions, alternating between completions and cocompletions. In this finite case, it is natural do both finite completions (but only for sums and products) in one step. Our proof of cut elimination and Church--Rosser does not make sense without finiteness however. A comment: decidability for categories with finite sums and products seems a result that we ought not to have overlooked all this time, but we cannot find any reference to this in the literature. Of course, comments are welcome. Next, unlike the related work on categories with finite products (or sums, but not both), with or without cartesian closedness, we cannot rely only on directed rewrites ("reductions") but must also make essential use of two-way rewrites (which we might call "equations"). Hence we need to use the theory of reduction systems modulo equations; in particular, we need to strengthen an old result of Huet's in this connection. Our use of such systems to provide a decision procedure for the equality of derivations is not particularly common in categorical cut elimination, but it was a key ingredient in our earlier work on linearly distributive categories and *-autonomous categories [BCST]. Its reappearance here in a slightly different guise is one of the highlights of the present paper, we think. Finally, we drawn the reader's attention to the fact that in setting up the equivalence relation for the category induced by the deductive system, we need not assume the categorical axioms of identity (apart from atomic instances) and associativity - these follow from the cut elimination process. This is not unusual in working with free logics, but may be somewhat less familiar to the reader in the present case of logic over an arbitrary category. Small points individually, but together they give this result a slightly different flavour from its long-familiar relations. ............................................. The paper may be found on the McGill ftp site ftp://ftp.math.mcgill.ca/rags/sigmapi/sigmapi.ps.gz or from rags' web page http://www.math.mcgill.ca/rags ================== R.A.G. Seely From rrosebru@mta.ca Wed Apr 5 23:39:37 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA16009 for categories-list; Wed, 5 Apr 2000 10:00:12 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 5 Apr 2000 12:39:05 +0200 (MET DST) From: Riccardo Focardi To: Riccardo Focardi Subject: categories: WITS'00 -- last call for paper Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Apologies for multiple copies. ************************************************************************* Last Call for Papers ==================== Workshop on Issues in the Theory of Security (WITS '00) University of Geneva, Switzerland 7,8 July 2000 http://www.dsi.unive.it/IFIPWG1_7/wits2000.html Co-located with ICALP '00, the 27th International Colloquium on Automata, Languages, and Programming (9 to 15 July 2000) http://cuiwww.unige.ch/~icalp/ ************************************************************************* IMPORTANT DATES/DEADLINES: Submission of papers: *** 15 April 2000 *** Notification of acceptance: 31 May 2000 Workshop: 7,8 July 2000 OVERALL TOPIC AND FORMAT OF WORKSHOP: The IFIP WG 1.7 on "Theoretical Foundations of Security Analysis and Design" has been recently established to investigate the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications. The members of WG will hold their annual workshop as an open event to which all researchers working on the theory of computer security are invited. The program will encourage discussions by all attendees, both during and after scheduled presentations on participants' ongoing work. Extended abstracts of work presented at the Workshop will be collected and distributed to the participants; no proceedings are foreseen for this year's workshop. POSSIBLE TOPICS FOR SUBMITTED PAPERS: Researchers are invited to submit abstracts of original work on topics in the spirit of the workshop. Possible topics for submitted papers include, but are not limited to: - formal definition and verification of the various aspects of security: confidentiality, integrity, authentication and availability; - new theoretically-based techniques for the formal analysis and design of cryptographic protocols and their manifold applications (e.g., electronic commerce); - information flow modelling and its application to the theory of confidentiality policies, composition of systems, and covert channel analysis; - formal techniques for the analysis and verification of mobile code; - formal analysis and design for prevention of denial of service. ORGANISING COMMITTEE: Pierpaolo Degano (chair) (Universita` di Pisa, I) Riccardo Focardi (Universita` di Venezia, I) Cathy Meadows (Naval Research Laboratory, USA) Paul Syverson (Naval Research Laboratory, USA) Joshua Guttman (Mitre, USA) SUBMISSION INSTRUCTIONS: Authors are invited to submit an extended abstract, 1-2 pages long, through the web. Instructions for electronic submissions can be found at the Workshop home page. Alternatively, they may e_mail a .ps file, or may mail a single copy of their paper to the program chair; in the last case, please allow ample time for delivery. Submissions should have the author's full name, address, fax number, e-mail address. VENUE: The workshop is co-located with the ICALP '00 conference, which will be held at the University of Geneva. Accommodations at a special ICALP rate have been reserved in a couple of hotels and very inexpensive rooms will be available at the Student Housing. Lunch will be served daily on campus and there will be morning and afternoon refreshment breaks. For more details see the ICALP '00 web address given above. CONTACT INFORMATION: Web: http://www.dsi.unive.it/IFIPWG1_7/wits2000.html Program chair: Pierpaolo Degano e-mail: degano@di.unipi.it telephone: +39 050 887257 fax: +39 050 887226 postal: Dipartimento di Informatica Universita' degli Studi di Pisa Corso Italia, 40 I-56125 PISA, Italia From rrosebru@mta.ca Fri Apr 7 10:36:16 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA03206 for categories-list; Fri, 7 Apr 2000 10:29:49 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Thu, 6 Apr 2000 18:04:15 -0400 (EDT) From: "Robert A.G. Seely" To: Categories List Subject: categories: Correction to paper announcement (ftp URL) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Earlier I posted an announcement of a paper Finite sum - product logic by J.R.B. Cockett R.A.G. Seely University of Calgary and McGill University robin@cpcs.ucalgary.ca rags@math.mcgill.ca But there was a slight error in the ftp URL given (the http url was correct however). The paper may be found at: rags web page: http://www.math.mcgill.ca/rags/ or McGill Maths ftp site: ftp://ftp.math.mcgill.ca/pub/rags/sigmapi/sigmapi.ps.gz ftp://ftp.math.mcgill.ca/pub/rags/sigmapi/sigmapi.dvi.gz ================== R.A.G. Seely From rrosebru@mta.ca Sun Apr 9 11:13:36 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA11916 for categories-list; Sun, 9 Apr 2000 11:06:28 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Sender: audersec@f-user.unifr.ch (Unverified) Message-Id: Date: Sun, 9 Apr 2000 14:41:38 +0200 To: categories@mta.ca From: Claude Auderset Subject: categories: CATOP 2000 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id JAA17653 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Conference C A T O P 2 0 0 0 (Third and last announcement) to be held at the University of Fribourg (Switzerland), 4-6 July, 2000. TOPIC: It is the aim of this conference to discuss categorical topological methods that are likely to be mathematically important in the next century. Furthermore, on Thursday afternoon resp. evening, we shall celebrate the seventieth birthday of Professor Heinrich Kleisli (Fribourg). Those interested in attending only the birthday celebration or the following banquet should not forget to register, too; see below. Of course, they need not pay the registration fee. Titles of the eight invited two hour lectures: A. ARHANGEL'SKII (Moscow, Russia): Topological and paratopological groups and homogeneous spaces. M. BARR (Montreal, Canada): The *-autonomous category of Mackey spaces. MARIA M. CLEMENTINO (Coimbra, Portugal): Closure operators. KATHRYN P. HESS (Lausanne, Switzerland): Model categories in algebraic topology. R. LOWEN (Antwerp, Belgium): Approach spaces. HILARY A. PRIESTLEY (Oxford, England): Duality theory. D. PUMPLUEN (Hagen, Germany): Convex sets and Saks spaces (A paradigmatic case of applied category theory). S. WATSON (York, Canada): How to construct counterexamples in general and set-theoretic topology usefully with pullbacks. SHORT COMMUNICATIONS: Persons interested in giving a short communication are kindly asked to send a one page abstract of their talk by ordinary (air)mail to Prof. Heinrich Kleisli, Department of Mathematics, University of Fribourg, 1700 Fribourg, Switzerland, before April 20, 2000. Please note that the programme of the congress consists of the afore-mentioned 8 invited lectures (of 2 times 50 minutes each) and short communications (of 20 minutes each). Each participant who wishes to give a short communication will be informed by May 1, 2000, whether his or her talk is part of the final programme of the congress. PROCEEDINGS: In connection with the conference CATOP2000 a special volume of the Journal Applied Categorical Structures (www.wkap.nl/journalhome.htm/0927-2852; guest editor Hans-Peter Kuenzi) is to be published, which will be dedicated to Professor Heinrich Kleisli on the occasion of his seventieth birthday. Those who would like to submit a paper, should contact hans-peter.kuenzi@math-stat.unibe.ch as soon as possible. ACCOMMODATION: The hotels (and student residences) are located near the railway station. The prices are as follows (breakfast included): Single room: 90 sFr. up, Double room: 140 sFr. up. Student residence: Single room (~45 sFr.) Double room (~35 sFr./pers.) TRAVELLING TO FRIBOURG: Intercity trains connect Fribourg with the international airports of Geneva and Zurich. Talks will take place in the Chemistry Building, Perolles-site of the University of Fribourg, close to the centre of the town. There is a bus from the railway station to Perolles, bus-stop Charmettes, where you face the buildings of the Perolles-site of the University. Further information about the congress (e.g. campus and town maps) can be obtained via its homepage: www.unifr.ch/math/catop2000 REGISTRATION: A participation fee of 100 sFr. (Swiss francs) will be paid by each participant. The participation of the Thursday afternoon lectures is free. The ticket for the (optional) banquet on Thursday night costs additional 80 sFr. Please indicate in the registration form below how many tickets for the banquet you need. The deadline for paying the registration fee and tickets is April 10, 2000. Please make money orders payable to Banque Cantonale, CATOP2000, Inst. Math., CH-1700 Fribourg, account-no 25'01'016.390-09, b.cl. 768, or CCP 17-49-3, CATOP2000, Inst. Math., account-no 25'01'016.390-09. The registration desk will open on the ground floor of the Chemistry Building on Tuesday morning at 8.00. Email facilities will be available to participants during the conference. The organizers strongly recommend electronic preregistration via our homepage mentioned above. Persons who have no access to Internet may also fill in the preregistration form given below and send it to one of the following addresses of the congress: Email: catop2000@unifr.ch (Air)mail: Catop2000, Department of Mathematics, University of Fribourg, 1700 Fribourg, Switzerland Note that after April 10 hotelrooms will have to be booked directly via the local tourist information bureau, possibly at a higher price. We look forward to meeting you in Fribourg. The organizing committee of CATOP 2000: Ernst Ruh (Fribourg), Hans-Peter Kuenzi (Bern), Claude Auderset (Fribourg). ========================================================================= Preregistration Form (before 10th April, 2000) ------------------------------------------------------------------------- Registration Details: Family name (please print): First name: Affiliation: Mailing address (if different): Email: Fax: Arrival date: Departure date: I shall arrive with accompanying persons. I need tickets for the banquet. [ ] I would like to have a vegetarian menu. Visa support: I need an official invitation: yes/no accommodation needed: yes/no accommodation in student residence: single/ double room in hotel: single / double room Additional remarks: -------------------------------- From rrosebru@mta.ca Tue Apr 11 14:52:32 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA03486 for categories-list; Tue, 11 Apr 2000 14:44:11 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Tue, 11 Apr 2000 11:56:27 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: AB4.5 Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: The file ab45.zip, that includes both the dvi and ps version, is now available at ftp.math.mcgill.ca/pub/barr. It is a preliminary version because I want to investigate if the condition is really stronger than AB4. The following consideration raises the possibility that it might not be. One place to look to distinguish AB4* from AB4.5* might be in the abelian groups of a topos. But in order for the abelian groups of a topos to satisfy AB4*, you need AC (in the topos). But AC implies dependent choice and then it looks like you have AB4.5*, which really is just like dependent choice. Michael From rrosebru@mta.ca Fri Apr 14 15:05:32 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA15699 for categories-list; Fri, 14 Apr 2000 15:01:41 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: exmh version 2.0.2 2/24/98 To: categories@mta.ca, concurrency@cwi.nl Subject: categories: LICS Workshop on Chu Spaces and Applications 25th June 2000, Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii From: Valeria Correa Vaz de Paiva Message-Id: <00Apr14.100139pdt."79848"@panini.parc.xerox.com> Date: Fri, 14 Apr 2000 10:01:58 PDT Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Final CALL FOR PAPERS LICS'2000 Workshop on Chu Spaces: Theory and Applications Sunday, June 25, 2000, Santa Barbara, California http://www.cs.bham.ac.uk/~vdp/chu.html ****Submission deadline: April,25, 2000**** A Chu space is a related pair of complementary objects. Besides having intrinsic interest in their own right, Chu spaces have found applications to concurrent processes, information flow, linear logic, proof theory, and universal categories. The workshop is concerned with the theory and applications of Chu spaces, as well as related structures such as the Dialectica construction and double glueing. The workshop will bring together computer scientists, mathematicians, logicians, philosophers, and other interested parties to discuss the development of the subject with regard to its foundations, applications, prospects, and directions for future work. Work in the subject is currently fragmented across several areas: category theory, traditional model theory, concurrency, and the semantics of programming languages, and such a workshop can contribute to the coordination and possibly even some unification of these efforts. Suggested topics for presentation and discussion include but are by no means limited to new results about Chu spaces and related structures; their applications to various areas such as concurrency, games, proof theory, etc.; and their implications for foundations and philosophy of computation, mathematics, physics, and other disciplines. The workshop will be held on Sunday, June 25, 2000 at Santa Barbara, California, as an adjunct to the International Conference on Logic in Computer Science (LICS'2000), June 26-29 at the same location as per http://www.cs.bell-labs.com/who/libkin/lics/index.html. Papers within the scope of the workshop are solicited, and may be either work in progress or more mature work. Submission should be in the form of an extended abstract of at most 10 pages, in postscript format, mailed electronically to paiva@parc.xerox.com. Submissions will be evaluated by a committee selected by the organizers, and the full version of accepted papers will be printed in a proceedings available at the start of the workshop. Important dates: Extended abstract: April 25, 2000 Notification of acceptance: May 15, 2000 Proceedings version: June 9, 2000 The workshop will be one full day and is open to all interested researchers. Valeria de Paiva paiva@parc.xerox.com Vaughan Pratt pratt@cs.stanford.edu http://www.cs.bham.ac.uk/~vdp/chu.html From rrosebru@mta.ca Fri Apr 14 15:05:34 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA19715 for categories-list; Fri, 14 Apr 2000 15:01:04 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: jvoosten@math.uu.nl Date: Fri, 14 Apr 2000 16:38:00 +0200 (MET DST) Message-Id: <200004141438.QAA10363@kodder.math.uu.nl> To: categories@mta.ca Subject: categories: preprints available Cc: jvoosten@math.uu.nl X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: The following preprints are available from the WWW: Jaap van Oosten Realizability: A Historical Essay http://www.math.uu.nl/publications/preprints/1131.ps.gz Abstract: historical survey on Realizability. Focuses on notions of realizability used in the study of metamathematics of arithmetical theories, and topos-theoretic developments. Bibliography contains 96 items.24 pages Lars Birkedal and Jaap van Oosten Relative and Modified Relative Realizability http://www.math.uu.nl/publications/preprints/1146.ps.gz Abstract: We approach `relative realizability' from an abstract point of view, studying internal partial combinatory algebras in an arbitrary topos E. Let RT(E,A) denote the standard realizability topos over E w.r.t. A. We define the notion of `elementary subobject' in a topos; if, for two internal pca's A and B in E, there is an embedding which maps A as elementary subobject into B, there is a local geometric morphism from RT(E,B) to RT(E,A). Next we study the situation where an internal topology j is given; we have a tripos over E using only the j-closed subobjects of A, giving a topos RTj(E,A). RTj(E,A) is a subtopos of RT(E,A) and we have a pullback diagram of toposes: Sh_j(E)--->RTj(E,A) | | | | V V E ----> RT(E,A) If A--> B is an embedding with A elementary subobject of B, the local geometric morphism restricts to a local geometric morphism: RTj(E,B)-->RTj(E,A) Moreover if A --> B is a j-dense embedding, there is a logical functor (a filter-quotient situation): RTj(E,A) --> RTj(E,B). If j is an open topology, the inclusion RTj(E,A)-->RT(E,A) is open too, and it makes sense to consider its closed complement; we call this the modified relative realizability topos Mj(E,A) w.r.t. A and j. We have an automatic pullback diagram Sh_k(E)---->Mj(E,A) | | | | V V E ----> RT(E,A) where k denotes the closed complement of j. In a section `Examples' we show that our treatment generalizes former definitions of relative realizability (in Awodey, Birkedal, Scott) and modified realizability. 16 pages. From rrosebru@mta.ca Fri Apr 14 15:05:36 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id PAA14393 for categories-list; Fri, 14 Apr 2000 15:00:33 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: parigot@logique.jussieu.fr Date: Fri, 14 Apr 2000 16:37:06 +0200 Message-Id: <200004141437.QAA19865@herbrand.logique.jussieu.fr> To: categories@mta.ca Subject: categories: LPAR'2000: call for papers Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: [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 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 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. Programme Committee: * Stefano Berardi, Torino * Patrick Lincoln, SRI * Manfred Broy, Munich * David McAllester, AT&T Labs * Maurice Bruynooghe, Leuven * 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 * Giorgio Levi, Pisa * Pascal van Hentenryck, Providence * Leonid Libkin, Bell Labs * 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. Submitted "theoretical" papers should not be longer than 15 proceedings pages. Submitted "experimental" papers should not be longer than 10 proceedings pages. Instructions for submission will be on the conference web page: http://www.cs.man.ac.uk/~voronkov/LPAR/2000/general.html 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 Mon Apr 17 11:38:01 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA16485 for categories-list; Mon, 17 Apr 2000 11:30:32 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <38FB0DD2.DD7B2B@essex.ac.uk> Date: Mon, 17 Apr 2000 14:12:50 +0100 From: Wilkins E B Organization: University of Essex X-Mailer: Mozilla 4.6 [en] (X11; I; Linux 2.2.14 i686) X-Accept-Language: en MIME-Version: 1.0 To: Category mailing list Subject: categories: Osius' set theory Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Hello, In his 1974 paper Osius showed that there are enough transitive objects in the initial topos to define a naive set theory. He then goes on the assume his topoi are well-pointedness and produces a characterisation of the category of sets in terms familiar to set theorists. I'm wondering whether anyone has produced an axiomatic set theory from Osius' naive set theory which characterises the initial topos. -- Dr Elwood Wilkins e-mail: elwood@essex.ac.uk Senior Research Officer tel: (+44) (0)1206 872336 Department of Computer Science fax: (+44) (0)1206 872788 University of Essex, Colchester, Essex, UK From rrosebru@mta.ca Mon Apr 17 14:39:15 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA24854 for categories-list; Mon, 17 Apr 2000 14:10:34 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Paul Taylor Date: Mon, 17 Apr 2000 16:57:19 +0100 Message-Id: <200004171557.QAA06124@koi-pc.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: Osius' set theory Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Elwood Wilkins reminds us that... > In his 1974 paper Osius showed that there are enough transitive objects > in the initial topos to define a naive set theory. ... Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory. In fact Osius's is, so far as I am aware, the only work that discusses *set* theory - Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations, but set theory - epsilontics as Lawvere calls it - is of some interest in the study of very high powered induction. Peter Johnstone included a precis of Osius's paper in his book "Topos Theory" (Academic Press, 1977). Apart from that, I was unable to track down anything that built significantly on it. Indeed, Osius himself didn't seem very interested when I wrote to him about it (he now does statistics). The successor to this paper would therefore seem to be my "Intuitionistic Sets and Ordinals", J. Symbolic Logic, 61 (1996) 705--744 This develops, in a symbolic way, the notions of "transitive set" and "ordinal" in the sense of a carrier equipped with an extensional well founded relation. Several qualitatively different notions of ordinal arise intuitionistically. I also pick up on Osius's set theory and pose some questions that suggest ways of adapting it to Grothendieck toposes in general. What remains of considerable interest (once we have agreed that set theory is wrong, wrong, wrong) is Osius's categorical notion of recursion. The equation f(x) = r( { f(y) | y in [=element_of] x } ) he writes as the (3=1, not 2=2) commutative square P(f) { y | y in x } P(X) ---------> P(A) ^ ^ | | | | | | | | | | r | | | | | | - | f v x X -------------> A which we may of course generalise to a "homomorphism" from any P-coalgebra to any P-algebra, where indeed P may be any functor instead of the covariant powerset functor. The coalgebra admits recursion by definition if there is exactly one such "homomorphism" to any algebra whatever. The exercises in Chapter VI of my book "Practical Foundations of Mathematics" (Cambridge University Press, 1999) explore applications of the commutative square to recursive functional programs. http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s6e.html Osius's 3+1 square is about RECURSION - defining functions or programs - but I have also considered INDUCTION - proving theorems - categorically. Again this is a property ("well foundedness") of coalgebras. See Section 6.3 http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/s63.html of the book, or my unfinished paper "Towards a Unified Treatment of Induction" (also known as "On the General Recursion Theorem") which you can get from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP The final section of the book (s96.html) sketches the way in which this categorical notion of ordinal can be used to define transfinite iterates of a functor (for example, internally in a topos). I hope to use this to develop categorical notions of the Axiom of Replacement. Paul Taylor From rrosebru@mta.ca Thu Apr 20 14:57:23 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA04844 for categories-list; Thu, 20 Apr 2000 14:52:52 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <38FDD625.A3AD2CB4@essex.ac.uk> Date: Wed, 19 Apr 2000 16:52:05 +0100 From: Wilkins E B Organization: University of Essex X-Mailer: Mozilla 4.6 [en] (X11; I; Linux 2.2.14 i686) X-Accept-Language: en MIME-Version: 1.0 To: Category mailing list Subject: categories: Re: Osius' set theory Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Paul Taylor wrote: > > Gerhard Osius's work was significant in 1974 as one of the ways in which > it was shown that toposes do the same thing as set theory. Osius showed that well-pointed topoi do essentially the same thing as set theory. I have yet to find any adequate analogy between what elementary topoi in general do and set theory. The problem being, as far as I can see, that classical set theory finds it very difficult to describe the rather more subtle behaviour occurring in the initial topos. Whence the standard set theoretic account of topos logic includes the assumption that bound variables denote, which make the semantics of elementary topoi almost identical to those of well-pointed ones (for instance every proper subtype of 1 is treated as though it is empty!). > In fact Osius's > is, so far as I am aware, the only work that discusses *set* theory - > Benabou, Joyal, Mitchell, Lawvere etc showed that toposes do the same thing > as some form of *type* theory. Of course, it is the latter that > mathematicians actually use when they claim to be using set theory > as foundations ... In practice this is true, but not if they're interested in actually studying the foundations of maths. My (set minded) colleagues point out (quite forcibly) that unless something is expressible in ZF (say) then they find it hard to accept, a view that appears to be widespread in the theoretical end of computer science. Now I have the practical problem of convincing people that what I do constructively is better than what they do with their "bound variables denote" assumptions, and an axiomatic set theory equivalent to the initial topos would make this much easier: they could go away contentedly believing that I'm really doing set theory (while I can be happy with the knowledge that they're doing typed theory). There are potential applications to category theory from producing a set theory. For instance one might speculate that this set theory could replace the rather cumbersome Freyd cover in the proof of the constructive properties of the initial topos. A host of other speculations can be formulated ... Elwood -- Dr Elwood Wilkins e-mail: elwood@essex.ac.uk Senior Research Officer tel: (+44) (0)1206 872336 Department of Computer Science fax: (+44) (0)1206 872788 University of Essex, Colchester, Essex, UK From rrosebru@mta.ca Thu Apr 20 14:57:23 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA05708 for categories-list; Thu, 20 Apr 2000 14:53:42 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 20 Apr 2000 14:49:22 +0200 From: matthieu amiguet Subject: categories: process algebras To: categories@mta.ca Reply-to: matthieu.amiguet@info.unine.ch Message-id: <38FEFCD1.A189A453@info.unine.ch> MIME-version: 1.0 X-Mailer: Mozilla 4.5 [fr] (Macintosh; I; PPC) Content-type: text/plain; charset=us-ascii Content-transfer-encoding: 7BIT X-Accept-Language: fr References: <200004171557.QAA06124@koi-pc.dcs.qmw.ac.uk> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Dear categoricians, 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? Thank you for your help, Matthieu Amiguet From rrosebru@mta.ca Thu Apr 20 14:57:28 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA10176 for categories-list; Thu, 20 Apr 2000 14:54:54 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 20 Apr 2000 15:46:39 +0100 (BST) From: Marta Z Kwiatkowska Message-Id: <200004201446.PAA05020@chip.cs.bham.ac.uk> To: categories@mta.ca Subject: categories: Lectureships in Computer Science at Birmingham Cc: M.Z.Kwiatkowska@cs.bham.ac.uk X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Lectureship in Computer Science (3 posts) *** Closing date: 16th May 2000 *** Applications are invited for THREE Lectureships in Computer Science at the University of Birmingham. All areas will be considered, but preference will be given to candidates who are research active in areas listed below: Vision Computational Linguistics Commonsense Reasoning Robotics Agents Advanced Interaction Technology & Software Systems Verification Bioinformatics Evolutionary and Natural Computation For more information see http://www.bham.ac.uk/personnel/s35434.htm Informal enquiries to Prof Achim Jung (Head of School), Email A.Jung@cs.bham.ac.uk, tel +44 121 414 4776. From rrosebru@mta.ca Thu Apr 20 14:57:35 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA10054 for categories-list; Thu, 20 Apr 2000 14:57:26 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <00cd01bfaa97$c1ed4800$4ae1fea9@tmp-sabadini.fis.unico.it> From: "RFC Walters" To: Subject: categories: CT 2000: Registration and Accomodation Date: Thu, 20 Apr 2000 09:11:34 +0200 MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: CATEGORY THEORY 2000 (CT 2000) July 16-22, 2000 Centro di Cultura Scientifica "Alessandro Volta" di Villa Olmo Como, Italy REGISTRATION and booking of ACCOMODATION for CT 2000 is now possible through the web page for the conference http://www.disi.unige.it/conferences/ct2000/ Accomodation in Como may be booked through the Centro di Cultura Scientifica "A. Volta", Villa Olmo, at the web page http://www.disi.unige.it/conferences/ct2000/accomodation_form.html The deadline for such a booking is 12th June 2000. Organizing Committee A. Carboni (Insubria) G. Rosolini (Genova) R.F.C. Walters (Insubria) 20th April 2000 From rrosebru@mta.ca Fri Apr 21 09:24:32 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA06755 for categories-list; Fri, 21 Apr 2000 09:23:29 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Microsoft Outlook Express for Macintosh - 4.01 (295) Date: Fri, 21 Apr 2000 07:51:40 +0200 Subject: categories: process algebras From: "Anna Labella" To: categories@mta.ca Mime-version: 1.0 X-Priority: 3 Content-type: text/plain; charset="US-ASCII" Content-transfer-encoding: 7bit Message-Id: <20000421055400.MRQY19811.fep03-svc.tin.it@[212.171.210.220]> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ---------- >Da: matthieu amiguet >A: categories@mta.ca >Oggetto: categories: process algebras >Data: Gio, 20 apr 2000 14:49 > >Dear categoricians, > >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? >Thank you for your help, > >Matthieu Amiguet > We have a categorical formalization of process algebras in terms of enriched category theory. You can see for a general presentation: S.Kasangian, A.Labella "Observational trees as models for concurrency" Math. Struct. in Comp.Science (1999) vol.9 pp.687-718 Anna Labella From rrosebru@mta.ca Fri Apr 21 17:04:09 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA28904 for categories-list; Fri, 21 Apr 2000 16:58:21 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200004211652.KAA29229@mailhost> Date: Fri, 21 Apr 2000 10:52:41 -0600 (MDT) From: Robin Cockett Reply-To: robin@cpsc.ucalgary.ca Subject: categories: re: process algebras To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; CHARSET=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Another few papers which may be of interest are: "Constructing process categories" J.R,B. Cockett (me!) & D.A. Spooner TCS 177 (1997) 73-109 "Categories for syncrony and asynchrony" J.R,B. Cockett & D.A. Spooner Electronic Notes in Theoretical Computer Science I (1995) 495-520 These papers explore the "combinatorial" representation of processes using span categories. In particular they give an account of Abramsky's program to model processes (based on a CCS style presentation) using span categories. -robin From rrosebru@mta.ca Fri Apr 21 17:04:12 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA28672 for categories-list; Fri, 21 Apr 2000 16:59:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: dusko@dusko.org Date: 21 Apr 2000 12:19:50 -0700 Message-ID: <20000421191950.25329.cpmta@c017.sfo.cp.net> X-Sent: 21 Apr 2000 19:19:50 GMT Content-Type: text/plain Content-Disposition: inline Mime-Version: 1.0 To: categories@mta.ca X-Mailer: Web Mail 3.6.0.2 Subject: categories: Re: process algebras 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? around 1995, i had two papers about "convenient categories for process calculus" and one about "categorical logic of concurrency and interaction". the simplest way to get them is probably on hypatia, or from my web page http://www.kestrel.edu/HTML/people/pavlovic/ i am not sure to which extent is this what you are looking for, but it is surely related. later samson abramsky and i figured how to deal with process categories much better, but most of it was never written up. an initial account was in our CTCS 97 paper (also available, i think, at the same sites.) -- dusko pavlovic From rrosebru@mta.ca Wed Apr 26 08:35:47 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA11591 for categories-list; Wed, 26 Apr 2000 08:31:12 -0300 (ADT) From: John Baez X-Authentication-Warning: math.ucr.edu: smap set sender to using -f Message-Id: <200004260920.CAA26766@math-cl-n04.ucr.edu> Subject: categories: From finite sets to Feynman diagrams To: categories@mta.ca (categories) Date: Wed, 26 Apr 2000 02:20:46 -0700 (PDT) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Here's a paper that might be of interest to some category theorists, although it's actually aimed at a general audience, and secretly tries to get them interested in categories. Later we'll write a more technical paper about Feynman diagrams and `stuff operators'. >From Finite Sets to Feynman Diagrams John C. Baez and James Dolan To appear in "Mathematics Unlimited - 2001 and Beyond", eds. Bjorn Engquist and Wilfried Schmid, Springer Verlag. Abstract: `Categorification' is the process of replacing equations by isomorphisms. We describe some of the ways a thoroughgoing emphasis on categorification can simplify and unify mathematics. We begin with elementary arithmetic, where the category of finite sets serves as a categorified version of the set of natural numbers, with disjoint union and Cartesian product playing the role of addition and multiplication. We sketch how categorifying the integers leads naturally to the infinite loop space Omega^infinity S^infinity, and how categorifying the positive rationals leads naturally to a notion of the `homotopy cardinality' of a tame space. Then we show how categorifying formal power series leads to Joyal's `especes des structures', or `structure types'. We also describe a useful generalization of structure types called `stuff types'. There is an inner product of stuff types that makes the category of stuff types into a categorified version of the Hilbert space of the quantized harmonic oscillator. We conclude by sketching how this idea gives a nice explanation of the combinatorics of Feynman diagrams. Available at: http://arXiv.org/abs/math.QA/0004133 From rrosebru@mta.ca Fri Apr 28 14:06:01 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA32635 for categories-list; Fri, 28 Apr 2000 13:58:09 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3906F97A.DA4312BD@daimi.au.dk> Date: Wed, 26 Apr 2000 16:14:11 +0200 From: karen =?iso-8859-1?Q?Kj=E6r=20M=F8ller?= X-Mailer: Mozilla 4.7 (Macintosh; I; PPC) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Associate Professorship in Logic in Computer Science, Aarhus, DK Content-Type: text/plain; charset=us-ascii; x-mac-type="54455854"; x-mac-creator="4D4F5353" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: UNIVERSITY OF AARHUS DEPARTMENT OF COMPUTER SCIENCE A tenured position as associate professor in the area of Logic in Computer Science, i.e. computational logic in a broad sense, is available at the Department of Computer Science, starting August 1, 2000. Ideally we seek applicants who as well as exhibiting a broad and impressive knowledge of Logic applicable in Computer Science, are able to support and encourage Logic on a broad front within the department. As a minimum requirement, applicants must have documented scientific qualifications within the area (equivalent to a PhD plus at least 2-3 years additional research and teaching). The Department conducts research and teaching in theoretical as well as experimental computer science. The staff is close to 200 people, including 25 full or associate professors, and 50 PhD students. The number of M.Sc. students is approximately 500. The position is intended to strengthen the Department's existing research group in Theoretical Computer Science, and will be associated with Research Centre BRICS (http:www.brics.dk/). Applicants must submit a curriculum vitae, a description of scientific accomplishments, future research plans and participation in research programmes, a description of teaching experience, a list of publications (all in 4 copies), and 3 copies of publications to be considered in the evaluation. The Faculty refers to the Ministerial Order No. 650 of 31.8.1998 on the appointment of teaching and research staff at the universities under the Ministry of Research and Information Technology. Applications should be addressed to The Faculty of Science, University of Aarhus, Ny Munkegade, Building 520, DK-8000 Aarhus C, Denmark, and marked 212/5-189 The deadline for receipt of all applications is May 10, 2000, at 12,00. For more information, please contact the head of the department Kurt Jensen (e-mail: kjensen@daimi.au.dk. Phone: +45 8942 5612) or consult the Web pages: http://www.daimi.au.dk/ From rrosebru@mta.ca Sun Apr 30 09:34:58 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA25360 for categories-list; Sun, 30 Apr 2000 09:29:36 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sat, 29 Apr 2000 20:50:35 -0500 (CDT) From: "Todd H. Trimble" Message-Id: <200004300150.UAA00297@fermat.math.luc.edu> Subject: categories: devissage To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: In section 5 of his Esquisse d'un Programme, in connection with tame topology, Grothendieck says he was able to convince himself that a formalism of devissage had some meaning in the context of topoi, via a suitable notion of "canonical tubular neighborhood of a subtopos" in an ambient topos. Has anyone besides Grothendieck pursued this idea? Thanks, Todd