From MAILER-DAEMON Wed Mar 12 19:50:15 2008 Date: 12 Mar 2008 19:50:15 -0300 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1205362215@mta.ca> X-IMAP: 1201902028 0000000057 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Fri Feb 1 17:17:25 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 01 Feb 2008 17:17:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JL35I-0002nU-EG for categories-list@mta.ca; Fri, 01 Feb 2008 17:06:04 -0400 From: Gaucher Philippe Subject: categories: cogenerator of k-spaces Date: Fri, 1 Feb 2008 14:27:23 +0100 MIME-Version: 1.0 Content-Disposition: inline To: categories@mta.ca Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 1 Dear All, Does the category of k-spaces (i.e. colimits of compact Hausdorff spaces) have a cogenerator ? Note that these spaces are not necessarily normal because they are not necessarily Hausdorff. Otherwise [0,1] would have work without any additional argument. Thanks in advance. pg. From rrosebru@mta.ca Fri Feb 1 17:17:25 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 01 Feb 2008 17:17:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JL36P-00030I-Kl for categories-list@mta.ca; Fri, 01 Feb 2008 17:07:13 -0400 From: "Noson" To: Subject: categories: Alex Heller Date: Fri, 1 Feb 2008 15:28:16 -0500 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 2 It is with great sadness that I inform you of the passing of Alex Heller. He passed away yesterday after a short illness. Details to follow. From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLIlr-00042H-ES for categories-list@mta.ca; Sat, 02 Feb 2008 09:51:03 -0400 From: Dana Scott To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Subject: categories: Re: Alex Heller Date: Fri, 1 Feb 2008 13:39:20 -0800 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 4 On Feb 1, 2008, at 12:28 PM, Noson wrote: > It is with great sadness that I inform you of the passing of > Alex Heller. He passed away yesterday after a short illness. > Details to follow. Sad, sad, sad news indeed. I have to relay a story Alex told me not so many years ago when we sat next to each other at a conference dinner. I asked him about the last illness of Eilenberg, which was long and difficult. Alex visited him often, and after a stroke Sammy could not talk. On the last time he saw him, as Alex was getting up to leave, he saw Sammy wanted something. Then he realized he wanted a farewell hug. Anyone who remembers Sammy will recall he was one of the world's prime skeptics and not much into hugging. Alex gave him the hug, and just imagining the scene brings tears to my eyes. Dana & Irene Scott 1149 Shattuck Avenue Berkeley, CA 94707-2609 ------ Tel: (510) 527-5287 From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLInI-00047K-K9 for categories-list@mta.ca; Sat, 02 Feb 2008 09:52:32 -0400 Date: Fri, 1 Feb 2008 19:42:47 -0500 (EST) From: Michael Barr To: Categories list Subject: categories: Alex Heller MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 5 The younger category theorists will have had little knowledge of the great contributions Alex made in the early days. Not research in category theory per se, but an early promoter, supporter, and consumer of category theory in algebraic topology. See his paper in the La Jolla volume. I believe that he was also one of the organizers of that meeting. When I arrived in Urbana in the fall of 1964, there was an active seminar in category theory. Alex, Jon Beck, Max Kelly, John Gray and I were the main participants along with graduate students. Mac Lane's invitation to the five of us to spend a weekend in Chicago constituted the first mid-west category meeting. Then came the La Jolla meeting. Unfortunately, at the end of that year, Alex went off to CUNY, Jon to Cornell, Max back to Sydney and John and I were left alone. Alex was really the third established mathematician (after Eilenberg and Mac Lane, of course) to embrace category theory in that way. We mourn his passing. From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLIo7-00049X-6y for categories-list@mta.ca; Sat, 02 Feb 2008 09:53:23 -0400 Date: Fri, 1 Feb 2008 20:37:23 -0600 (CST) From: Gabor Lukacs To: categories@mta.ca Subject: categories: Re: cogenerator of k-spaces MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 6 Dear Philippe, You wrote "colimits of compact Hausdorff spaces." In what category? There is both a Hausdorff and a non-Hausdorff notion for k-spaces. The earlier is certainly easier to define. You may wish to look at Chapter 1 of my thesis: http://at.yorku.ca/p/a/a/o/41.htm I discuss there both notions, and provide some reference to the literature, so it might be a good starting point. Spaces where points can be distinguished by continuous real-valued functions are often referred to as "functionally Hausdorff." T. Ishii gives an example of a regular k-space that is not functionally Hausdorff in his paper "On the Tychonoff functor and $w$-compactness" that appeared in Topology Appl., 11(2):173--187, 1980. (See Lemma 3.1.) (I can send you the paper if you are interested.) This, of course, means that even for Hausdorff k-spaces you cannot use [0,1] as a cogenerator. Now, as I am writing this, I wonder what you mean by 'cogenerator': An object such that morphisms into that object can distinguish between morphisms in the category (i.e., generalized points), or something that every space in your category admits an __embedding__ to some power of this object? The notion of "embedding" already requires some kind of factorization system, though. For the earlier, however, {0,1} equipped with the anti-discrete topology (i.e., only the set itself and the emptyset are open) does what you want. It is certainly a k-space (albeit non-Hausdorff). Best wishes, Gabi On Fri, 1 Feb 2008, Gaucher Philippe wrote: > Dear All, > > Does the category of k-spaces (i.e. colimits of compact Hausdorff spaces) have > a cogenerator ? Note that these spaces are not necessarily normal because > they are not necessarily Hausdorff. Otherwise [0,1] would have work without > any additional argument. > > Thanks in advance. pg. > From rrosebru@mta.ca Sat Feb 2 14:09:26 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 02 Feb 2008 14:09:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLMhu-0000zk-GD for categories-list@mta.ca; Sat, 02 Feb 2008 14:03:14 -0400 Date: Sat, 02 Feb 2008 16:52:09 +0000 From: Eike Ritter MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Midlands Graduate School in the Foundations of Computing Science 14-18 April 2008 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 7 Call for Participation Midlands Graduate School in Computer Science 14-18 April 2008 School of Computer Science, University of Birmingham The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the Mathematical Foundations of Computing. It has run annually since 1999, and is hosted by the Universites of Birmingham, Leicester, and Nottingham in rotation. The lectures are aimed at PhD students, typically in their first or second year of study. However, the school is open to anyone who is interested in learning more about the mathematical foundations of computing, and all such participants are warmly welcomed. We also very much welcome students from abroad. We gratefully acknowledge financial support by ESPRC. The following courses will be offered: Basic Courses: Category Theory (Neil Ghani, University of Nottingham) Operational Semantics (Roy Crole, University of Leicester) Typed Lambda Calculus (Paul Levy, University of Birmingham) Advanced Courses: The Mathematical Structure of Information Flow, in Physics, Geometry, Logic and Computation. (Samson Abramsky, University of Oxford) Coq (Thorsten Altenkirch, University of Nottingham) Denotational Semantics (Martin Escardo, University of Birmingham) Games for Software Verification (Dan Ghica, University of Birmingham) Proof Theory (Peter Hancock, University of Nottingham) Algebraic Methods (Georg Struth, University of Sheffield) LOCATION The school will be held in the School of Computer Science, University of Birmingham. Birmingham is centrally located in the UK, and is easily reachable by road, rail and air (Birmingham International Airport). REGISTRATION The deadline for registration is 8 March 2008, and the registration fee is 350 UK pounds, including accomodation. We also have a number of free places for UK-based PhD students. The deadline for applying for these free places is 15 February 2008. The number of places is limited, so early registration is advised. FURTHER DETAILS Google search - MGS 2008 Web page - http://events.cs.bham.ac.uk/mgs2008 -- ------------------------------------ Dr Eike Ritter Tel.: (+44) 121 41 44772 School of Computer Science Sec.: (+44) 121 41 43711 The University of Birmingham Fax.: (+44) 121 41 44281 Edgbaston Email: E.Ritter@cs.bham.ac.uk BIRMINGHAM, B15 2TT Web: http://www.cs.bham.ac.uk England ------------------------------------ From rrosebru@mta.ca Sun Feb 3 10:02:26 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 03 Feb 2008 10:02:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLfHT-0006L8-T4 for categories-list@mta.ca; Sun, 03 Feb 2008 09:53:11 -0400 From: "Noson" To: Subject: categories: Alex Heller Date: Sat, 2 Feb 2008 21:15:39 -0500 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 8 Alex Heller, who was 82, died Jan. 31st, at St. Vincent's Hospital, where he was taken after collapsing in his home the previous day.=A0=20 His wife, Grace, said it was a torn aorta. They did emergency surgery on him, though he succumbed about eighteen hours later. Condolences can be sent to: Mrs. Grace Heller 29 West 10th Street New York, NY 10011 He will truly be missed. Noson=20 From rrosebru@mta.ca Sun Feb 3 10:02:26 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 03 Feb 2008 10:02:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLfGH-0006HY-0n for categories-list@mta.ca; Sun, 03 Feb 2008 09:51:57 -0400 From: John Duskin To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Subject: categories: Alex Date: Sat, 2 Feb 2008 13:17:47 -0500 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 9 There is a marvelous picture of Saunders and Alex chairing the Coimbra CT99 conference. Everyone who knows them should see it. From rrosebru@mta.ca Sun Feb 3 16:28:20 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 03 Feb 2008 16:28:20 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLlO6-0006O0-Nh for categories-list@mta.ca; Sun, 03 Feb 2008 16:24:26 -0400 From: John Duskin To: categories@mta.ca Subject: categories: Re: Alex Date: Sun, 03 Feb 2008 13:17:51 -0500 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 10 Curiously, Fred's marvelous pictures do not include the one I have of Saund= ers and Alex (taken by the conference photographer). I don't know how to pu= t it on the web. From rrosebru@mta.ca Sun Feb 3 16:28:20 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 03 Feb 2008 16:28:20 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JLlMl-0006HG-Qj for categories-list@mta.ca; Sun, 03 Feb 2008 16:23:03 -0400 Date: Sun, 03 Feb 2008 11:16:07 -0500 From: "Fred E.J. Linton" To: Subject: categories: Re: Alex Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 11 [Note from moderator: Jack may refer to a nice picture linked from: http://www.mat.uc.pt/~ct99/ ] Jack Duskin wrote, recently, without being terribly specific, > There is a marvelous picture of Saunders and Alex chairing the Coimbra > CT99 conference. Everyone who knows them should see it. A few neat, if low-res, pictures of Alex (and Saunders) at Coimbra = may be found as the jpegs http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/Sym-03.jpg http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/Sym-25.jpg or on the book pages http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/S-06.htm http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/S-19.htm and those before and after. While these may well NOT be the images = Jack meant, they may do until he provides more specific references. Of course, I, like all who had the privilege of coming to know Alex and Grace, mourn the passing of this cosmopolitan gentleman, quiet scholar, and supportive enthusiast for category theory. Would that I might know how to support Grace in these terrible hours: my heart goes out to her, as also to his children, both biological and mathematical. -- Fred From rrosebru@mta.ca Mon Feb 4 11:16:55 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 04 Feb 2008 11:16:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JM2sb-0003qp-Lg for categories-list@mta.ca; Mon, 04 Feb 2008 11:05:05 -0400 From: John Duskin To: categories@mta.ca Mime-Version: 1.0 (Apple Message framework v915) Subject: categories: Saunders and Alex'spicture Date: Mon, 4 Feb 2008 01:00:14 -0500 Content-Type: text/plain;charset=US-ASCII;format=flowed;delsp=yes Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 12 Thanks to the moderator and Fred, the picture of the pair of them that I was referring to is on the collection of pics from the Coimbra CT99 conference: ...Note from moderator: Jack may refer to a nice picture linked from: http://www.mat.uc.pt/~ct99/ ]... Its the one with them smiling, sitting behind the conference poster. From rrosebru@mta.ca Mon Feb 4 11:16:55 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 04 Feb 2008 11:16:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JM2tN-0003xt-IT for categories-list@mta.ca; Mon, 04 Feb 2008 11:05:53 -0400 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Content-Transfer-Encoding: quoted-printable From: Dan Ghica Subject: categories: GaLoP 2008 : Submission Deadline Extended Date: Mon, 4 Feb 2008 10:31:15 +0000 To: types-announce@lists.seas.upenn.edu, categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 13 Dear all, The submission deadline for the Games for Logic and Programming =20 Languages III workshop (ETAPS 2008, March 29 - April 6, 2008, =20 Budapest, Hungary) has been extended to February 14. The call for =20 submissions is attached below. GAMES FOR LOGIC AND PROGRAMMING LANGUAGES III ETAPS 2008, March 29 - April 6, 2008, Budapest, Hungary =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D *The submission deadline has been extended to February 14.* The submission site is open: http://www.easychair.org/conferences/?conf=3Dgalop08 Introduction GaLoP is an annual international workshop on game-semantic models for =20= logics and programming languages and their applications. This is an =20 informal workshop that welcomes work in progress, overviews of more =20 extensive work, programmatic or position papers and tutorials as well =20= as contributed papers and invited talks. Contributions are invited on all pertinent subjects, with particular =20 interest in compositional game-semantic models. Typical but not =20 exclusive areas of interest are: * categorical aspects; * algorithmic aspects; * programming languages and full abstraction; * semantics of logics and proof systems; * proof search; * higher-order automata; * program verification and model checking; * program analysis; * security; * theories of concurrency; * probabilistic models. Publication This is intended to be an informal workshop without widely =20 distributed proceedings. We therefore ask for submission both of =20 short abstracts outlining what will be presented at the workshop and =20 of longer papers describing completed work, either published or =20 unpublished, in the relevant areas. A special issue of the journal Annals of Pure and Applied Logic =20 associated with the workshop will be discussed at the workshop. Important dates # Submission: February 14 # Notification: March 1 # Workshop: April 5-6 Invited speakers # Gabriel Sandu, Helsinki # Paul-Andr=E9 Melli=E8s, PPS Program committee # Dan Ghica (co-chair), Birmingham # Russ Harmer (co-chair), PPS # Martin Hyland, Cambridge # Pierre Hyvernat, Savoie # Jim Laird, Bath # John Longley, Edinburgh # Andrzej Murawski, Oxford # Andrea Schalk, Manchester --- Dr. Dan Ghica, Lecturer School of Computer Science University of Birmingham Birmingham B15 2TT tel: +44 121 414 8819 mailto:D.R.Ghica@cs.bham.ac.uk http://www.cs.bham.ac.uk/~drg From rrosebru@mta.ca Mon Feb 4 14:47:34 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 04 Feb 2008 14:47:34 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JM6HU-0001LG-UU for categories-list@mta.ca; Mon, 04 Feb 2008 14:43:00 -0400 From: Thomas Streicher Subject: categories: Colloquium Logicum 2008, September 10-12 To: categories@mta.ca Date: Mon, 4 Feb 2008 17:02:33 +0100 (CET) MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 14 --------------------------------------------------------------- Colloquium Logicum 2008, September 10-12, TU Darmstadt, Germany --------------------------------------------------------------- The biennial meeting of the German Society for Mathematical Logic (DVMLG), Colloquium Logicum 2008, will be held at the Technische Universitaet Darmstadt, September 10-12, 2008. The scientific programme comprises * Herbrand Centenary Lecture: Georg Kreisel, F.R.S., Salzburg * invited plenary lectures by * Hans Adler (Leeds) * Sergei Goncharov (Novosibirsk) * Joel David Hamkins (New York) * Robert Lubarsky (Florida) * Nicole Schweikardt (Frankfurt) * Michiel van Lambalgen (Amsterdam) plus a PhD Colloquium with the presentation of selected recent PhD Theses in Logic as well as contributed talks. Further details about the meeting, registration, etc. will be published on the meeting's homepage in the near future: www.mathematik.tu-darmstadt.de/fbereiche/logik/events/collogicum/. ------- From rrosebru@mta.ca Tue Feb 5 14:34:19 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 05 Feb 2008 14:34:19 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JMSQI-0001kt-HN for categories-list@mta.ca; Tue, 05 Feb 2008 14:21:34 -0400 Date: Tue, 5 Feb 2008 19:11:21 +0200 From: Doron Peled To: Subject: categories: CFP: 5th Workshop on Model Checking and AI Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 15 - Call for Papers - Fifth Workshop on MODEL CHECKING and ARTIFICIAL INTELLIGENCE (MoChArt-2008) At ECAI-2008 - Patras, Greece, July 2008 http://www.csc.liv.ac.uk/~mjw/mochart/ INTRODUCTION Model checking is the process of determining whether or not a formula of some logic is satisfied by a model for the logic. For many logics of interest -- particularly temporal and modal logics -- model checking procedures can be efficiently automated. This has led to widespread interest in the use of model checking as a technique for verifying properties of systems, and the development of a number of widely used model checking tools (e.g., Carnegie-Mellon's SMV, Cadence-SMV, and AT&T's SPIN). The success of model checking in the computer aided verification community has led to a growth of interest in the use of model checking in AI. The MOCHART workshop brings together both researchers in AI with an interest in model checking, and researchers in model checking who are interested in AI techniques. Previous editions of the workshop were held in Riva del Garda, Italy in 2006 (as satellite workshops of ECAI), San Francisco in 2005 (as satellite workshop of Concur), Acapulco in 2003 (as satellite workshop of IJCAI03), and Lyon in 2002 (as satellite workshop of ECAI02). We are exploring the possibility of publishing a formal proceedings after the event with Springer-Verlag. TOPICS OF INTEREST Topics of interest include (but are not limited to): - Application of model checking techniques to AI problems. - planning as model checking - model checking for multi-agent systems - diagnosis and model checking - model checking versus theorem proving - Model Checking and AI logics. - model checking for combined modal/temporal logics - model checking for logics of common sense reasoning - Relations between different techniques used in the two fields for similar purposes (e.g., reducing state explosion). - New model checking techniques specifically for AI problems. - Exploitation of AI techniques in model checking. - AI approaches to the state explosion problem - heuristics for model checking - AI approaches to automatic abstraction - Software tools for model checking in AI. - languages and software platforms for AI model checking - model checking symbolic reasoning systems & languages - Model checking for verification of AI systems. - automated verification of AI systems - case studies & experience with model checking in AI Preliminary papers and papers on applications are strongly encouraged. IMPORTANT DATES Deadline for submissions: April 10th, 2008 Notification: May 10th, 2008 Workshop: July 21st-22nd, 2008 SUBMISSION PROCEDURES Submissions must be formatted according to Springer-Verlag's "Lecture Notes in Computer Science" styles, and must be no more than 15 pages in length. Papers must be submitted through the EasyChair web-based conference management system: follow the link from the workshop web page. All papers will be peer reviewed, and evaluated on the basis of relevance, technical quality, significance, evaluation, and presentation. PARTICIPATION The workshop forms part of the ECAI-2008 workshop programme, and as such delegates must register for the ECAI conference. For full information about ECAI-2008, including travel & accomodation, see: ORGANISING COMMITTEE * Doron Peled Department of Computer Science Bar-Ilan University Ramat Gan, 52900 Israel mailto:doron.peled@gmail.com * Michael Wooldridge Department of Computer Science University of Liverpool Liverpool L69 7ZF, United Kingdom mailto:mjw@liv.ac.uk PROGRAM COMMITTEE * Rajeev Alur (USA) * Massimo Benerecetti (Italy) * Rafael Bordini (UK) * Kousha Etessami (UK) * Michael Fisher (UK) * Gerard Holzmann (USA) * Hadas Kress-Gazit (USA) * Orna Kupferman (Israel) * Alessio Lomuscio (UK) * Ron van de Meyden (Australia) * Peter Niebert (France) * Charles Pecheur (USA) * Wojciech Penczek (Poland) * Franco Raimondi (UK) * Mark Ryan (UK) * Farn Wang (China) From rrosebru@mta.ca Wed Feb 6 15:15:21 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 06 Feb 2008 15:15:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JMpVq-0002kj-Cc for categories-list@mta.ca; Wed, 06 Feb 2008 15:00:50 -0400 Date: Wed, 06 Feb 2008 13:31:38 -0500 From: Jacques Carette MIME-Version: 1.0 To: categories Subject: categories: Looking for some categorical PhD theses Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 16 In particular I cannot seem to find these: D.S. Rajan, "Differentiation and Integration of the Combinatorial Species of Joyal", PhD Thesis, Dept. of Mathematics, SUNY at Buffalo. Yeong-Nan Yeh, "On the Combinatorial Species of Joyal", PhD Thesis, Dept. of Mathematics, SUNY at Buffalo. Electronic versions would be extremely welcome. If only paper versions exist (but you have a copy!), contact me by email and we can work out an appropriate method of duplication+transmission. Jacques From rrosebru@mta.ca Wed Feb 6 15:15:22 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 06 Feb 2008 15:15:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JMpVB-0002f6-8W for categories-list@mta.ca; Wed, 06 Feb 2008 15:00:09 -0400 To: categories@mta.ca Subject: categories: second call for papers From: Myriam Quatrini Date: Wed, 6 Feb 2008 10:59:14 +0100 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain;charset=ISO-8859-1;format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 17 SECOND CALL FOR PAPERS Workshop on Symmetric calculi and Ludics for the semantic=20 interpretation (http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html) August 4-8, 2008 organized as part of the European Summer School on Logic, Language and Information ESSLLI 2008 (http://www.illc.uva.nl/ESSLLI2008/), 4-15 August, 2008 in Hamburg, Germany Workshop Organizers: Alain Lecomte (SFL - Paris 8), Alain.Lecomte@upmf-grenoble.fr Myriam Quatrini (IML Marseille), quatrini@iml.univ-mrs.fr Workshop Purpose and topics: In recent years there have been some important new developments of=20 methods of dealing with semantic and pragmatic phenomena in=20 Linguistics, inspired by developments in Logic and Theoretical Computer=20= Science. Among these developments, Continuation Theory, Symmetric=20 calculi and Ludics play an important role. Continuation theory dates=20 back from the early seventies (cf. Reynolds, 93) and was at the heart=20 of Programming Languages like Scheme. More recently, a logical account=20= was given to it, by extending the Curry-Howard homomorphism (Griffin,=20 1990),. This led to several calculi like such as Parigot's=20 lambda-mu-calculus, Curien-Herbelin's lambda-mu-mu-tilde-calculus,=20 Wadler's dual calculus and so on. These calculi are based on the core=20 idea that programs and contexts are dual entities and this is reflected=20= in the symmetry of the "classical" sequents. These systems were=20 prefigured by the so called Lambek-Grishin calculus (Grishin, 83), a=20 calculus extending the Lambek calculus by taking classical sequents=20 into account. Following Curien-Herbelin (Bernardi and Moortgat, 2007)=20 focuses on the connection between Lambek-Grishin calculus with=20 lambda-mu-tilde-calculus and hence with continuation semantics. Classical linear logic (Girard, 87, 95) gives another viewpoint, where=20= the co-product is realized by an authentic parallelisation connective.=20= Linguistic applications have been given since around 2000, particularly=20= by C. Barker (Barker, 2002), K. Chung-chieh Shan (Chung-chieh Shan,=20 2002) and P. de Groote (de Groote, 2001) who exploited the advantages=20 of these systems in the task of giving several readings of an ambiguous=20= sentence. De Groote (de Groote, 2007) also shows that we gain a new=20 dynamical logic which enables us to elegantly treat phenomena of=20 discourse like anaphora resolution. M. Moortgat and R. Bernardi=20 (Moortgat & Bernardi, 2007) shows how moving to a symmetric categorial=20= grammar, namely Lambek Grishin calculus, helps accounting for=20 discontinous phenomena that are not captured by the asymmetric Lambek=20 calculus. Independently, linear logic was intensively studied in=20 particular by Girard himself who invented "Ludics" as a new conception=20= of logic, where the dualism between syntax and semantics is abolished :=20= the meaning of rules is in the rules themselves. This conception has=20 some similarities with more traditional "Game Semantics" (Lorenz,=20 Lorenzen, Hintikka...) but it is dynamic, in the sense that=20 "strategies" are replaced by interacting processes. Moreover, a new=20 step in abstraction is provided, which consists in stating rule=20 schemata which are only expressed in terms of loci (that we may see as=20= memory cells). The two approaches in this workshop are connected, basically because=20= of their common root : explorations in the meaning of Logics and in=20 particular reflections on one of the symmetrical systems, namely linear=20= logic. Linguistic applications of Ludics remain very embryonic, but=20 some authors have already emphasized that it is suitable for giving a=20 framework in which it is possible to study speech acts and dialogue=20 (Livet, 2007, Troncon, 2006). Other authors have pointed out=20 similarities of the Ludics' philosophy with Wittgenstein's views on=20 language games (Pietarinen, 2006). This workshop will provide an=20 opportunity to study these questions. It will accept several kinds of=20 contributions : theoretical works on continuation theory, symmetric=20 calculi and ludics, applied works of these theory concerning linguistic=20= topics (semantics, pragmatics) and philosophical investigations. Submission Details: Authors are invited to submit an anonymous, extended abstract.=20 Submissions should not exceed 7 pages, including references.=20 Submissions should be in PDF format. Please send your submission=20 electronically using the interface EasyChair. The submissions will be=20 reviewed by the workshop's programme committee. Workshop format: The workshop is part of ESSLLI and is open to all ESSLLI participants.=20= It will consist of five 90-minute sessions held over five consecutive=20 days in the first week of ESSLLI. There will be 2 slots for paper=20 presentation and discussion per session. On the first day the workshop=20= organisers will give an introduction to the topic. Invited Speakers: Philippe de Groote, LORIA, France. Additional invited speaker to be confirmed Workshop Programme Committee: Raffaella Bernardi (Bolzano) Claire Beyssade (Institut Jean Nicod, Paris) Marie-Ren=E9e Fleury (IML - Marseille) Philippe de Groote (LORIA - Nancy) Hugo Herbelin (Paris) Jean-Baptiste Joinet (Paris 1) Greg Kobele (Humboldt Universitat zu Berlin) Alain Lecomte (SFL - Paris 8) Pierre Livet (Aix en Provence) Richard Moot (LABRI - Bordeaux) Sylvain Pogodalla (LORIA - Nancy) Carl Pollard (Ohio University) Myriam Quatrini (IML Marseille) Christian Retor=E9 (LABRI - Bordeaux) Laurent Roussarie (SFL - Paris 8) Sylvain Salvati (LABRI - Bordeaux) Important Dates: Submission Deadline: March 8, 2008 Notification: April 21, 2008 Preliminary Program: April 24, 2008 ESSLLI Early Registration: May 1, 2008 Final Papers for Proceedings: May 17, 2008 Final Program: June 21, 2008 Workshop Dates: August 11-15, 2008 Local Arrangements: All workshop participants including the presenters will be required to register for ESSLLI. The registration fee for authors presenting a paper will correspond to the early student/workshop speaker registration fee. There will be no reimbursement for travel costs and accommodation. Further Information: About the workshop: http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html About ESSLLI: http://www.illc.uva.nl/ESSLLI2008/ From rrosebru@mta.ca Thu Feb 7 17:22:21 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 07 Feb 2008 17:22:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNDzY-0003pl-Hj for categories-list@mta.ca; Thu, 07 Feb 2008 17:09:08 -0400 Date: Thu, 7 Feb 2008 20:05:47 +0000 (GMT) From: Paul B Levy To: categories@mta.ca Subject: categories: question about monoidal categories MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 18 Let F be a functor from a monoidal category M to a category S. We are given beta(p,a) : F(p) --> F(p*a) natural in p,a in M. If I tell you that, in addition to naturality, beta is "monoidal", I'm sure you will immediately guess what I mean by this, viz. (a) for any p,a,b in M beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b)) (b) for any p in M beta(p,1) = F(rho(p)) Yet I cannot see any reason for giving the name "monoidality" to (a)-(b). It doesn't appear to be a monoidal natural transformation in the official sense. There are no monoidal functors in sight. Can somebody please justify my usage? Paul From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNYPB-0004d5-BI for categories-list@mta.ca; Fri, 08 Feb 2008 14:56:57 -0400 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit From: Sam Staton Subject: categories: Re: question about monoidal categories Date: Fri, 8 Feb 2008 09:51:09 +0000 To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 19 Hello, here is an answer to Paul's question: The data (F,beta) defines a (lax?) functor between "monoidal categories with right units but not left units" [henceforth MR-categories]. Every pointed category can be considered as an MR-category, in fact a strict one. The tensor product is left projection. The right unit is the point of the category (although every object of the category behaves like a right unit for this category.) In particular, the category S in Paul's email, with point F(1), can be seen as an MR-category. Of course, every monoidal category, including M, is an MR-category too. The data for a lax MR-functor M->S consists of a functor F:M->S, a morphism F(i)->F(i), which we can take as identity, and a natural transformation F(p)*F(a) --> F(p*a) which in this case amounts to a map beta:F(p) --> F(p*a) A monoidal functor must satisfy three coherence conditions, for associativity, left identity and right identity. For an MR-functor, there are only axioms for associativity and right identity, and these are exactly the axioms that Paul gave. Hope that makes sense! All the best, Sam. On 7 Feb 2008, at 20:05, Paul B Levy wrote: > > > > Let F be a functor from a monoidal category M to a category S. > > We are given > > beta(p,a) : F(p) --> F(p*a) > > natural in p,a in M. > > If I tell you that, in addition to naturality, beta is "monoidal", I'm > sure you will immediately guess what I mean by this, viz. > > (a) for any p,a,b in M > > beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b)) > > (b) for any p in M > > beta(p,1) = F(rho(p)) > > Yet I cannot see any reason for giving the name "monoidality" to > (a)-(b). > > It doesn't appear to be a monoidal natural transformation in the > official > sense. There are no monoidal functors in sight. > > Can somebody please justify my usage? > > Paul > > From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNYOU-0004YU-Ji for categories-list@mta.ca; Fri, 08 Feb 2008 14:56:14 -0400 Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: categories@mta.ca Content-Transfer-Encoding: 7bit From: Marco Grandis Subject: categories: Re: question about monoidal categories Date: Fri, 8 Feb 2008 09:31:58 +0100 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 20 Dear Paul, Let us forget about the monoidal unit and fix (a). You define a strict semi? monoidal structure on S letting x*y = x. Then your pair (F, beta) is a lax monoidal functor M --> S. Your condition (a) is the hexagon of consistency with alpha, which here reduces to: F(p) = F(p) || | F(p) F(p*a) | | F(p*(a*b) --> F((p*a)*b) (a single | stands for a downward beta) Now, to fix also (b), I guess you should add to S a new object which is a strict identity for the tensor and work out things. However, if your problem is only about terminology and you do not want to use the tensor on S in the sequel (eg to compose F with other monoidal functors), you might not bother about that. Best regards Marco From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNYNc-0004QF-Vg for categories-list@mta.ca; Fri, 08 Feb 2008 14:55:21 -0400 Date: Thu, 7 Feb 2008 18:58:47 -0500 (EST) From: Jeff Egger Subject: categories: Re: question about monoidal categories To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 21 Hi Paul,=20 I think that I have written previously to the list about the=20 possibility of a monoidal functor acting on a mere functor,=20 and what you have is an instance of this notion. =20 Here the monoidal functor is the unique functor M ---> T, where T is the terminal (monoidal) category. Your beta is=20 a right action of this guy on F. In general, a right action of monoidal A --U--> C on mere=20 P --F--> S requires a right action of A on P and a right=20 action of C on S as well as a natural transformation=20 F(p)*U(a) --beta(p,a)--> F(p*a)=20 satisfying the appropriate associativity and unit axioms. In your case S is equipped with the trivial right T-action=20 (x*1=3Dx), and M with its canonical right M-action (a*b=3Da*b). =20 The axioms are identical. Cheers, Jeff. --- Paul B Levy wrote: >=20 >=20 >=20 > Let F be a functor from a monoidal category M to a category S. >=20 > We are given >=20 > beta(p,a) : F(p) --> F(p*a) >=20 > natural in p,a in M. >=20 > If I tell you that, in addition to naturality, beta is "monoidal", I'm > sure you will immediately guess what I mean by this, viz. >=20 > (a) for any p,a,b in M >=20 > beta(p,a) ; beta(p*a,b) =3D beta(p,a*b) ; F(alpha(p,a,b)) >=20 > (b) for any p in M >=20 > beta(p,1) =3D F(rho(p)) >=20 > Yet I cannot see any reason for giving the name "monoidality" to (a)-(b= ). >=20 > It doesn't appear to be a monoidal natural transformation in the offici= al > sense. There are no monoidal functors in sight. >=20 > Can somebody please justify my usage? >=20 > Paul >=20 >=20 >=20 Be smarter than spam. See how smart SpamGuard is at giving junk ema= il the boot with the All-new Yahoo! Mail. Click on Options in Mail and s= witch to New Mail today or register for free at http://mail.yahoo.ca=20 From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNYMo-0004Ix-RO for categories-list@mta.ca; Fri, 08 Feb 2008 14:54:30 -0400 Date: Thu, 7 Feb 2008 22:36:24 +0000 (GMT) From: Richard Garner To: categories@mta.ca Subject: categories: Re: question about monoidal categories MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 22 Dear Paul, Here is one possible answer to your question. One has a notion of action of a monoidal category V on an arbitrary category X, which generalises that of action by a monoid on a set; thus we have a functor (-) * (-): X x V --> X together with natural isomorphisms x * I ~ x and x * (v * w) ~ (x * v) * w satisfying pentagon and triangle axioms. Formally, one may define an action of V on X to be a strong monoidal functor V --> [X, X], where the latter is equipped with its compositional monoidal structure. If we are given two categories X and Y equipped with an action by V, then we have a notion of equivariant morphism between them; namely a functor F: X --> Y together with natural morphisms m_{x, v} : F(x) * v --> F(x * v) obeying axioms like those for a monoidal functor. This is what one might call a lax equivariant morphism; if the m_{x, v}'s are all invertible we should rather call it strong, whilst if they point in the opposite direction then what we have is an oplax morphism. The situation you have described is a special case of an lax equivariant morphism. You have a monoidal category M, and a functor F : M --> S. Now, M has a canonical action on itself induced by tensoring on the right (the "right regular representation"); and it has a trivial action on S given by s * m = s for all s and m. Your natural transformation beta can now be written as beta(p, a) : F(p) * a --> F(p * a), and your two axioms are precisely the axioms required for beta to equip F with the structure of a lax equivariant morphism. This whole area of monoidal actions is slightly folklorish but a useful source is: George Janelidze and Max Kelly, "A note on actions of a monoidal category", TAC Vol. 9, No. 4 Also worth mentioning is the work of Paddy McCrudden who has studied actions by a symmetric monoidal V under the name "V-actegories". Hope this is of some help, Richard --On 07 February 2008 20:05 Paul B Levy wrote: > > > > Let F be a functor from a monoidal category M to a category S. > > We are given > > beta(p,a) : F(p) --> F(p*a) > > natural in p,a in M. > > If I tell you that, in addition to naturality, beta is "monoidal", I'm > sure you will immediately guess what I mean by this, viz. > > (a) for any p,a,b in M > > beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b)) > > (b) for any p in M > > beta(p,1) = F(rho(p)) > > Yet I cannot see any reason for giving the name "monoidality" to (a)-(b). > > It doesn't appear to be a monoidal natural transformation in the official > sense. There are no monoidal functors in sight. > > Can somebody please justify my usage? > > Paul > > > From rrosebru@mta.ca Fri Feb 8 20:49:31 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Feb 2008 20:49:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JNdjV-0002M2-Ux for categories-list@mta.ca; Fri, 08 Feb 2008 20:38:18 -0400 Date: Fri, 8 Feb 2008 20:03:46 +0000 (GMT) From: Richard Garner To: categories@mta.ca Subject: categories: Re: question about monoidal categories MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 23 As an addendum to the interesting answers that have been given so far to Paul's question, it is perhaps worth pointing out that using an old result of Max Kelly's, the situation Paul describes can be expressed purely in terms of a strong monoidal functor. Given a monoidal category M and functor F : M --> S as in Paul's message, we define a strict monoidal category {F, F} as follows. Its objects are triples (G, H, a) fitting into a diagram of functors and natural transformations G M -----> M | | | a | F | => | F | | v v S -----> S H Its morphisms (G, H, a) --> (G', H', a') are pairs of natural transformations b : G => G', c : H => H' satisfying the obvious compatibility condition with a and a'. The tensor product is given by pasting squares next to each other horizontally. There are strict monoidal functors p_1 : {F, F} -> [M, M] and p_2 : {F, F} -> [S, S] sending (G, H, a) to G and H respectively; and as in my previous message we have strong monoidal functors R : M ---> [M, M] m |--> (-) * m T : M ---> [S, S] m |--> id_S corresponding to the right regular action of M on itself, and to the trivial action of M on S. Now to give the natural transformation beta of Paul's message, satisfying his "monoidality" conditions, is precisely to give a strong monoidal functor B: M --> {F, F} rendering the diagram _ {F, F} .| | . | B . | (p_1, p_2) . | . v M --------> [M, M] x [S, S] (R, T) commutative. I believe this technique originates in the paper "Coherence theorems for lax algebras and for distributive laws", G.M. Kelly, LNM 420. A good place to learn more about it is in Section 2 of "On property-like structures", G.M. Kelly and S. Lack, TAC Vol. 3, No. 9 Richard --On 07 February 2008 20:05 Paul B Levy wrote: > > > > Let F be a functor from a monoidal category M to a category S. > > We are given > > beta(p,a) : F(p) --> F(p*a) > > natural in p,a in M. > > If I tell you that, in addition to naturality, beta is "monoidal", I'm > sure you will immediately guess what I mean by this, viz. > > (a) for any p,a,b in M > > beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b)) > > (b) for any p in M > > beta(p,1) = F(rho(p)) > > Yet I cannot see any reason for giving the name "monoidality" to (a)-(b). > > It doesn't appear to be a monoidal natural transformation in the official > sense. There are no monoidal functors in sight. > > Can somebody please justify my usage? > > Paul > > > From rrosebru@mta.ca Sun Feb 10 20:54:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 10 Feb 2008 20:54:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOMiw-0000iu-Cb for categories-list@mta.ca; Sun, 10 Feb 2008 20:40:42 -0400 Date: Sun, 10 Feb 2008 11:03:59 -0500 (EST) From: Jeff Egger Subject: categories: Uniformity via Cauchy filters? To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 24 Dear categorists, One of my current research projects has drifted into the realm=20 of uniform locales, which is not exactly my forte. As I went=20 to re-familiarise myself with the assorted definitions, I found myself wondering whether one could define a uniform locale as a=20 locale equipped with a designated set of Cauchy filters, instead=20 of uniform covers, or entourages. Does anyone know whether this=20 idea has already been pursued, either for locales or for spaces? =20 Cheers, Jeff. =20 Looking for the perfect gift? Give the gift of Flickr!=20 http://www.flickr.com/gift/ From rrosebru@mta.ca Mon Feb 11 10:41:14 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 11 Feb 2008 10:41:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOZi9-00022E-61 for categories-list@mta.ca; Mon, 11 Feb 2008 10:32:45 -0400 Date: Mon, 11 Feb 2008 11:32:53 +0100 From: Lutz Schroeder MIME-Version: 1.0 To: categories Subject: categories: AMAST'08 Final Call-For-Papers Content-Type: text/plain; charset=ISO-8859-15 Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 25 [Apologies for multiple copies.] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % The 12th International Conference on % % Algebraic Methodology and Software Technology % % AMAST 2008 % % % % July 28-31, 2008 % % University of Illinois % % Urbana-Champaign, Illinois, USA % % % % http://amast08.cs.uiuc.edu % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SCOPE AND AIMS ============== The major goal of the AMAST conferences is to promote research towards setting software technology on a firm, mathematical basis. Work towards this goal is a collaborative, international effort with contributions from both academia and industry. The envisioned virtues of providing software technology developed on a mathematical basis include (a) correctness, which can be proved mathematically, (b) safety, so that developed software can be used in the implementation of critical systems, (c) portability, i.e., independence from computing platforms and language generations, and (d) evolutionary change, i.e., the software is self-adaptable and evolves with the problem domain. The previous conferences were held in: Iowa City, Iowa, USA (1989, 1991 and 2000); Twente, The Netherlands (1993); Montreal, Canada (1995); Munich, Germany (1996); Sydney, Australia (1997); Manaus, Amazonia, Brazil (1998); Reunion Island, France (2002); Stirling, UK (2004, colocated with MPC' 04); Kuressaare, Estonia (2006, colocated with MPC '06). Topics of interest include, but are not limited to, the following: SOFTWARE TECHNOLOGY: - systems software technology - application software technology - concurrent and reactive systems - formal methods in industrial software development - formal techniques for software requirements, design - evolutionary software/adaptive systems PROGRAMMING METHODOLOGY: - logic programming, functional programming, object paradigms - constraint programming and concurrency - program verification and transformation - programming calculi - specification languages and tools - formal specification and development case studies ALGEBRAIC AND LOGICAL FOUNDATIONS: - logic, category theory, relation algebra, computational algebra - algebraic foundations for languages and systems, coinduction - theorem proving and logical frameworks for reasoning - logics of programs - algebra and coalgebra SYSTEMS AND TOOLS (for system demonstrations or ordinary papers): - software development environments - support for correct software development - system support for reuse - tools for prototyping - component based software development tools - validation and verification - computer algebra systems - theorem proving systems INVITED SPEAKERS ================ Rajeev Alur (confirmed) Edmund M. Clarke Jayadev Misra (confirmed) Teodor Rus (confirmed) AMAST steering committee ======================== Michael Johnson Macquarie University (chair) Egidio Astesiano Universita degli Studi di Genova Robert Berwick MIT Zohar Manna Stanford University Michael Mislove Tulane University Anton Nijholt University of Twente Maurice Nivat Universite Paris 7 Charles Rattray University of Stirling Teodor Rus University of Iowa Giuseppe Scollo Universita degli Studi di Catania Michael Sintzoff Universite Catholique de Louvain Jeannette Wing Carnegie Mellon University Martin Wirsing Ludwig-Maximilians-Universitat Munchen PROGRAM COMMITTEE ================= Gilles Barthe France INRIA Sophia-Antipolis Michel Bidoit France INRIA Saclay - Ile-de-France Manfred Broy Germany Technische Universitat Munchen Roberto Bruni Italy University of Pisa Mads Dam Sweden Royal Institute of Technology (KTH), Stockholm Razvan Diaconescu Romania Institute of Mathematics (IMAR) Jose Fiadeiro UK University of Leicester Rob Goldblatt New Zealand Victoria University Bernhard Gramlich Austria Vienna University of Technology Radu Grosu USA State University of New York at Stony Brook Anne Haxthausen Denmark Technical University of Denmark Rolf Hennicker Germany Ludwig-Maximilians-Universitat Munchen Michael Johnson Australia Macquarie University Helene Kirchner France INRIA Loria, Nancy Paul Klint The Netherlands CWI and Universiteit van Amsterdam Gary T. Leavens USA University of Central Florida Narciso Marti-Oliet Spain Universidad Complutense de Madrid Jose Meseguer (co-chair) USA University of Illinois at Urbana-Champaign Michael Mislove USA Tulane University Ugo Montanari Italy University of Pisa Larry Moss USA Indiana University Till Mossakowski Germany DFKI Bremen Peter Mosses UK Swansea University Fernando Orejas Spain Technical University of Catalonia, Barcelona Dusko Pavlovic USA Kestrel Institute and Oxford University Grigore Rosu (co-chair) USA University of Illinois at Urbana-Champaign Jan Rutten The Netherlands CWI and Vrije Universiteit Amsterdam Lutz Schroeder Germany DFKI Bremen/Universitat Bremen Wolfram Schulte USA Microsoft Research Giuseppe Scollo Italy Universita di Catania Henny Sipma USA Stanford University Doug Smith USA Kestrel Institute Carolyn Talcott USA SRI International Andrzej Tarlecki Poland Warsaw University Varmo Vene Estonia University of Tartu Martin Wirsing Germany Ludwig-Maximilians-Universitat Munchen Uwe Wolter Norway University of Bergen LOCAL ORGANIZATION ================== (all at the University of Illinois Urbana-Champaign) Jose Meseguer Mark Hills Grigore Rosu Ralf Sasse IMPORTANT DATES =============== * Submission of abstracts: 1 March 2008 * Submission of full papers: 8 March 2008 * Notification of authors: 20 April 2008 * Camera-ready version: 15 May 2008 SUBMISSION ========== Two kinds of submissions are solicited for this conference: technical papers and system demonstrations. Papers may report academic or industrial progress, and papers which deal with both are especially well-regarded. Submission is in two stages. Abstracts (plain text) must be submitted by 1 March 2008. Full papers (pdf) adhering to the llncs style and not longer than 15 pages (6 pages for system demonstrations) must be submitted by 8 March 2008. Submissions will be open soon. Papers must report previously unpublished work and not be submitted concurrently to another conference with refereed proceedings. Accepted papers must be presented at the conference by one of the authors. All papers will be refereed by the programme committee, and will be judged based on their significance, technical merit, and relevance to the conference. The proceedings of AMAST '08 will be published in the Lecture Notes in Computer Science series of Springer-Verlag. From rrosebru@mta.ca Mon Feb 11 19:38:44 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 11 Feb 2008 19:38:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOi8k-0003tl-A2 for categories-list@mta.ca; Mon, 11 Feb 2008 19:32:46 -0400 Date: Mon, 11 Feb 2008 08:13:42 -0800 (PST) From: Bill Rowan To: categories@mta.ca Subject: categories: Re: Uniformity via Cauchy filters? MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 26 Hi Jeff, I don't know about locales, but I worked on issues surrounding taking a uniform space, and forgetting the uniformity but keeping the set of cauchy filters. This turns out to be a nontrivial amount of forgetting. I liked the result because the resulting category, which I call the category of completable spaces, can be used as a base category and, for example, if you have a commutative ring, you can look at the compatible completabilities on it (making it a completable space with the discrete completability) and they generalize the valuations on a field. Bill Rowan On Sun, 10 Feb 2008, Jeff Egger wrote: > Dear categorists, > > One of my current research projects has drifted into the realm > of uniform locales, which is not exactly my forte. As I went > to re-familiarise myself with the assorted definitions, I found > myself wondering whether one could define a uniform locale as a > locale equipped with a designated set of Cauchy filters, instead > of uniform covers, or entourages. Does anyone know whether this > idea has already been pursued, either for locales or for spaces? > > Cheers, > Jeff. > > > > Looking for the perfect gift? Give the gift of Flickr! > > http://www.flickr.com/gift/ > > > > From rrosebru@mta.ca Mon Feb 11 19:38:44 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 11 Feb 2008 19:38:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOi9t-000413-OE for categories-list@mta.ca; Mon, 11 Feb 2008 19:33:57 -0400 Date: Mon, 11 Feb 2008 11:59:32 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: Uniformity via Cauchy filters? MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 27 Jeff Egger wrote in part: >one could define a uniform locale as a >locale equipped with a designated set of Cauchy filters This can be done, although you get a more general notion: a _Cauchy_space_ (or locale, but spaces have a bigger literature). Note that a uniform space is a Cauchy space with extra ~structure~; there is no way, in a mere Cauchy space, to compare sizes of neighbourhoods of different points. For the basic definition, you could do worse than the English Wikipedia: < http://en.wikipedia.org/wiki/Cauchy_space >. I had some references (monographs) that I liked too, but I can't find them now; perhaps I can find them tomorrow. --Toby From rrosebru@mta.ca Tue Feb 12 10:20:12 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 12 Feb 2008 10:20:12 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOvna-0005CJ-Ve for categories-list@mta.ca; Tue, 12 Feb 2008 10:07:51 -0400 From: Aleks Nanevski To: categories@mta.ca Date: Mon, 11 Feb 2008 17:24:15 +0000 Subject: categories: IMLA'08: Call for Papers Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 28 Fourth Internation Workshop on Intuitionistic Modal Logic and Applications (IMLA'08) (http://www.cs.bham.ac.uk/~vdp/IMLA08.html) A LICS'08 affiliated workshop Pittsburgh, Pennsylvania, June 23, 2008 Constructive modal logics and type theories are of increasing foundational = and practical relevance in computer science. Applications are in type disci= plines for programming languages, and meta-logics for reasoning about a var= iety of computational phenomena. Theoretical and methodological issues center around the question of how the= proof-theoretic strengths of constructive logics can best be combined with= the model-theoretic strengths of modal logics. Practical issues center aro= und the question which modal connectives with associated laws or proof rule= s capture computational phenomena accurately and at the right level of abst= raction. This workshop will bring together designers, implementers, and users to dis= cuss all aspects of intuitionistic modal logics and type theories. Topics = include, but are not limited to: * applications of intuitionistic necessity and possibility * monads and strong monads * constructive belief logics and type theories * applications of constructive modal logic and modal type theory to formal = verification, foundations of security, abstract interpretation, and program= analysis and optimization * modal types for integration of inductive and co-inductive types, higher-o= rder abstract syntax, strong functional programming * models of constructive modal logics such as algebraic, categorical, Kripk= e, topological, and realizability interpretations * notions of proof for constructive modal logics * extraction of constraints or programs from modal proofs * proof search methods for constructive modal logics and their implementati= ons The workshop continues a series of previous LICS-affiliated workshops, whic= h were held as part of FLoC'99, Trento, Italy and of FLoC'02, Copenhagen, Denmark. We solicit submissions on work in progress and on more mature results. Subm= issions should be extended abstracts of 5-10 pages sent in PostScript or PDF format to the program co-chair at aleksn@microsoft.com. IMPORTANT DATES: Submission: April 25, 2008 Notification: May 23, 2008 Final papers due: June 7, 2008 Workshop Date: June 23, 2008 It is planned to publish workshop proceedings as Electronic Notes in Theore= tical Computer Science (ENTCS) or in CEURS, to be decided. Authors please u= se the generic ENTCS macro package at http://www.math.tulane.edu/~entcs. PROGRAM COMMITTEE: Gavin Bierman (Microsoft, UK) Valeria de Paiva (PARC, USA) Michael Mendler (Bamberg, DE) Aleks Nanevski (Microsoft, UK) Brigitte Pientka (McGill, CA) Eike Ritter (Birmingham, UK) INVITED SPEAKERS: Frank Pfenning (CMU, USA) Torben Brauner (Roskilde, RK) CONTACTS Valeria de Paiva Aleks Nanevski PARC, Palo Alto Research Center Microsoft Research paiva@parc.xeroc.com aleksn@microsoft.com From rrosebru@mta.ca Tue Feb 12 10:20:12 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 12 Feb 2008 10:20:12 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JOvoO-0005Jj-BE for categories-list@mta.ca; Tue, 12 Feb 2008 10:08:40 -0400 Date: Tue, 12 Feb 2008 11:06:09 +0100 (MET) From: Patrik Eklund To: categories@mta.ca Subject: categories: Re: Uniformity via Cauchy filters? MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 29 Might be interesting to note that Cauchy and filters with convergence etc can be described now in more generality involving underlying (partially ordered) monads. See e.g. http://books.google.com/books?id=EoJGeBZVOaQC&pg=PA65&lpg=PA65&dq=%22partially+ordered+monad%22+eklund&source=web&ots=Jg6-Pbj-z5&sig=lFHkMQ-_VjvQMxHMfTryuHprKPQ#PPA102,M1 http://sevein.matap.uma.es/~aciego/mat-es/patrik.pdf Cheers, Patrik On Mon, 11 Feb 2008, Toby Bartels wrote: > Jeff Egger wrote in part: > >> one could define a uniform locale as a >> locale equipped with a designated set of Cauchy filters > > This can be done, although you get a more general notion: > a _Cauchy_space_ (or locale, but spaces have a bigger literature). > Note that a uniform space is a Cauchy space with extra ~structure~; > there is no way, in a mere Cauchy space, > to compare sizes of neighbourhoods of different points. > > For the basic definition, you could do worse than the English Wikipedia: > < http://en.wikipedia.org/wiki/Cauchy_space >. > I had some references (monographs) that I liked too, > but I can't find them now; perhaps I can find them tomorrow. > > > --Toby > > From rrosebru@mta.ca Wed Feb 13 20:36:25 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 13 Feb 2008 20:36:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JPRvI-0001nZ-BS for categories-list@mta.ca; Wed, 13 Feb 2008 20:25:56 -0400 Date: Tue, 12 Feb 2008 16:34:09 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: Uniformity via Cauchy filters? MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 30 I wrote in part: >I had some references (monographs) that I liked too, >but I can't find them now; perhaps I can find them tomorrow. I've (re-)found this one: Eva Lowen-Colebunders (1989). Function Classes of Cauchy Continuous Maps. Dekker, New York, 1989. This has many pretty diagrams of various categories of spaces, all included in one another by bireflections and the like. The whole subject seems messy, as point-set topology can be, (there are too many categories around to keep track of), and probably needs to be cleaned up somewhat before outsiders (including me) can get a grasp on it; in particular, perhaps locales would be a better approach. OTOH, my reference is nearly 20 years old, and perhaps the situation has improved. Indeed, perhaps this is what Paul Ekland's references are doing; I haven't looked at them carefully yet. --Toby From rrosebru@mta.ca Wed Feb 13 20:36:25 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 13 Feb 2008 20:36:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JPRtz-0001ar-RB for categories-list@mta.ca; Wed, 13 Feb 2008 20:24:35 -0400 Date: Tue, 12 Feb 2008 18:15:06 +0100 From: =?ISO-8859-15?Q?Bernhard_M=F6ller?= MIME-Version: 1.0 To: Verborgene_Empfaenger:; Subject: categories: Call for Participation RELMICS10/AKA5 Content-Type: text/plain; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 31 [Apologies for multiple copies.] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Call for Participation % % % % RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 10th International Conference on Relational Methods in Computer Science (RelMiCS10) joint with 5th International Conference on Applications of Kleene Algebra (AKA5) 7-11 April 2008 Frauenw=F6rth (near Munich), Germany http://www.uni-augsburg.de/rel_aka The RelMiCS Conference is the main forum for the relational calculus as a conceptual and methodological tool. The AKA Conference is a meeting on topics related to Kleene algebras. As in previous years, the two events are co-organised; they have a joint programme committee and joint proceedings. Registration deadline: 15 March 2006 PROGRAMME: The conference features 2 invited talks and 26 contributed papers. In addition, there is a PhD programme with 3 invited tutorial and 8 contributed talks; participation is open for everyone. Invited Talks: Marc Pauly (Standford) Formal Methods and the Theory of Social Choice Gunther Schmidt (Munich) Relations Making Their Way From Logics to Mathematics and Applied Sciences The full programme as well as registration details are available at the conference website. For further inquiries please contact the local organisers under rel_aka08@informatik.uni-augsburg.de. SPONSORS: ARIVA.DE AG (Kiel) CrossSoft (Kiel) Deutsche Forschungsgemeinschaft DFG HSH Nordbank AG (Kiel) COMMITTEES: General Chair: Rudolf Berghammer, Kiel, Germany Bernhard Moeller, Augsburg, Germany Local Organisation: Bernhard Moeller, Augsburg, Germany Roland Glueck, Augsburg, Germany Peter Hoefner, Augsburg, Germany Iris Kellner, Augsburg, Germany Ulrike Pollakowski, Kiel, Germany Programme Committee: Rudolf Berghammer, Kiel, Germany Harrie de Swart, Tilburg, The Netherlands Jules Desharnais, Laval, Canada Marcelo Frias, Buenos Aires, Argentina Hitoshi Furusawa, Kagoshima, Japan Peter Jipsen, Chapman, USA Wolfram Kahl, McMaster, Canada Yasuo Kawahara, Kyushu, Japan Bernhard Moeller, Augsburg, Germany Carroll Morgan New South Wales, Australia Manuel Ojeda Aciego, M=E1laga, Spain Ewa Orlowska, Warsaw, Poland Susanne Saminger, Linz, Austria Gunther Schmidt, Munich, Germany Renate Schmidt, Manchester, UK Giuseppe Scollo, Catania, Italy Georg Struth, Sheffield, UK Andrzej Szalas, Link=F6ping, Sweden Johan van Benthem, Amsterdam, The Netherlands Michael Winter, Brock U., Canada --=20 Prof. Dr. Bernhard M=F6ller | http://www.informatik.Uni-Augsburg.DE/~moeller/ Institut f=FCr Informatik | Tel: ++49-821-598-2164 Universit=E4t Augsburg | Fax: ++49-821-598-2274 Universit=E4tsstr. 14, D-86135 Augsburg, Germany From rrosebru@mta.ca Thu Feb 14 22:59:36 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 14 Feb 2008 22:59:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JPqc4-0001pE-Rb for categories-list@mta.ca; Thu, 14 Feb 2008 22:47:44 -0400 Date: Thu, 14 Feb 2008 15:06:49 -0500 From: PETER EASTHOPE Subject: categories: A small cartesian closed concrete category To: categories@mta.ca MIME-version: 1.0 Content-type: text/plain; charset=us-ascii Content-language: en Content-transfer-encoding: 7bit Content-disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 32 Is there a cartesian closed concrete category which is small enough to write out explicitly? It would be helpful in learning about map objects, exponentiation, distributivity and etc. Can such a category be made with binary numbers for instance? Thanks, ... Peter E. http://carnot.yi.org/ From rrosebru@mta.ca Fri Feb 15 10:43:09 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 15 Feb 2008 10:43:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQ1hV-0006Xq-7n for categories-list@mta.ca; Fri, 15 Feb 2008 10:38:05 -0400 Date: Thu, 14 Feb 2008 22:46:44 -0500 From: "Fred E.J. Linton" Subject: categories: Re: A small cartesian closed concrete category To: Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 33 On Thu, 14 Feb 2008 10:07:27 PM EST, PETER EASTHOPE asked: > Is there a cartesian closed concrete category which > is small enough to write out explicitly? = How about the full category of finite sets? Or, = if that's not small enough, and you really fancy an example > ... made with binary numbers for instance , try the skeletal version of the full category of "sets of cardinality < 2= " having as only objects the ordinal numbers 0 and 1. Here 0 x A =3D 0, 1 x A =3D A, 0^1 =3D 0, 0^0 =3D 1, 1^A =3D 1. In other words, B x A =3D min(A, B), B^A =3D max(1-A, B). Happy Valentines's Day! -- Fred From rrosebru@mta.ca Fri Feb 15 10:43:09 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 15 Feb 2008 10:43:09 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQ1i2-0006co-PZ for categories-list@mta.ca; Fri, 15 Feb 2008 10:38:38 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Re: A small cartesian closed concrete category Date: Fri, 15 Feb 2008 08:18:57 +0000 To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 34 Peter Easthope asked, > Is there a cartesian closed concrete category which > is small enough to write out explicitly? It would be > helpful in learning about map objects, exponentiation, > distributivity and etc. Can such a category be made > with binary numbers for instance? How about finite sets and functions? Not just a CCC but an elementary topos. I'm not sure what you mean by "binary numbers", but the powerset of n is 2^n (I wonder why Cantor introduced this notation?), and the subsets of n are n-digit binary numbers. As for more general function spaces, maybe it's worth an undergraduate exercise to see whether there's a neat representation. NBB: You don't need even to have heard of domain theory to find examples of CCCs! Paul Taylor From rrosebru@mta.ca Fri Feb 15 15:23:16 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 15 Feb 2008 15:23:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQ64W-0003yi-Ed for categories-list@mta.ca; Fri, 15 Feb 2008 15:18:08 -0400 Date: Fri, 15 Feb 2008 13:08:11 -0600 From: "Matt Hellige" Subject: categories: Re: A small cartesian closed concrete category To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 35 On Thu, Feb 14, 2008 at 9:46 PM, Fred E.J. Linton wrote: > On Thu, 14 Feb 2008 10:07:27 PM EST, PETER EASTHOPE > asked: > > > Is there a cartesian closed concrete category which > > is small enough to write out explicitly? > > try the skeletal version of the full category of "sets of cardinality < 2" > having as only objects the ordinal numbers 0 and 1. > > Here 0 x A = 0, 1 x A = A, 0^1 = 0, 0^0 = 1, 1^A = 1. > In other words, B x A = min(A, B), B^A = max(1-A, B). > Or, in case that's too small, what about any short chain? For instance, let S = {0,1,2,3} and say there exists a morphism a -> b iff a < b. I believe this is cartesian closed, and I believe it can easily be understood as concrete. This should be enough to give non-trivial product and exponentiation, but you can still draw the whole diagram. Matt -- Matt Hellige / matt@immute.net http://matt.immute.net From rrosebru@mta.ca Fri Feb 15 15:23:16 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 15 Feb 2008 15:23:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQ63Z-0003qF-JD for categories-list@mta.ca; Fri, 15 Feb 2008 15:17:09 -0400 Date: Fri, 15 Feb 2008 18:25:19 +0000 From: "Jamie Vicary" To: categories@mta.ca Subject: categories: Finite limits in a category of free modules over a semiring MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 36 Dear category theorists, Given a commutative semiring R, construct the category that has nonnegative integers as objects, and matrices with entries in R as morphisms, such that the hom-set from N to M consists of matrices with M rows and N columns. This is then just the category of finitely-generated free R-modules. It admits a symmetric monoidal structure given by tensor product of modules, and has finite biproducts, with the induced CMon-enrichment agreeing with addition in R. Is there a nice way to characterise the semirings R for which this category has binary equalisers, and hence all finite limits? Note that the category is equal to its opposite, identifying each matrix with its transpose, and so it will have finite colimits iff it has finite limits. Also, we assume that our semiring has a 0 and a 1, is distributive, and that x.0=0.x=0 for all x in R. Jamie. PS: There was a interesting discussion of this towards the end of this page: http://golem.ph.utexas.edu/category/2007/11/geometric_representation_theor_13.html From rrosebru@mta.ca Fri Feb 15 21:24:51 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 15 Feb 2008 21:24:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQBer-00034b-Ja for categories-list@mta.ca; Fri, 15 Feb 2008 21:16:01 -0400 Date: Sat, 16 Feb 2008 01:17:24 +0100 From: Andrej Bauer MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: A small cartesian closed concrete category Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 37 PETER EASTHOPE wrote: > Is there a cartesian closed concrete category which > is small enough to write out explicitly? It would be > helpful in learning about map objects, exponentiation, > distributivity and etc. Can such a category be made > with binary numbers for instance? A Heyting algebra, viewed as a category (every poset is a category), is a CCC. If you take a small Heyting algebra, e.g. the topology of a finite topological space, you can write it out explicitly. If you would like a CCC made from n-bit binary numbers, here is how you can do it: The two-point lattice B = {0, 1} is a Boolean algebra with the usual logical connectives as the operations. Because B is a poset with 0<=1, it is also a category (with two objects 0, 1 and a morphism between them). Since every Boolean algebra is a Heyting algebra, B is cartesian closed, with the following structure: - 1 is the terminal object - the product X x Y is the conjuction X & Y - the exponential Y^X is the implicatoin X => Y The product of n copies of B is the same thing as n-tuples of bits, i.e., the n-bit numbers. This is again a CCC (with coordinate-wise structure). At this late hour I cannot see what can be said about finite CCC's which are not (eqivalent to) posets. Andrej From rrosebru@mta.ca Sat Feb 16 10:19:51 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 16 Feb 2008 10:19:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQNhT-0004PF-5l for categories-list@mta.ca; Sat, 16 Feb 2008 10:07:31 -0400 To: categories@mta.ca From: Thorsten Altenkirch Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Subject: categories: Re: A small cartesian closed concrete category Date: Sat, 16 Feb 2008 12:21:01 +0000 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 38 On 16 Feb 2008, at 00:17, Andrej Bauer wrote: > PETER EASTHOPE wrote: >> Is there a cartesian closed concrete category which >> is small enough to write out explicitly? It would be >> helpful in learning about map objects, exponentiation, >> distributivity and etc. Can such a category be made >> with binary numbers for instance? > > A Heyting algebra, viewed as a category (every poset is a category), > is > a CCC. If you take a small Heyting algebra, e.g. the topology of a > finite topological space, you can write it out explicitly. > > If you would like a CCC made from n-bit binary numbers, here is how > you > can do it: > > The two-point lattice B = {0, 1} is a Boolean algebra with the usual > logical connectives as the operations. Because B is a poset with 0<=1, > it is also a category (with two objects 0, 1 and a morphism between > them). Since every Boolean algebra is a Heyting algebra, B is > cartesian > closed, with the following structure: > - 1 is the terminal object > - the product X x Y is the conjuction X & Y > - the exponential Y^X is the implicatoin X => Y > > The product of n copies of B is the same thing as n-tuples of bits, > i.e., the n-bit numbers. This is again a CCC (with coordinate-wise > structure). > > At this late hour I cannot see what can be said about finite CCC's > which > are not (eqivalent to) posets. Indeed, are there any at all? If you have coproducts you can define the infinite collection of objectss 0,1,2,... and if you identify any of those you get equational inconsistency. A similar construction should also work for CCCs. In the simply typed lambda calculus with one base type o you can iterpret n as o^n -> o and you get equational inconsistency if you identify any two finite types. This carries over to a finite collection of base types, and hence there cannot be a finite CCC which isn't a preorder. I am sure there must be a more elegant proof of this. Cheers, Thorsten From rrosebru@mta.ca Sat Feb 16 10:19:51 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 16 Feb 2008 10:19:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQNg9-0004Jn-W7 for categories-list@mta.ca; Sat, 16 Feb 2008 10:06:10 -0400 From: Colin McLarty To: categories@mta.ca Date: Fri, 15 Feb 2008 20:51:48 -0500 MIME-Version: 1.0 Subject: categories: Re: A small cartesian closed concrete category Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 39 Every finite category with binary products is a preorder: any two objects A,B have at most one arrow A-->B. Otherwise the successive powers of B would have unboundedly many arrows from A. This is Peter Freyd's proof that small complete categories are preorders. Andrei would have thought of it at a more reasonable hour. Colin From rrosebru@mta.ca Sun Feb 17 15:48:36 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 17 Feb 2008 15:48:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQpIe-0001F3-Pp for categories-list@mta.ca; Sun, 17 Feb 2008 15:35:44 -0400 Date: Sat, 16 Feb 2008 20:55:45 -0500 From: "Fred E.J. Linton" To: Subject: categories: Re: Finite limits in a category of free modules over a semiring Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 40 Greetings. On Fri, 15 Feb 2008 02:30:45 PM EST, "Jamie Vicary" wrote: > Given a commutative semiring R, construct the category that has > nonnegative integers as objects, and matrices with entries in R as > morphisms, such that the hom-set from N to M consists of matrices with = M > rows and N columns. This is then just the category of finitely-generate= d > free R-modules. It admits a symmetric monoidal structure given by tenso= r > product of modules, and has finite biproducts, with the induced > CMon-enrichment agreeing with addition in R. Is there a nice way to > characterise the semirings R for which this category has binary equalis= ers, > and hence all finite limits? > = > Note that the category is equal to its opposite, identifying each matrix > with its transpose, and so it will have finite colimits iff it has fini= te > limits. ... While I offer no answer, I will point out that coequalizers here = (and, by the same token, equalizers) need not look like what you might expect. For example, when the commutative semiring R is the ordinary ring of integers, so that the category of R-matrices "is" = the full category of f.-g. free abelian groups, the coequalizer of the pair of 1x1 matrices (2): 1 --> 1 and (0): 1 --> 1 exists and is !: 1-->0 , with the "expected" coequalizer value of Z/2Z being = "unavailable here." So: beware! Cheers, -- Fred From rrosebru@mta.ca Mon Feb 18 11:16:19 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 18 Feb 2008 11:16:19 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JR7az-0005H5-EB for categories-list@mta.ca; Mon, 18 Feb 2008 11:07:53 -0400 From: Martin Escardo MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Date: Mon, 18 Feb 2008 00:17:02 +0000 To: categories@mta.ca Subject: categories: a monad Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 41 Have you come across the following strong monad? Until I learn that it already has a name, I'll temporarily call it the selection monad, and denote it by S = (S,mu,eta). It is defined on an arbitrary cartesian closed category C after choosing an object V of C. Probably a monoidal closed category will do, but I haven't paused to consider this. On objects, define SX = X^(V^X) = ((X -> V) -> X). (One can contravariantly change the value object V, but I won't consider this in this message.) Think of elements of V^X as V-valued predicates, ranged over by p, and of elements of SX as selection functionals, ranged over by epsilon (like Hilbert's epsilon operator). Intuition: epsilon(p) picks an element x of X (perhaps among elements of a subset A of X) such that p(x) holds, if such an element exists. On morphisms f : X -> Y, define Sf: SX -> SY, using the lambda-calculus, with "\" as the notation for "lambda", and "o" for composition: Sf : SX -> SY epsilon |-> \p.f(epsilon(p o f)) This is easily seen to be functorial. Intuition: if epsilon selects elements among a subset A of X, then Sf(epsilon) selects elements among the set f(A). To do that, we first find an element x in A such that p(f(x)) holds, and then apply f to it. For the unit, take eta :: X -> SX x |-> \p.x Intuition: epsilon = eta(x) selects elements in the singleton set {x}, no matter which predicate p is given. For multiplication, take mu : S(S X) -> S X E |-> \p. E(\epsilon. p(epsilon p)) p Intuition: Given a selection operator E of selection operators, and given a predicate p, we select a selection operator epsilon, among the ones that E can select, such that epsilon selects an element x = epsilon(p) with p(x), and then apply such a selection operator to p to finally get such an element x. The unit and associativity laws are easily (but a bit laboriously) verified. This monad is strong, with strength t = t_{X,Y} defined by t : X x SY -> S(X x Y) (x, epsilon) |-> \p.(x, epsilon(\y.p(x,y))) Intuition: if epsilon selects elements among a subset B of Y, then t(x,epsilon) selects elements among the set {x} x B. This of course, using the monad structure and cartesian closedness, extends to a map times : SX x SY -> S(X x Y) Intuition: if epsilon_X and epsilon_Y select elements among sets A and B, then times(epsilon_X,epsilon_Y) selects among elements of A x B. (I don't think the strength is commutative.) Of course, one is familiar with the "continuation" monad QX=V^(V^X). There is a monad morphism SX -> QX epsilon |-> \p. p(epsilon p) My question is: have you come across the strong monad S (and its relationship to the monad Q)? Of course, S has many interesting submonads for particular choices of V, which correspond to submonads of Q that have been considered. I carry on a bit further. Suppose our category C has a nno N=(N,s,0), and write x+1=sx. Then we can define a natural isomorphism cons = cons_X cons : X x X^N <---> X^N : (head,tail) with head(alpha)=alpha(0) and tail(alpha)(n)=alpha(n+1). Then, as is well known, the map (head,tail) is a final coalgebra for the functor (-) -> X x (-). I want to consider the composite mul = (S cons) o times, mul : SX x S(X^N) -> S(X^N) For a sequence alpha = epsilon_0, epsilon_1, epsilon_2 ... of epsilon operators in SX, we may attempt to define the infinitely iterated product mul(epsilon_0, mul(epsilon_1, mul(epsilon_2, ...) ... )) It turns out that, in particular categories of interest, with a suitable choice of V, this exists. Moreover, there is a unique functional that picks the product selection operator, given the selection operators for the components: prod : (SX)^N -> S(X^N) prod(cons(epsilon,alpha)) = mul(epsilon, prod alpha) or, equivalently, prod o cons = mul o (id x prod) and so this is a kind of algebra homomorphism. The odd thing is that cons is the inverse of the final coalgebra, and, for this particular situation, it is instead playing the role of an initial algebra with respect to mul. (Of course, we are all familiar with odd situations of this kind.) There is no reason why such a unique morphism prod should exist in an arbitrary ccc with a chosen V, and counter-examples are readily obtained. My original example of prod was constructed before I realized there was a monad behind it, and was given by a construction that now can be considered to be rather ad hoc, but that is readily seen to be equivalent to the above formulation. So this message is a sort of apology for overlooking obvious considerations. The example was given in a ccc of computable higher-type functionals (defined on continuous functionals), with V the booleans, and, the point, was indeed, that prod is well defined and computable. I had considered another (more efficient) product functional, based on (seeing sequences as) binary trees. This also is explained, in very much the same (and obvious) way, by the above considerations, but I won't spell it down in this message, which is already long. To compare it with the ad hoc algorithms, I have coded the above categorical definitions in the higher-type programming language Haskell, including the definition of prod derived from them, for both sequences and trees. The performance in particular examples is the same as that of the ad hoc previously given algorithms, apart from a constant factor of approximately 1/2. I could, in principle, have started from the categorical ideas of this message and then derived the algorithms. I wish I had done that. In any case, here are the algorithms as they are derived in this message (including the tree-like product functional): http://www.cs.bham.ac.uk/~mhe/papers/selection-monad.hs MHE. From rrosebru@mta.ca Tue Feb 19 16:44:31 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 19 Feb 2008 16:44:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JRZ4j-000055-TQ for categories-list@mta.ca; Tue, 19 Feb 2008 16:28:25 -0400 From: Michael Mislove To: mfpsmail@lax.math.tulane.edu, categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v919.2) Subject: categories: Clifford Lectures 2008 Date: Tue, 19 Feb 2008 11:23:55 -0600 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 42 Dear Colleagues, This is an invitation to attend the 2008 Clifford Lectures, which will be held at Tulane from March 12 through March 15, 2008. The Clifford Lectures are annual series of lectures hosted by the Tulane Math Department in honoring of A. H. Clifford, noted algebraist, who was a long time member of the department. This year's Clifford Lecturer is Samson Abramsky, and the topic of his lectures is, "Information flow in physics, geometry, logic and computation". Samson will deliver five lectures on this topic during the course of the series. In addition, thirteen researchers are also giving one-hour lectures on this topic as part of the series. You can find details about the speakers, the titles and abstracts of their talks, the program and registration information at the page http://www.math.tulane.edu/~mwm/clifford Best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== From rrosebru@mta.ca Tue Feb 19 16:44:31 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 19 Feb 2008 16:44:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JRZ3u-0007m7-Md for categories-list@mta.ca; Tue, 19 Feb 2008 16:27:34 -0400 Date: Tue, 19 Feb 2008 17:58:14 +0200 (EET) Subject: categories: pssl87 - final announcement From: "Panagis Karazeris" To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-7 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 43 Peripatetic Seminar on Sheaves and Logic 87 Honouring the 70th birthday of Anders Kock Patras, 21-23 March 2008 The 87th Peripatetic Seminar on Sheaves and Logic will be held in Patras, Greece, on 22-23 March 2008. An extra session will be held in the afternoon of Friday 21 March, celebrating the 70th birthday of Anders Kock. A. Joyal, F. W. Lawvere and G. Reyes will participate honouring Anders. Accommodation Information: The University of Patras is located in the suburbs, 10 km NE of the downtown area. The participants have the options of either staying downtown or in one of the hotels along the coast near the University. In the first case they will have to use local transportation (bus or taxi= ). In the second case they may choose to walk (weather permitting) or get a ride by the people involved in the organization. With the second option in mind, a number of rooms has been reserved at Hotel Achaia Beach and will be available at the price of 69 Euros (single room) and 85 Euros (double room), provided that reservatio= n is confirmed before 15 January 2008. The hotel is 2,5 km away from the PSSL venue and has the extra advantage of being close to some fine restaurants and in walking distance from the cafes, bars and restaurants of the coast of Rion, which starts getting lively at that time of the year. A small number of rooms will be availabl= e until Friday 22 February 2008. If you wish to book a hotel room yourself you may consult http://www.tripadvisor.com/Hotels-g189488-Patras_Peloponnese-Hotels.html Registration: You may register for PSSL87 by filling out the following fo= rm REGISTRATION FORM Name: ....... Affiliation: ..... I wish to give a talk: YES/NO Title: ..... Arrival Date: .... Departure Date: .... I wish to book a hotel room in Achaia Beach Hotel: YES/NO - SINGLE/DOUBLE and submitting it to pssl87@math.upatras.gr Transportation Information: Patras is located 220km W of the Athens airport. The best way to approach it is to use the Athens Suburban Railway (Proastiakos) which stretches west up to the town of Kiato, on the northern coast of the Peloponnese, 110km away from Patras. The idea is to arrange some private car or coach rides from Kiato to Patras, according to the date and time of arrival of most of you. Otherwise there is the option of getting on the (slow, narro= w gauge) train to Patras. Further details as well as a list of participants appear in the meeting's webpage http://www.math.upatras.gr/~pssl87/ From rrosebru@mta.ca Wed Feb 20 17:23:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 20 Feb 2008 17:23:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JRwAd-0006Ci-B3 for categories-list@mta.ca; Wed, 20 Feb 2008 17:08:03 -0400 Date: Wed, 20 Feb 2008 19:41:43 +0100 (CET) Subject: categories: position at Utrecht From: moerdijk@math.uu.nl To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 44 Dear colleagues, I'd like to draw your attention to an opening for a tenure (track) position at Utrecht, at the level of "universitair docent" (comparable to Lecturer in the UK, Assistant Professor in the US or Maitre de Conferences in France). The position is related to a large group grant in the area between (and including) geometry/topology and mathematical physics, which I'm sure will fit the interests of many readers of this list. For more information, see http://www.math.uu.nl/Main/Department/Positions= / It is vacancy #62800 on the list of four. With best regards, Ieke Moerdijk. --=20 From rrosebru@mta.ca Sat Feb 23 11:14:26 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 23 Feb 2008 11:14:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JSvsk-0002Gq-3O for categories-list@mta.ca; Sat, 23 Feb 2008 11:01:42 -0400 Subject: categories: FM'08 -- CALL FOR PARTICIPATION To: events@fmeurope.org MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 From: events-admin@fmeurope.org Date: Fri, 22 Feb 2008 16:15:39 +0100 (CET) Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 45 *** Apologies if you receive multiple copies. *** FM'08: 15TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS May 26 - 30, 2008 =C5bo Akademi University Turku, Finland CALL FOR PARTICIPATION http://www.fm2008.abo.fi/ It is our pleasure to invite you to FM'08, the premier international foru= m for practitioners and researchers applying mathematical methods to the design of highly reliable computer systems. FM'08 is the fifteenth in a series of symposia organized by Formal Method= s Europe, http://www.fmeurope.org, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development, industrial users as well as researchers. A program of five invited talks and 23 outstanding research papers provides the opportunity to learn about the newest developments in the theory and application of formal methods. The program covers a wide range of topics, including real-time and concurrency, design, verification, communication, runtime monitoring and analysis, constraint analysis, programming language analysis, formal methods practice, and grand challenge problems. As in the previous years, an Industry Day is dedicate= d for practitioners to share their experiences with industrial applications= . This year's Industry Day investigates telecommunications and embedded systems, being supported by NOKIA. Speakers from five major industries will address this year's theme, together with the Johnson Professor Arvin= d from MIT. Tutorials are a central part of this year=92s FM symposium, as an effecti= ve way of disseminating emerging application areas, tools, and techniques. This year we have seven tutorials, given by renowned experts in their fields. The five co-located workshops address issues of specific formal techniques as well as novel computational models and grand challenges. Th= e following list of tutorials and workshops are available: Tutorials =B7 Computational Systems Biology =B7 Teaching formal methods to students in high school and introductory university courses =B7 Event-B and the Rodin Platform =B7 Why formal verification remains on the fringes of commercial development =B7 Formal Methods and Signal Processing =B7 Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking =B7 Formal modelling and analysis of real-time systems using UPPA= AL Workshops =B7 Formal aspects of virtual organisations =B7 Overture/VDM++ =B7 Refinement workshop =B7 Pilot Projects for the Grand Challenge in Verified Software =B7 Computational Models for Cell Processes A Doctoral Symposium on all aspects of formal methods research is also part of FM=9208, giving young researchers the opportunity to have their ideas critically, but constructively examined by the community. A Poster and Tool Exhibition of both research projects and commercial tools allows researchers to engage in a dialogue with potential users in early phases of their work. The submission date for the both the Doctoral Symposium an= d the Poster and Tool Exhibition is March 7. Registration to all types of events will open during week 8, with the possibility of early registration until March 25. Important dates for submitting papers to the workshops should be identified via the own homepages of these events, reachable from above or from the FM=9208 websi= te. Generally, workshop papers should be submitted in March. The list of the accepted papers to the technical symposium and the preliminary schedule o= f FM=9208 can already be retrieved via our website. We hope you will enjoy a rewarding symposium program! Kaisa Sere, General Chair Jorge Cuellar, Tom Maibaum, Program Chairs _______________________________________________ events mailing list events@fmeurope.org http://www.fmeurope.org/mailman/listinfo/events From rrosebru@mta.ca Sat Feb 23 11:14:26 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 23 Feb 2008 11:14:26 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JSvrP-0002By-7T for categories-list@mta.ca; Sat, 23 Feb 2008 11:00:19 -0400 From: Michael Mislove To: mfpsmail@linus.math.tulane.edu, categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v919.2) Subject: categories: MFPS Final Call for Papers Date: Fri, 22 Feb 2008 08:25:38 -0600 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 46 Dear Colleagues, This is the Final Call for Papers for MFPS 24. Details about the meeting are given below. Submissions should be made to EasyChair at the link http://www.easychair.org/conferences/?conf=mfps24 The deadline for submissions of titles and brief abstracts is Friday, March 7, and the deadline for full submissions is the following Friday, March 14. Thanks, and best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== CALL FOR PAPERS MFPS XXIV http://www.math.tulane.edu/~mfps/mfps24.htm Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics University of Pennsylvania Philadelphia, PA USA May 22 - 25, 2008 Partially Supported by US Office of Naval Research The MFPS conferences are devoted to those areas of mathematics, logic, and computer science which are related to models of computation, in general, and to the semantics of programming languages, in particular. The series has particularly stressed providing a forum where researchers in mathematics and computer science can meet and exchange ideas about problems of common interest. As the series also strives to maintain breadth in its scope, the conference strongly encourages participation by researchers in neighboring areas. TOPICS include, but are not limited to, the following: biocomputation; categorical models; concurrent and distributed computation; constructive mathematics; domain theory; formal languages; formal methods; game semantics; lambda calculus; logic; non-classical computation; probabilistic systems; process calculi; program analysis; programming-language theory; quantum computation; rewriting theory; security; specifications; topological models; type systems; type theory. The Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV) will take place on the campus of University of Pennsylvania, Philadelphia, PA USA from Thursday, May 22 through Sunday, May 25, 2008. The Organising Committee for MFPS consists of Stephen Brookes (CMU), Achim Jung (Birmingham), Catherine Meadows (NRL), Michael Mislove (Tulane), and Prakash Panangaden (McGill). The local arrangements for MFPS XXIV are being overseen by Andre Scedrov (Penn). The INVITED SPEAKERS for MFPS XXIV are Samson Abramsky, Oxford Luca Cardelli, Microsoft Research, Cambridge Dusko Pavlovic, Kestrel Institute Benjamin Pierce, Penn Phil Scott, Ottawa James Worrell, Oxford In addition, there will be four special sessions: - A session honoring Phil Scott on the occasion of his 60th birthday year, which is being organized by Rick Blute (Ottawa) and Andre Scedrov (Penn). - A session on Systems Biology will be held in conjunction with Luca Cardelli's plenaary talk. It is being organized by Jean Krivine (LIX). - A third session will be devoted to Type Theory. It is being organized by Benjamin Pierce and by Robert Harper (CMU) will be held in conjunction with Benjamin Pierce's plenary talk. - The fourth special session will be on Security, and will be organized by Catherine Meadows (NRL) in conjunction with Dusko Pavlovic's plenary talk. Further, there will be a TUTORIAL DAY on May 21. The topic will be Category Theory and Its Applications to Theoretical Computer Science. It is being organized by Phil Scott (Ottawa); the speakers will be announced at a later date. This event will be free to all those who are interested in attending. The remainder of the program will consist of papers selected by the following PROGRAM COMMITTEE Andrej Bauer (Ljubljana), CHAIR Ulrich Berger (Swansea) Lars Birkedal (Copenhagen) Jens Blanck (Swansea) Steve Brookes (CMU) Bob Coecke (Oxford) Karl Crary (CMU) Martin Escardo (Birmingham) Achim Jung (Birmingham) Jean Krivine (LIX) James Laird (Sussex) Paul Levy (Birmingham) Catherine Meadows (NRL) Michael Mislove (Tulane) Catuscia Palamidessi (INRIA) Prakash Panangaden (McGill) Alex Simpson (Edinburgh) Christopher Stone (Harvey Mudd) Thomas Streicher (Darmstadt) James Worrell (Oxford) from submissions received in response to this Call for Papers. Submissions Now Open! Authors can submit papers in response to this Call for Papers by pointing their browser to http://www.easychair.org/conferences/?conf=mfps24 The submission process requires registering as an author and submitting the title and a short abstract for your paper by March 7, 2008. The deadline for submissions of full papers is one week later, March 14, 2008. The other important dates are listed below. Papers should be no more than 15 pages in LaTeX, and should be in the form of either a PostScript file or a pdf file suitable for printing on a generic printer. The accepted papers will appear in ENTCS, and the required format for ENTCS can be used for submissions. The generic ENTCS macro package can be found at this web site. There is no special entcsmacro.sty file for this year's MFPS Proceedings as yet; authors who use the ENTCS macros should just use the file that comes in the generic package. IMPORTANT DATES: * Fri Mar 7: Paper registration deadline, with short abstracts. * Fri Mar 14: Paper submission deadline. * Fri Apr 7: Author notification. * Fri Apr 21: Final versions for the proceedings. From rrosebru@mta.ca Mon Feb 25 09:57:01 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 25 Feb 2008 09:57:01 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JTdbf-00038q-K6 for categories-list@mta.ca; Mon, 25 Feb 2008 09:42:59 -0400 Content-class: urn:content-classes:message MIME-Version: 1.0 Subject: categories: REACHABILITY PROBLEMS (RP'08) Liverpool, 15-17 September 2008 Date: Sun, 24 Feb 2008 10:38:54 -0000 From: "Potapov, Igor" To: Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 47 =20 2nd WORKSHOP ON REACHABILITY PROBLEMS, RP'08 (September 15-17, 2008, Liverpool, UK) Deadline for submissions: 19 May, 2008 http://www.csc.liv.ac.uk/~rp2008/ =20 The Workshop on Reachability Problems will take place at=20 the University of Liverpool, Liverpool, UK on September=20 15-17, 2008. Papers presenting original contributions=20 related to reachability problems in different=20 computational models and systems are being sought.=20 The Reachability Workshop is specifically aimed at gathering=20 together scholars from diverse disciplines and backgrounds=20 interested in reachability problems that appear in - Algebraic structures - Computational models - Hybrid systems - Verification =20 Invited Speakers: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D - Ahmed Bouajjani, Paris, France=20 - Juhani Karhumaki, Turku, Finland=20 - Colin Stirling, Edinburgh, UK=20 - Wolfgang Thomas, Aachen, Germany=20 =20 Submissions: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=20 Papers presenting original contributions related to=20 reachability problems in different computational models=20 and systems are being sought.=20 Topics of interest include (but are not limited to):=20 Reachability probelms in infinite state systems,=20 rewriting systems, dynamical and hybrid systems;=20 reachability problems in logic and verification;=20 reachability analysis in different computational=20 models, counter/ timed/ cellular/ communicating=20 automata; Petri-Nets; computational aspects of=20 algebraic structures (semigroups, groups and rings);=20 predictability in iterative maps and new=20 computational paradigms.=20 =20 Authors are invited to submit a draft of a full paper with=20 at most 12 pages (in standard LaTeX article style 11pt A4 paper)=20 via the conference web page http://www.csc.liv.ac.uk/~rp2008/ .=20 Proofs omitted due to space constraints must be put into an appendix=20 to be read by the program committee members at their discretion. Submissions deviating from these guidelines risk=20 rejection. Electronic submissions should be formatted in=20 postscript or pdf. Simultaneous submission to other conferences=20 or workshops with published proceedings is not allowed. =20 Important dates: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Submission deadline : May 19, 2008=20 Notification to authors: June 30, 2008=20 Final version: July 15, 2008=20 Workshop: September 15-17, 2008=20 =20 The proceedings of the workshop will appear in=20 Electronic Notes in Theoretical Computer Science (ENTCS).=20 ENTCS is published electronically on Science Direct,=20 Elsevier's main platform for electronic publication to=20 provide rapid publication and broad dissemination of the=20 volumes in the series. Selected papers will appear in a=20 special issue of a high quality journal.=20 =20 Program Committee: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D - Parosh Aziz Abdulla , Uppsala=20 - Eugene Asarin , Paris=20 - Vincent Blondel, Louvain=20 - Olivier Bournez, Nancy=20 - Cristian S. Calude , Auckland=20 - Javier Esparza , Munchen=20 - Vesa Halava , Turku=20 - Oscar Ibarra , Santa Barbara=20 - Juhani Karhumaki, Turku=20 - Igor Potapov , Liverpool=20 - Colin Stirling, Edinburgh=20 - Wolfgang Thomas , Aachen=20 - Hsu-Chun Yen , Taipei=20 =20 Organizing Committee: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D - Igor Potapov, Liverpool - Vesa Halava, Turku =20 Contact:=20 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D RP'08,=20 Department of Computer Science, University of Liverpool,=20 Ashton Building, Ashton Street,=20 Liverpool, L69 3BX E-mail: rp2008 [at] csc.liv.ac.uk=20 Web: http://www.csc.liv.ac.uk/~rp2008/ From rrosebru@mta.ca Mon Feb 25 17:27:36 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 25 Feb 2008 17:27:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JTkku-0003C0-DC for categories-list@mta.ca; Mon, 25 Feb 2008 17:21:00 -0400 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=US-ASCII; format=flowed To: categories@mta.ca Content-Transfer-Encoding: 7bit From: Matthew Hennessy Subject: categories: Postdoctoral Fellowhships Date: Mon, 25 Feb 2008 14:42:37 +0000 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 48 Apologies for Multiple Postings --------------------------------------------------- The Foundations of Global Computing - Trinity College Dublin Two postdoctoral Research Fellowships Applications are invited for TWO post-doctoral positions to undertake research into the foundations of Global Computing. The posts are within the Software Systems Lab of the Department of Computer Science at Trinity College Dublin as part of a new SFI-funded research project, under the direction of Matthew Hennessy, which seeks to establish a firm mathematical and logical basis for the next generation of widely distributed computing computing environments. Applicants should have a PhD in Computer Science, or a closely related discipline. Candidates with expertise in following areas are particularly welcome: - operational semantics - concurrency theory - model checking - verification techniques - type theory - program logics These posts are tenable from April 2008 at a salary commensurate with the successful candidates' qualifications and experience. Appointments will be made initially for a 24 month period, although there will be scope for extension. Further particulars of the posts may be obtained from the address below, and informal enquiries are also welcomed. Applications should include - detailed curriculum vitae, in pdf format - copies of relevant publications, or url-pointers to them - the names of two referees - a statement outlining the applicant's suitability to the project. Applications should be sent to: Matthew Hennessy Department of Computer Science The O'Reilly Institute Trinity College Dublin 2 Ireland email: matthew.hennessy@cs.tcd.ie tel: +353 (01) 8962634 Trinity College is an equal opportunities employer. From rrosebru@mta.ca Mon Feb 25 17:27:37 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 25 Feb 2008 17:27:37 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JTkm8-0003K1-DG for categories-list@mta.ca; Mon, 25 Feb 2008 17:22:16 -0400 Date: Mon, 25 Feb 2008 14:21:25 -0500 From: Nath Rao MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Language of an internal category? Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 49 Is there a version of Mitchell-Benabou language for internal categories in toposes (with natural number objects)? What I have in mind is something that will allow automatic translations of definitions and proofs to internal categories that gives the expected results for established notions. [I have glanced through "Relative set theories", and the relevant chapters of Jacobs, "Categorical logic and type theory"; they do not seem to what I am looking for, in the sense that the primary focus is not on the properties of the internal category.] Thanks in advance Nath Rao From rrosebru@mta.ca Tue Feb 26 15:36:29 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 26 Feb 2008 15:36:29 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JU5Pe-0005BA-Ud for categories-list@mta.ca; Tue, 26 Feb 2008 15:24:26 -0400 Mime-Version: 1.0 (Apple Message framework v752.3) Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed To: types-list@lists.seas.upenn.edu, categories@mta.ca From: Russ Harmer Subject: categories: GALOP@ETAPS'08: Call for participation Date: Tue, 26 Feb 2008 12:12:12 +0100 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 50 This is a Call for Participation to the 3rd International Workshop on Games for Logic and Programming =20= Languages (GALOP3) to be held at ETAPS, on 5--6 April 2008, in Budapest. Invited speakers are: # Gabriel Sandu (University of Helsinki): Independence between =20= quantifiers # Merlijn Sevenster (Universiteit van Amsterdam): Independence =20= between modal operators # Paul-Andr=E9 Melli=E8s (PPS, CNRS & Paris-Diderot): Game = semantics as =20 string diagrams More details about the workshop, including a list of accepted =20 contributions, can be found at: http://www.cs.bham.ac.uk/~drg/galop.html To register for the workshop, please use the following link: http://etaps08.mit.bme.hu/ From rrosebru@mta.ca Wed Feb 27 13:09:23 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 27 Feb 2008 13:09:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JUPe6-0003bY-16 for categories-list@mta.ca; Wed, 27 Feb 2008 13:00:42 -0400 Date: Wed, 27 Feb 2008 12:03:53 +0100 From: Clemens Kupke MIME-Version: 1.0 To: cmcs08@cwi.nl Subject: categories: CMCS 08: final call for short contributions Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 51 ---------------------------------------------------------------------- CMCS 08 : FINAL CALL FOR SHORT CONTRIBUTIONS 9th International Workshop on Coalgebraic Methods in Computer Science http://www.cwi.nl/projects/cmcs08/ Budapest, Hungary April 4-6, 2008 Key Note Speaker: Dexter Kozen Invited Speakers: Stefan Milius and Dirk Pattinson The workshop will be held in conjunction with the 11th European Joint Conferences on Theory and Practice of Software ETAPS 2008 March 29 - April 6, 2008 Following the tradition of preceding workshops we invite short contributions that will be collected in a technical report of the Technical University of Braunschweig. They should be no more than two pages and may describe work in progress, summarise work submitted to a conference or workshop elsewhere, or in some other way appeal to the CMCS audience. They should be submitted in postscript or pdf form as attachments to an email to cmcs08@cwi.nl. Deadline for submission of short contributions: March 10, 2008. Notification of acceptance of short contributions: March 17, 2008. Jiri Adamek and Clemens Kupke PC co-chairs From rrosebru@mta.ca Wed Feb 27 20:23:08 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 27 Feb 2008 20:23:08 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JUWRs-0000oe-DN for categories-list@mta.ca; Wed, 27 Feb 2008 20:16:32 -0400 From: Sam Staton To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v919.2) Subject: categories: Mismatch in lcc pretoposes with W-types? Date: Wed, 27 Feb 2008 19:07:21 +0000 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 52 Various people (including Moerdijk & Palmgren, Hyland & Gambino, Abbott & Altenkirch & Ghani) have considered locally cartesian closed pretoposes with W-types, ie initial algebras for generalized polynomial functors, aka 'containers'. (These W-types are an appropriate analysis of the fixed points of intensional constructions and so these categories have been motivated as "constructive toposes", as models of a particular version of Martin-Lof's type theory). Lcc pretoposes are Heyting pretoposes. For any object X, consider those monotone endofunctions on the class Sub(X) that can be constructed from the pullback functors and their left and right adjoints. By my calculations, in a topos, these monotone endofunctions have least and greatest fixed points (by internalizing them and then using Tarski's fixed point theorem). It seems that, in general, these monotone endofunctions will not have least or greatest fixed points in lcc pretoposes with W-types. (I haven't proved this, though, and perhaps I have missed a neat trick.) If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work both intensionally and extensionally, yet when it comes to W-types, we only consider the intensional constructions. Is there a reason for this?-- are these fixed points "non-constructive" or "impredicative" in some sense? Has anybody thought about these things before? Have I missed something? All the best, Sam [My example is bisimilarity for transition systems, as studied in concurrency theory. This is conventionally calculated as a maximum fixed point for a monotone endofunction on the lattice of binary relations. I can define a 'constructive' version of bisimilarity using W-types, and then take the image. This differs from the usual notion, unless choice is assumed.] From rrosebru@mta.ca Thu Feb 28 22:22:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 28 Feb 2008 22:22:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JUugd-0000z8-Gm for categories-list@mta.ca; Thu, 28 Feb 2008 22:09:23 -0400 Mime-Version: 1.0 (Apple Message framework v752.3) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: categories@mta.ca Content-Transfer-Encoding: 7bit From: Neil Ghani Subject: categories: Re: Mismatch in lcc pretoposes with W-types? Date: Thu, 28 Feb 2008 15:41:47 +0000 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 53 Hi All, Since we have a semantic characterisation of containers, we can look at Thorstens question > Alternatively for containers: Every endofunctor which has an > initial algebra is a container. Obviously, this will only hold in > the syntax of Type Theory, i.e. the classifying predicative > pretopos with W-types. Surely, it must be the case that all syntactically definable endofunctors are accessible. And, being syntactic constructions, I'd not be too surprised if they preserved connected limits ... Unless I've got the wrong end of the stick which is entirely possible. All the best Neil On 28 Feb 2008, at 15:32, Thorsten Altenkirch wrote: > Hi Sam, > > the issue you address has to do with the question of predicative > vs. impredicative, I think. > > As you say in a topos any monotone operator on the lattice of > subsets of a given type has a least (and greatest fixpoint). In a > predicative theory like Martin-Loef's Type Theory these fixpoints > only exist if the monotone operator is defined in a *strictly* > positive way. > > There seems to be no simple example of such a fixpoint because all > simple examples turn out to be strictly positive. Here is the > simplest one I can think of in the moment: Let (A,@) be a partial > combinatory algebra, e.g. the natural number with an encoding of > Turing machines. Then choose a subset R \subseteq A to define an > antitone operator F on subsets of A by > > F P = { x:A | all y:A.P y -> R (x @ y) } > > Now clearly FF (do F twice) is monotone and hence will have a least > fixpoint in a topos. However, by a proof-theoretic analysis (I > think) we can show that the fixpoint cannot be constructed in > Martin-Loef Type Theory. (It would be nicer to have a semantical > argument). > > Btw this is just an encoding of Reynold's construction to show that > there are no set-theoretic models of System F. In System F you get > a fixpoint of (X -> 2) -> 2 which corresponds to choosing R to be > an encoding of 2, e.g. > R = {\xy.x,\xy.y}. > > There is a semantic characterisation of strictly positive operators > on subsets which is similar to the concept of containers, I have > used this in joint work with Andreas Abel a while ago (our JFP 2002 > paper and TYPES 99). It would be nice, if one could show that all > operators which have fixpoints are one of those. Alternatively for > containers: Every endofunctor which has an initial algebra is a > container. Obviously, this will only hold in the syntax of Type > Theory, i.e. the classifying predicative pretopos with W-types. > > I am not sure this mismatch is a problem: Do you ever need > fixpoints of non-strict positive operators? > > Cheers, > Thorsten > > On 27 Feb 2008, at 19:07, Sam Staton wrote: > >> Various people (including Moerdijk & Palmgren, Hyland & Gambino, >> Abbott & Altenkirch & Ghani) have considered locally cartesian closed >> pretoposes with W-types, ie initial algebras for generalized >> polynomial functors, aka 'containers'. (These W-types are an >> appropriate analysis of the fixed points of intensional constructions >> and so these categories have been motivated as "constructive >> toposes", >> as models of a particular version of Martin-Lof's type theory). >> >> Lcc pretoposes are Heyting pretoposes. For any object X, consider >> those monotone endofunctions on the class Sub(X) that can be >> constructed from the pullback functors and their left and right >> adjoints. By my calculations, in a topos, these monotone >> endofunctions >> have least and greatest fixed points (by internalizing them and then >> using Tarski's fixed point theorem). >> >> It seems that, in general, these monotone endofunctions will not have >> least or greatest fixed points in lcc pretoposes with W-types. (I >> haven't proved this, though, and perhaps I have missed a neat trick.) >> >> If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work >> both intensionally and extensionally, yet when it comes to W- >> types, we >> only consider the intensional constructions. Is there a reason for >> this?-- are these fixed points "non-constructive" or "impredicative" >> in some sense? >> >> Has anybody thought about these things before? Have I missed >> something? All the best, Sam >> >> >> [My example is bisimilarity for transition systems, as studied in >> concurrency theory. This is conventionally calculated as a maximum >> fixed point for a monotone endofunction on the lattice of binary >> relations. I can define a 'constructive' version of bisimilarity >> using >> W-types, and then take the image. This differs from the usual notion, >> unless choice is assumed.] >> >> > This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. From rrosebru@mta.ca Thu Feb 28 22:22:05 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 28 Feb 2008 22:22:05 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JUufJ-0000u8-4s for categories-list@mta.ca; Thu, 28 Feb 2008 22:08:01 -0400 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: categories@mta.ca Content-Transfer-Encoding: 7bit From: Thorsten Altenkirch Subject: categories: Re: Mismatch in lcc pretoposes with W-types? Date: Thu, 28 Feb 2008 15:32:57 +0000 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 54 Hi Sam, the issue you address has to do with the question of predicative vs. impredicative, I think. As you say in a topos any monotone operator on the lattice of subsets of a given type has a least (and greatest fixpoint). In a predicative theory like Martin-Loef's Type Theory these fixpoints only exist if the monotone operator is defined in a *strictly* positive way. There seems to be no simple example of such a fixpoint because all simple examples turn out to be strictly positive. Here is the simplest one I can think of in the moment: Let (A,@) be a partial combinatory algebra, e.g. the natural number with an encoding of Turing machines. Then choose a subset R \subseteq A to define an antitone operator F on subsets of A by F P = { x:A | all y:A.P y -> R (x @ y) } Now clearly FF (do F twice) is monotone and hence will have a least fixpoint in a topos. However, by a proof-theoretic analysis (I think) we can show that the fixpoint cannot be constructed in Martin-Loef Type Theory. (It would be nicer to have a semantical argument). Btw this is just an encoding of Reynold's construction to show that there are no set-theoretic models of System F. In System F you get a fixpoint of (X -> 2) -> 2 which corresponds to choosing R to be an encoding of 2, e.g. R = {\xy.x,\xy.y}. There is a semantic characterisation of strictly positive operators on subsets which is similar to the concept of containers, I have used this in joint work with Andreas Abel a while ago (our JFP 2002 paper and TYPES 99). It would be nice, if one could show that all operators which have fixpoints are one of those. Alternatively for containers: Every endofunctor which has an initial algebra is a container. Obviously, this will only hold in the syntax of Type Theory, i.e. the classifying predicative pretopos with W-types. I am not sure this mismatch is a problem: Do you ever need fixpoints of non-strict positive operators? Cheers, Thorsten On 27 Feb 2008, at 19:07, Sam Staton wrote: > Various people (including Moerdijk & Palmgren, Hyland & Gambino, > Abbott & Altenkirch & Ghani) have considered locally cartesian closed > pretoposes with W-types, ie initial algebras for generalized > polynomial functors, aka 'containers'. (These W-types are an > appropriate analysis of the fixed points of intensional constructions > and so these categories have been motivated as "constructive toposes", > as models of a particular version of Martin-Lof's type theory). > > Lcc pretoposes are Heyting pretoposes. For any object X, consider > those monotone endofunctions on the class Sub(X) that can be > constructed from the pullback functors and their left and right > adjoints. By my calculations, in a topos, these monotone endofunctions > have least and greatest fixed points (by internalizing them and then > using Tarski's fixed point theorem). > > It seems that, in general, these monotone endofunctions will not have > least or greatest fixed points in lcc pretoposes with W-types. (I > haven't proved this, though, and perhaps I have missed a neat trick.) > > If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work > both intensionally and extensionally, yet when it comes to W-types, we > only consider the intensional constructions. Is there a reason for > this?-- are these fixed points "non-constructive" or "impredicative" > in some sense? > > Has anybody thought about these things before? Have I missed > something? All the best, Sam > > > [My example is bisimilarity for transition systems, as studied in > concurrency theory. This is conventionally calculated as a maximum > fixed point for a monotone endofunction on the lattice of binary > relations. I can define a 'constructive' version of bisimilarity using > W-types, and then take the image. This differs from the usual notion, > unless choice is assumed.] > > This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. From rrosebru@mta.ca Fri Feb 29 09:40:35 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 29 Feb 2008 09:40:35 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JV5MN-0006a9-UV for categories-list@mta.ca; Fri, 29 Feb 2008 09:33:11 -0400 From: "Ronnie" To: Subject: categories: preprints available Date: Fri, 29 Feb 2008 12:12:43 -0000 MIME-Version: 1.0 Content-Type: text/plain;charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 55 The following are available from my preprint page, by me unless stated = otherwise:=20 http://www.bangor.ac.uk/~mas010/brownpr.html 1) 08.04 Exact sequences of fibrations of crossed complexes, homotopy = classification of maps, and nonabelian extensions of groups=20 ABSTRACT: The classifying space of a crossed complex generalises the = construction of Eilenberg-Mac Lane spaces. We show how the theory of = fibrations of crossed complexes allows the analysis of homotopy classes = of maps from a free crossed complex to such a classifying space. This = gives results on the homotopy classification of maps from a CW-complex = to the classifying space of a crossed module and also, more generally, = of a crossed complex whose homotopy groups vanish in dimensions between = 1 and n. The results are analogous to those for the obstruction to an = abstract kernel in group extension theory.=20 2) 06.04 R. Brown, I. Morris, J. Shrimpton and C.D. Wensley=20 Graphs of morphisms of graphs=20 ABSTRACT: This is an account for the combinatorially minded reader of = various categories of directed and undirected graphs, and their = analogies with the category of sets. As an application, the = endomorphisms of a graph are in this context not only composable, giving = a monoid structure, but also have a notion of adjacency, so that the set = of endomorphisms is both a monoid and a graph. We extend Shrimpton's = (unpublished) investigations on the morphism digraphs of reflexive = digraphs to the undirected case by using an equivalence between a = category of reflexive, undirected graphs and the category of reflexive, = directed graphs with reversal. In so doing, we emphasise a picture of = the elements of an undirected graph, as involving two types of edges = with a single vertex, namely `bands' and `loops'. Such edges are = distinguished by the behaviour of morphisms with respect to these = elements. 3) Possible connections between whiskered categories and groupoids, many = object Lie algebras, automorphism structures and local-to-global = questions=20 ABSTRACT: We define the notion of whiskered categories and groupoids and = discuss potential applications and extensions, for example to a many = object Lie theory, and to resolutions of monoids. This paper is more an = outline of a possible programme or programmes than giving conclusive = results.=20 4) A new higher homotopy groupoid: the fundamental globular = $\omega$-groupoid of a filtered space=20 MSC Classification:18D10, 18G30, 18G50, 20L05, 55N10, 55N25. KEY WORDS: filtered space, higher homotopy van Kampen theorem, cubical = singular complex, free globular groupoid ABSTRACT: We show that the graded set of filter homotopy classes rel = vertices of maps from the $n$-globe to a filtered space may be given the = structure of globular $\omega$--groupoid. The proofs use an analogous = fundamental cubical $\omega$--groupoid due to the author and Philip = Higgins. This method also relates the construction to the fundamental = crossed complex of a filtered space, and this relation allows the proof = that the crossed complex associated to the free globular = $\omega$-groupoid on one element of dimension $n$ is the fundamental = crossed complex of the $n$-globe.=20 Ronnie=20 From rrosebru@mta.ca Fri Feb 29 17:18:57 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 29 Feb 2008 17:18:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JVCW8-0006oa-H2 for categories-list@mta.ca; Fri, 29 Feb 2008 17:11:44 -0400 Date: Wed, 27 Feb 2008 08:11:02 -0500 (EST) From: Michael Barr To: Categories list Subject: categories: Backup TeX editor MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 56 [Note from moderator: Please cc: any expressions of interest to tac@mta.ca] TAC has been in existence now for 13 years. For about the first half of its existence, Bob did everything to get papers ready for publication. He did consult with me if he had particular tex problems. About when I retired, I took on the task of preparing papers (most of them) for publication. However I am uncomfortable with being the only one who really understands what is going on with tac.cls. I would like to find a volunteer to back me up, with a view to eventually taking over when the times comes, as it must, that I can no longer do the job. The job is not onerous. We get about 20 papers a year. On average, a paper takes a couple hours of preparation. Sometimes it is more, but often there is essentially no prep time since the author has used tac.cls and made no formatting errors. I am not planning on stopping this any time soon, but I think it is past time to prepare for the future. Michael From rrosebru@mta.ca Sun Mar 2 12:42:54 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 02 Mar 2008 12:42:54 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JVr2C-0002lN-Ve for categories-list@mta.ca; Sun, 02 Mar 2008 12:27:33 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Re: Backup TeX editor Date: Fri, 29 Feb 2008 22:14:46 +0000 To: Categories list Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 57 [Note from moderator: To reiterate: expressions of interest in the backup TeX editor position for TAC should be sent directly to Michael Barr, , and not to this mailing list. Thanks for those already sent. The TAC request that authors submit a single source file has nothing to do with archiving. Its purpose is to simplify slightly the editors' work.] Dear Mike, In response to your request for volunteers to take over the TeXnical management of TAC, I would certainly consider taking part in a committee to undertake this. I believe that I am qualified for the job. TeX has an error message, "Interwoven alignment preambles are not allowed", about which the TeXbook (p299) says, "If you have been so devious as to get this message, you will know what it means, and you will deserve no sympathy". I got it in about 1992, developing my diagrams package, and take it as my qualification to be a "TeXpert". There is, however, a condition, namely that TAC's use of LaTeX be brought up to date. In particular, macros should be separated in a modular fashion from mathematics. You insist on their being pasted in-line for the dubious reason of trying to archive papers as single files, whereas anybody else would use a directory (folder). Since I am making this offer in public, I would like to take the opportunity to point out to users of my diagrams package that version 3.91 has expired, and they should get a new one from www.PaulTaylor.EU/diagrams Also, even in V 3.91, the option "noPostScript" has been renamed "UglyObsolete", as a further attempt to get people to stop using the pre-1992 code that uses LaTeX-style diagonal lines. Best wishes, Paul Taylor