*mbx* 3bb593a800000022 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f72G07H31529 for categories-list; Thu, 2 Aug 2001 13:00:07 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: "Roy L. Crole" To: categories@mta.ca Subject: categories: job: 1 Year Lectureship in Mathematics: Leicester Message-Id: Date: Thu, 02 Aug 2001 10:13:25 +0100 Sender: cat-dist@mta.ca Precedence: bulk Dear Colleagues, We have a one year lectureship in mathematics which has arisen from sabbatical leave. The Department has both pure mathematicians and computer scientists who develop and apply category theory, and the position may be of interest to members of this mailing list. Yours, Roy Crole --------------------------------- Department of Mathematics & Computer Science University of Leicester England Lecturer A in Mathematics Available for 1 year from 1 September 2001 £20,066 to £23,954 pa Ref: A5449 Applicants for this fixed term lectureship should have teaching experience and be engaged in a strong research programme in some areas of Mathematics. Preference may be given to applicants whose research interests complement those of existing members of the Department. The successful applicant will contribute to the teaching of the Department, which may include the lecturing of a final year module related to differential geometry. Further details about the Department may be found at http://www.mcs.le.ac.uk. Applications close on 13 August 2001 Application forms and further particulars are available from the Personnel Office, tel 0116 252 5114, fax 0116 252 5140, jobs@le.ac.uk, http://www.le.ac.uk/personnel/jobs 2-Aug-2001 14:12:23 -0300,1026;000000000000-00000002 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f72Fx0E05090 for categories-list; Thu, 2 Aug 2001 12:59:00 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: street@hera.mpce.mq.edu.au Message-Id: Date: Thu, 2 Aug 2001 09:27:42 +1000 To: categories@mta.ca From: Ross Street Subject: categories: job: Two year position: Macquarie Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Here is the location of an ad for a 2 year Math position at Macquarie http://www.jobs.mq.edu.au/2001/Jul/19169.html [The successful applicant will be expected to start in September 2001 which makes it a bit tight, especially for overseas applicants.] Also, the ad for our Chair of Math can be found at http://www.jobs.mq.edu.au/2001/May/19139.html --Ross 2-Aug-2001 16:16:20 -0300,1096;000000000000-00000003 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f72IvEJ32385 for categories-list; Thu, 2 Aug 2001 15:57:14 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Steve Stevenson MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Message-ID: <15209.39480.137534.538379@merlin.cs.clemson.edu> Date: Thu, 2 Aug 2001 14:21:44 -0400 (EDT) To: categories@mta.ca Subject: categories: A request for two references.... X-Mailer: VM 6.72 under 21.1 (patch 11) "Carlsbad Caverns" XEmacs Lucid Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f72ILnb18999 Sender: cat-dist@mta.ca Precedence: bulk Good afternoon, I'd like references on these two subjects: 1. The relationship between categories and Martin-Löf types. 2. Any attempts to develop a computer language/system in which categories are first class citizens. Thanks in advance.... best steve 4-Aug-2001 13:53:20 -0300,1493;000000000000-00000004 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f74GNNR26074 for categories-list; Sat, 4 Aug 2001 13:23:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <001201c11b94$142a22a0$7b76e4ce@Dell> From: "Robert E. Kent" To: "Categories" References: <15209.39480.137534.538379@merlin.cs.clemson.edu> Subject: categories: Re: A request for two references.... Date: Thu, 2 Aug 2001 13:45:34 -0700 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.50.4133.2400 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 Sender: cat-dist@mta.ca Precedence: bulk ----- Original Message ----- From: "Steve Stevenson" To: Sent: Thursday, August 02, 2001 11:21 AM Subject: categories: A request for two references.... > 2. Any attempts to develop a computer language/system in which > categories are first class citizens. I do not know whether this is what you are want, but you might consider the IFF Category Theory Ontology -- part of the IFF Foundation Ontology that I am developing. This is logically coded in a new version of KIF [see http://suo.ieee.org/Kent-IFF.pdf]. Robert E. Kent rekent@ontologos.org 6-Aug-2001 10:47:12 -0300,2700;000000000000-00000005 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f76DDFP06104 for categories-list; Mon, 6 Aug 2001 10:13:15 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3B6DE53D.AA24C0D8@it.uts.edu.au> Date: Mon, 06 Aug 2001 10:30:53 +1000 From: Barry Jay X-Mailer: Mozilla 4.77 [en] (X11; U; SunOS 5.8 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: Categories Subject: categories: Re: A request for two references.... References: <15209.39480.137534.538379@merlin.cs.clemson.edu> <001201c11b94$142a22a0$7b76e4ce@Dell> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Steve Stevenson asks for > 2. Any attempts to develop a computer language/system in which > categories are first class citizens. > The constructor calculus is a variant of the lambda-calculus typed using a functorial type sytem. The functoriality is captured by a program (not a given constant) map : forall m. forall F::m->1, X::m,Y::m. P(X->Y) -> FX -> FY where F is a functor of m arguments, X and Y are m-tuples of types, P is the product functor and P(X->Y) represents an m-tuple of functions from the Xs to the Ys. The calculus supports functors for lists, all sorts of trees, vectors, matrices, trees of matrices, etc. map can be specialised to functors of one argument to get map1 : forall F::1->1, X,Y. (X->Y) -> FX -> FY or to functors of two arguments to get map2 : forall F::2->1, X0,X1,Y0,Y1. (X0->Y0) -> (X1->Y1) -> F(X0,X1) -> F(Y0,Y1) In a similar way one can define functor-polymorphic functions for folding, zipping, etc. and also for numerical operations like plus : forall X. X -> X -> X The essentials of the system were presented at Typed Lambda-Calculi and Applications in May this year (Springer LNCS 2044). A more comprehensive account is available at www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps Both accounts are written for an audience familiar with polymorphically typed lambda-calculi. An account for a general audience has yet to be written (which is why I have not already announced to this list). Let me add that we have developed a programming language FISh2 which embodies all of these ideas, and may soon be stable enough for public release. Yours, Barry Jay -- Associate Professor C.Barry Jay, Phone: (61 2) 9514 1814 Associate Dean (RPP), Faculty of IT www-staff.it.uts.edu.au/~cbj University of Technology, Sydney. CRICOS Provider 00099F 6-Aug-2001 20:30:22 -0300,1826;000000000000-00000006 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f76N4VK17881 for categories-list; Mon, 6 Aug 2001 20:04:31 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Steve Stevenson Message-ID: <15214.54024.467816.519707@merlin.cs.clemson.edu> Date: Mon, 6 Aug 2001 13:25:28 -0400 (EDT) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 To: categories@mta.ca Subject: categories: Responses to my two questions. (Revised) X-Mailer: VM 6.72 under 21.1 (patch 11) "Carlsbad Caverns" XEmacs Lucid Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f76HPWb12533 Sender: cat-dist@mta.ca Precedence: bulk Many thanks to those who responded to my questions. Here's a short summary of th replies. best, steve ------------------------------------------------------------ 1. Relationship with Martin-Löf types: a. B. Jacobs. *Categorical Logic and Type Theory*. Elsevier. 1998. b. @Article{Seely84, author = "R. A. G. Seely", title = "Locally Cartesian Closed Categories and Type Theory", journal = "Math. Proc. Cambridge Philos. Soc.", volume = "95", pages = "33--48", year = "1984", } 2. Computer systems a. FISh, http://www-staff.socs.uts.edu.au/~cbj/FISh and www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps b. IFF Foundation Ontology, http://suo.ieee.org/Kent-IFF.pdf c. David Rydeheard provided a pointer to the code for *Computational Category Theory*, http://www.cs.man.ac.uk/~david/categories/code/ d. Charity, http://www.cpsc.ucalgary.ca/projects/charity/home.html 8-Aug-2001 18:07:23 -0300,1633;000000000000-00000007 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f78KU2k08997 for categories-list; Wed, 8 Aug 2001 17:30:02 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 8 Aug 2001 15:06:31 +0200 Message-Id: <200108081306.PAA24102@fb04193.mathematik.tu-darmstadt.de> From: Martin Hofmann To: categories@mta.ca Subject: categories: charact. of absolute equalisers Sender: cat-dist@mta.ca Precedence: bulk Dear categorists, I wonder whether the following result is known: Call an equaliser in a category C *absolute* if it is preserved by all functors. Proposition: An equaliser e:A->B, u,v:B->C is absolute if and only if there are maps p:B->A, h1,h2,...hn:C->B such that pe=id, ep=h1 u h1 u = h2 v h2 u = h3 v ... hn v = id Proof: An equaliser endowed with such maps is obviously preserved by any functor since whenever we have maps e,u,v,p,h1...hn such that ue=ve together with the equations listed above then e equalises u and v. For the converse consider the functor which maps X to C(B,X)/~ where ~ is the left congruence generated by u~v, i.e., f~g iff there are h1...hn such that f=h1 u h1 v = h2 u ... hn v = g If this functor preserves the equaliser then, since Fu([id]) = Fv([id]) we obtain p:B->A such that ep~id. Thus we have maps h1..hn with the desired properties. To show pe=id we calculate as follows: epe=h1 u e = h1 v e = h2 u e = ... = hn v e = e, so pe=id since e is a mono. Best wishes, Martin Hofmann 9-Aug-2001 10:28:59 -0300,953;000000000000-00000008 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f79Cv0Y15034 for categories-list; Thu, 9 Aug 2001 09:57:00 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Wed, 8 Aug 2001 21:55:25 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: categories@mta.ca Subject: categories: Re: charact. of absolute equalisers In-Reply-To: <200108081306.PAA24102@fb04193.mathematik.tu-darmstadt.de> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Bob Pare characterized absolute coequalizers in exactly those terms (dualized, of course) in his 1969 dissertation under Lambek. 9-Aug-2001 12:43:22 -0300,2501;000000000000-00000009 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f79FFCg30856 for categories-list; Thu, 9 Aug 2001 12:15:12 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Subject: categories: Re: charact. of absolute equalisers To: categories@mta.ca Date: Thu, 9 Aug 2001 10:17:05 -0300 (ADT) In-Reply-To: <200108081306.PAA24102@fb04193.mathematik.tu-darmstadt.de> from "Martin Hofmann" at Aug 08, 2001 03:06:31 PM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20010809131705.46720665C9@chase.mathstat.dal.ca> From: pare@mscs.cs.dal.ca (Robert Pare) Sender: cat-dist@mta.ca Precedence: bulk Dear Martin, These were studied in my PhD thesis "Absoluteness Properties in Category Theory" McGill 1969. See "Absolute Coequalizers" Springer Lecture Notes 86 (1969), 132-145, and "On Absolute Colimits" J. Alg. 19 (1971) 80-95. The proof I give shows that for colimits it is sufficient to test preservation by the Yoneda functor (or all representables). So while the Yoneda embedding preserves all limits, it preserves no colimits execpt those it absolutely has to. It's interesting that you came up with the same name for them. Bob > > Dear categorists, > > I wonder whether the following result is known: > > Call an equaliser in a category C *absolute* if it is preserved by all > functors. > > Proposition: An equaliser e:A->B, u,v:B->C is absolute if and only if > there are maps p:B->A, h1,h2,...hn:C->B such that > > pe=id, > ep=h1 u > h1 u = h2 v > h2 u = h3 v > ... > hn v = id > > Proof: An equaliser endowed with such maps is obviously preserved by > any functor since whenever we have maps e,u,v,p,h1...hn such that > ue=ve together with the equations listed above then e equalises u and v. > > For the converse consider the functor which maps X to C(B,X)/~ where ~ > is the left congruence generated by u~v, i.e., f~g iff there are h1...hn > such that f=h1 u h1 v = h2 u ... hn v = g > > If this functor preserves the equaliser then, since Fu([id]) = > Fv([id]) we obtain p:B->A such that ep~id. Thus we have maps h1..hn > with the desired properties. To show pe=id we calculate as follows: > epe=h1 u e = h1 v e = h2 u e = ... = hn v e = e, so pe=id since e is a > mono. > > Best wishes, > Martin Hofmann > > 10-Aug-2001 20:51:12 -0300,1517;000000000000-0000000a Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7AN5LY32048 for categories-list; Fri, 10 Aug 2001 20:05:21 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: street@hera.mpce.mq.edu.au Message-Id: In-Reply-To: <20010809131705.46720665C9@chase.mathstat.dal.ca> References: <20010809131705.46720665C9@chase.mathstat.dal.ca> Date: Fri, 10 Aug 2001 09:58:28 +1000 To: categories@mta.ca From: Ross Street Subject: categories: Re: charact. of absolute equalisers Content-Type: text/plain; charset="iso-8859-1" ; format="flowed" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f79NwVb11010 Sender: cat-dist@mta.ca Precedence: bulk Bob Pare's answer fully answers the immediate question. Please allow me to add mention of a little observation on absolute colimits (not just coequalizers) in the context of enriched categories which appears as: Absolute colimits in enriched categories, Cahiers topologie et géométrie différentielle 24 (1983) 377- 379; MR85i:18001. It is a good opportunity for me to push the notion of weighted (or indexed) limit; see Francis Borceux's books (p. 327 of Book II) and G. Max Kelly's book (almost the central notion!). Absoluteness is nicely expressible in terms of the weight. --Ross 7-Aug-2001 10:59:59 -0300,1967;000000000000-0000000b Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f77DKTK16523 for categories-list; Tue, 7 Aug 2001 10:20:29 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200108071218.NAA03240@cuillin.dcs.ed.ac.uk> X-Mailer: exmh version 2.3.1 01/18/2001 with nmh-1.0.4 To: categories@mta.ca Subject: categories: job: Lectureship, Edinburgh University Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Tue, 07 Aug 2001 13:18:04 +0100 From: Alex Simpson Sender: cat-dist@mta.ca Precedence: bulk Lectureship, Edinburgh University, Division of Informatics We seek to appoint a Lecturer to contribute either to our research in semantics of computation or to our research in automatic verification of finite and infinite state systems, both broadly construed. Possible areas of research interest in semantics include core formalisms for computation and programming language semantics, categorical and logical models, type theory as well as newer perspectives such as formalisms for global and mobile computation. Possible areas of research in verification include automata theory, algorithms, computational logic, abstract interpretation, constraint programming and we especially welcome applicants whose contribution has also been experimental, involving case studies. The successful candidate will work in the Laboratory for Foundations of Computer Science (LFCS). For application details see http://www.jobs.ed.ac.uk/jobs/index.cfm?action=jobdet&jobid=245 The closing date is 31st August. -- Alex Simpson, LFCS, Division of Informatics, University of Edinburgh Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113 FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209 URL: http://www.dcs.ed.ac.uk/home/als 18-Aug-2001 11:08:02 -0300,697;000000000001-0000000c Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7ICeDD29607 for categories-list; Sat, 18 Aug 2001 09:40:13 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <20010818030733.59792.qmail@web12204.mail.yahoo.com> Date: Fri, 17 Aug 2001 20:07:33 -0700 (PDT) From: Galchin Vasili Subject: categories: Downloadable Topos tutorial?? To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Hello, Where can I find a Topos tutorial online? Regards, Bill Halchin 18-Aug-2001 11:08:07 -0300,3833;000000000000-0000000d Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7ICjGm20592 for categories-list; Sat, 18 Aug 2001 09:45:16 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 17 Aug 2001 15:26:44 +0100 (BST) From: mpc02 To: categories@mta.ca Subject: categories: cfp: Mathematics of Program Construction Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk [Apologies for multiple copies] MPC 2002 6th International Conference on MATHEMATICS OF PROGRAM CONSTRUCTION ----------------------------------- http://www.cs.ukc.ac.uk/conf/mpc2002/ Organised in conjunction with WCGP '02 8--10 July, 2002 Dagstuhl, Germany CALL FOR PAPERS This conference aims to promote the development of mathematical principles and techniques that are demonstrably useful and usable in the process of constructing computer programs (whether implemented in hardware or software). The focus of the conference is on techniques that combine precision with conciseness, enabling programs to be constructed by formal calculation. Within this theme, the scope of the conference is very diverse. We welcome contributions to programming methodology (for example, formal methods for program specification and transformation), to programming paradigms (for example, generic programming techniques and type systems) and to language design (for example, programming calculi and programming language semantics). Theoretical contributions are welcome provided their relevance to program construction is evident; discussion of applications is welcome provided the mathematical basis is evident. The conference will be organised in conjunction with the IFIP TC2 Working Conference on Generic Programming, WCGP '02. There will also be a number of co-located workshops, including CMPP. IMPORTANT DATES Deadline for submission of papers: 6th January, 2002 Notification of acceptance/rejection: 4th March, 2002 Final papers due: 25th April, 2002 Full papers should be submitted in Postscript or pdf format by e-mail to mpc02@ukc.ac.uk by 6th January, 2002. PROGRAMME COMMITTEE Roland Backhouse (UK) Eerke Boiten (UK, co-chair) Michael Butler (UK) Ernie Cohen (USA) Jules Desharnais (Canada) Jeremy Gibbons (UK, GP liaison) David Gries (USA) Lindsay Groves (New Zealand) Ian Hayes (Australia) Eric Hehner (Canada) Zhenjiang Hu (Japan) John Hughes (Sweden) Bart Jacobs (The Netherlands) Johan Jeuring (The Netherlands, GP liaison) Dick Kieburtz (USA) Dexter Kozen (USA) K. Rustan M. Leino (USA) Christian Lengauer (Germany, CMPP liaison) Erik Meijer (The Netherlands/USA) Bernhard Moeller (Germany, co-chair) David Naumann (USA) J.N. Oliveira (Portugal) Alberto Pardo (Uruguay) Peter Pepper (Germany) Kaisa Sere (Finland) Mark Utting (New Zealand) FURTHER INFORMATION Please refer to the web page for further details. http://www.cs.ukc.ac.uk/conf/mpc2002/ -- Mathematics of Program Construction '02 at Dagstuhl Eerke Boiten, Computing Laboratory, University of Kent at Canterbury, UK +44.1227.827615 (fax 762811) 18-Aug-2001 13:28:18 -0300,1029;000000000001-0000000e Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7IFHXR01271 for categories-list; Sat, 18 Aug 2001 12:17:33 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Sat, 18 Aug 2001 09:33:43 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: categories@mta.ca Subject: categories: Re: Downloadable Topos tutorial?? In-Reply-To: <20010818030733.59792.qmail@web12204.mail.yahoo.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Why don't you try downloading ttt from ftp.math.mcgill.ca/pub/barr ? On Fri, 17 Aug 2001, Galchin Vasili wrote: > Hello, > > Where can I find a Topos tutorial online? > > Regards, Bill Halchin > > 20-Aug-2001 10:25:39 -0300,1552;000000000000-0000000f Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7KCndT08586 for categories-list; Mon, 20 Aug 2001 09:49:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 20 Aug 2001 12:29:29 +0200 From: Frank Atanassow To: Galchin Vasili Cc: categories@mta.ca Subject: categories: Re: Downloadable Topos tutorial?? Message-ID: <20010820122929.A2483@cs.uu.nl> References: <20010818030733.59792.qmail@web12204.mail.yahoo.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i In-Reply-To: <20010818030733.59792.qmail@web12204.mail.yahoo.com>; from vngalchin@yahoo.com on Fri, Aug 17, 2001 at 08:07:33PM -0700 Sender: cat-dist@mta.ca Precedence: bulk Galchin Vasili wrote (on 17-08-01 20:07 -0700): > Where can I find a Topos tutorial online? Another source, more oriented towards computer scientists: Phoa, Wesley, An introduction to fibrations, topos theory, the effective topos and modest sets, 1993, (howpublished=) Available by anonymous FTP from {\tt maths.su.oz.au} in the directory {\tt sydcat/papers/phoa}. It is the file {\tt tech.ps.Z}., (author_acronym=) PhoaW, , , (title_acronym=) intftt. -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379 20-Aug-2001 10:26:23 -0300,1705;000000000000-00000010 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7KCqZI02341 for categories-list; Mon, 20 Aug 2001 09:52:35 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <20010819000915.87760.qmail@web12205.mail.yahoo.com> Date: Sat, 18 Aug 2001 17:09:15 -0700 (PDT) From: Galchin Vasili Subject: categories: Subclassifier object question To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Hello, First of all sorry for the beginner's question. I have been reading various sources about the notion of a subobject classifier, e.g. McClarty's book, Lawvevre's book. Let assume the following situation: 1) Has a subobject classifier, true : 1 ---------> Omega. 2) Have an object X and object A and a monomorphism subX: A------->X. 3) With 2), we will have the pullback diagram with the corners of the pullback being the subobject classifier and the unqiue classifier/classifier X------>Omega 4)We have either a element, el: 1------>X or a generalized el: element H------->X. Question: Let's assume for simplicity that our category is Set. The problem is I don't understand how the notion of a subobject classifier determines whether "el" does or does not belong to the aforementioned subobject, "subX"! (I know that the outer commuting square figures in this, but it seems like every element will be "classified" as belonging to "subX"). Thanks and regards, Bill Halchin 20-Aug-2001 18:17:23 -0300,1833;000000000000-00000011 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7KKrGv09360 for categories-list; Mon, 20 Aug 2001 17:53:16 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: Re: Subclassifier object question Message-Id: From: Paul Taylor Date: Mon, 20 Aug 2001 14:29:17 +0100 X-Ident: pt Sender: cat-dist@mta.ca Precedence: bulk Bill Halchin asks > I don't understand how the notion of a subobject classifier > determines whether "el" does or does not belong to the subobject U ----------> 1 V _| | | | true | | V chi V X --------> Omega If any element "belongs to U" in the arrows sense that it factors through U, ie there is a map from 1 (or somewhere) to U, then the composite with chi:X->Omega is equal to (the composite with) true. Conversely, if an element of X "belongs to U" in the logical sense that its composite with chi is equal to (the composite with)true, then we have a commutative square that can be compared to the pullback. For more about the logical consequences of this property of Omega, and in particular the mysterious formula a & F(a) = a & F(true) see "Geometric and Higher Order Logic ..." in TAC, v7 (2000) pp 284--338. For a presentation of set theory (or, as I call it, Zermelo type theory) in a form that is both the way that ordinary mathematicians use it, and directly related to the topos-theoretic way of saying things, see Section 2.2 of my book "Practical Foundations of Mathematics". Both accessible via my home page at http://www.dcs.qmw.ac.uk/~pt Paul 20-Aug-2001 18:17:29 -0300,5651;000000000000-00000012 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7KKqF203088 for categories-list; Mon, 20 Aug 2001 17:52:15 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200108202001.NAA00544@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: Subclassifier object question In-Reply-To: Message from Galchin Vasili of "Sat, 18 Aug 2001 17:09:15 PDT." <20010819000915.87760.qmail@web12205.mail.yahoo.com> Date: Mon, 20 Aug 2001 13:01:52 -0700 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk The direct answer to Bill Halchin's concern (`it seems like every element will be "classified" as belonging to "subX"') is that this is the defining characteristic of subX: subX consists of those elements of X that belong to subX. That is, every element of subX has to be classified as belonging to subX. The triviality of this answer suggests that Bill's real question is, how does the pullback f Y ----> X | | !| |g | | v z v 1 ----> Z in the definition of topos work in the case of sets? Here's one answer. The basic idea is that there are two equally good ways of defining a subset of a set X, in terms of functions respectively to and from X. TO: A function f:Y->X has an image f(Y), a subset of X. FROM: A function g:X->Z has an inverse image g^-1({z}) of any given element z of Z, also a subset of X. Every subset of X arises in both ways (provided in the latter case that Z has at least two elements). With a little care it can be made to arise in a canonical way in both cases, and moreover such that these two ways are paired up according to the subset they each determine. TO: Now there are many functions to X with the same image. However any two _injections_ i:Y->X, i':Y'->X have the same image if and only if there is a bijection j:Y->Y' for which the evident triangle commutes, namely i'j = i. Call two such injections isomorphic. The isomorphism classes of injections to X are then in bijection with the subsets of X. FROM: Even if we hold Z and an element z thereof fixed there may still be many functions g:X->Z with the same inverse image g^-1({z}). This happens for |Z| >= 3, where two g's can agree on the members of a subset yet disagree about which of the non-z elements of Z to send the nonmembers to. On the other side, if Z is a singleton we lose the proper subsets of X, and if Z is empty we lose all subsets. We are now in a position to analyze the subobject classifier condition, which can be stated for sets as follows. For every injection i:Y->X there exists a unique g:X->Z making the above square a pullback. Existence and uniqueness each appear twice in this condition, once explicitly, and once implicitly in the notion of pullback. For the former, the existence requirement ensures that Z has enough elements to permit it to classify at all, while uniqueness prevents it from having too many, avoiding ``overclassification.'' Thus |Z|=2 is the only possible choice for a subobject classifier, i.e. Z (along with its element z) is determined up to isomorphism. For the latter, the uniqueness requirement in the definition of pullback ensures that i is an injection, and existence makes it the the maximal injection into X for which g(i(y)) = z for all y in Y. Note furthermore that g uniquely determines i up to isomorphism, i.e. the property of being a pullback ensures that for each g there exists a unique i up to isomorphism, giving us the other direction of our desired bijection. Although everything said above has been for Set, it can be lifted (with the necessary care) to any cartesian closed category with the obvious generalizations of set to object, function to morphism, injection to monic, and element to morphism-from-1. What does not lift are properties of the topos Set not common to all toposes, such as that Set has a natural numbers object {0,1,2,...}, and is a Boolean topos (the logic of set membership is Boolean). An example of a topos with no natural numbers object is furnished by the subtopos of Set consisting just of its finite sets. The argument that Set is a topos shows with almost no modification (and in particular with the same subobject classifier) that this evidently cartesian closed subcategory is itself a topos. An example of a non-Boolean topos is furnished by the cartesian closed category of directed graphs made a topos by taking Z to be the 2-clique (two vertices and four edges) with one of its self-loops duplicated and the duplicate taken as z (the elements of a directed graph being its self-loops). A CCC can be made a topos in at most one way up to isomorphism of its subobject classifier, so (given that this choice works), this strange graph is it for this topos. One quick way to see that this is a topos is to present it as the presheaf category Set^C where C is the category E=>V with two objects E,V and two morphisms s,t:E->V. A graph is a functor from C to Set; it assigns sets to E and V (respectively the set of edges and the set of vertices), and functions to s and t, respectively the source and target functions specifying the two vertices the edges run between. The relevant theorem here is that the functor category Set^C is a topos for any small category C. For C = E=>V the theorem automatically constructs the above strange graph. Vaughan Pratt 20-Aug-2001 18:17:37 -0300,987;000000000000-00000013 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7KKs4s27303 for categories-list; Mon, 20 Aug 2001 17:54:04 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 20 Aug 2001 11:53:33 -0300 (ADT) Message-Id: <200108201453.f7KErXb28690@mailserv.mta.ca> From: peter_easthope@gulfnet.sd64.bc.ca X-Mailer: Oberon Mail (ejz) on PC Native 08.12.2000 To: Cc: Subject: categories: sum of pointed sets. Sender: cat-dist@mta.ca Precedence: bulk Hypothesis: the sum of an m-pointed set and an n-pointed set is an m+n-pointed set. Is this true? I've not thought of a counterexample. If this is a theorem, can anyone tell me where to find a proof. Such a proof, presented by a professional mathematician, would be interesting and instructive. Thanks, peter_easthope@gulfnet.sd64.bc.ca 21-Aug-2001 10:16:08 -0300,1831;000000000000-00000014 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7LCeeQ27545 for categories-list; Tue, 21 Aug 2001 09:40:40 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 21 Aug 2001 13:53:16 +0200 From: Frank Atanassow To: categories@mta.ca Subject: categories: Re: Downloadable Topos tutorial?? Message-ID: <20010821135316.A2984@cs.uu.nl> References: <20010818030733.59792.qmail@web12204.mail.yahoo.com> <20010820122929.A2483@cs.uu.nl> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i In-Reply-To: <20010820122929.A2483@cs.uu.nl>; from franka@cs.uu.nl on Mon, Aug 20, 2001 at 12:29:29PM +0200 Sender: cat-dist@mta.ca Precedence: bulk Frank Atanassow wrote (on 20-08-01 12:29 +0200): > Galchin Vasili wrote (on 17-08-01 20:07 -0700): > > Where can I find a Topos tutorial online? > > Another source, more oriented towards computer scientists: > > Phoa, Wesley, An introduction to fibrations, topos theory, the effective > topos and modest sets, 1993, (howpublished=) Available by anonymous FTP > from {\tt maths.su.oz.au} in the directory {\tt sydcat/papers/phoa}. It is > the file {\tt tech.ps.Z}., (author_acronym=) PhoaW, , , (title_acronym=) > intftt. It turns out the location given above is out of date. Try this: http://www.margaretmorgan.com/wesley/ecs-lfcs-92-208.ps or follow the link named "Lecture Notes on the Effective Topos" at: http://www.margaretmorgan.com/wesley/ -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379 21-Aug-2001 10:16:08 -0300,10187;000000000000-00000015 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7LCmHe03809 for categories-list; Tue, 21 Aug 2001 09:48:17 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: paonico@primus.ca@pop.primus.ca (Unverified) Message-Id: Date: Tue, 21 Aug 2001 00:32:59 -0400 To: categories@mta.ca From: Nicola Santoro Subject: categories: TCS 2002 - Preliminary Call for Papers Content-Type: text/plain; charset="iso-8859-1" ; format="flowed" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f7L4Ysb21033 Sender: cat-dist@mta.ca Precedence: bulk ----------------------------------------------------------------- PRELIMINARY CALL FOR PAPERS ----------------------------------------------------------------- 2nd IFIP International Conference on THEORETICAL COMPUTER SCIENCE (TCS 2002) Montreal, August 25-30, 2002 co-sponsored by EATCS and ACM Sigact ----------------------------------------------------------------- Special Focus: Foundations of IT in the Era of Network and Mobile Computing ------------------------------------------------------- In recent years, IT application scenarios have evolved in very innovative ways. Highly distributed networks have now become a common platform for large-scale distributed programming, high bandwidth communications are cheap and widespread, and most of our work tools are equipped with processors enabling us to perform a multitude of tasks. In addition, mobile computing (referring not only to wireless devices and dynamically configured systems, but also and especially to mobile agents and robots) has made it possible to exploit interaction in novel ways. To harness the flexibility and power of these rapidly evolving, interactive systems, we need to come up with radically new foundational ideas and principles. Now is the time to develop the theoretical foundations required to design these systems. Our computational goal is to discover techniques, models and algorithms allowing us to construct systems that are flexible, dependable, secure, robust and efficient. The prime focus is how to control and coordinate the entities in the system. Cost and performance measures must account for the integration of communication and computing, as well as the natural interplay between structural information and complexity. In terms of programming paradigms, mechanisms are required to support mobility of code and computations, as well as effective infrastructures to support coordination and control of dynamically loaded software modules. Furthermore, a semantic and logic framework to formalize Internet computations is clearly required as well. Crucial issues in the development of Internet applications involve the control of component interactions, since some components can be dynamically downloaded from the network. Security architectures an monitor the execution of mobile code to protect a host from external attacks on private information. ------------------------------------------------------------------- Original and significant contributions on these issues, as well on foundational questions are sought from all areas of theoretical computer science. TCS 2002 will be composed of two interrelated tracks: Track 1 - Algorithms, Complexity and Models of Computation Track 2 - Logic, Semantics, Specification and Verification. A submission should include the track name, the title of the paper, names and affiliations of authors, an abstract up to 300 words, and the contact author's name, address, phone number, fax number, and email address. The submission must be in English, and it should provide a summary of the main results and their details to allow the program committee to assess their merits and significance, including references and comparisons. The result of the paper must be unpublished and not submitted for publication elsewhere, including journals and the proceedings of other symposia or workshops. One author of each accepted paper should be able to present it at the conference. The Proceedings will be published by Kluwer, the official publisher of IFIP. More details on the submission procedure will appear in the forthcoming First CFP and on the Confrence web site. Important Dates: December 3, 2001: Deadline for submission of papers February 20, 2002: Notification of acceptance ----------------------------------------------------------------- Conference Chair ---------------- Nicola Santoro, Carleton University (santoro@scs.carleton.ca) Conference Vice-Chairs ---------------------- Track (1) Ricardo Baeza-Yates, University of Chile (rbaeza@dcc.uchile.cl) Track (2) Ugo Montanari, University of Pisa, Italy (ugo@di.unipi.it) Program Committee ----------------- Track (1) Eric Allender (allender@aramis.rutgers.edu) JosÈ Balcazar (balqui@lsi.upc.es) Andrej Brodnik (Andrej.Brodnik@IMFM.Uni-Lj.SI) Volker Diekert (diekert@informatik.uni-stuttgart.de) David Fernandez-Baca (fernande@cs.iastate.edu) Kazuo Iwama (iwama@i.kyoto-u.ac.jp) John D. Kececioglu (kece@CS.Arizona.EDU) Jan van Leeuwen (jan@cs.uu.nl) Xuemin Lin (lxue@cse.unsw.EDU.AU) Alberto Marchetti Spaccamela (alberto@dis.uniroma1.it) David Peleg (peleg@wisdom.weizmann.ac.il) Prabhakar Raghavan (pragh@verity.com) Venkatesh Raman (vraman@imsc.ernet.in) Siang Song (song@ime.usp.br) Paul Spirakis (spirakis@cti.gr) Luca Trevisan (luca@eecs.berkeley.edu) Brigitte VallËe (Brigitte.Vallee@info.unicaen.fr) Alfredo Viola (viola@fing.edu.uy) Manfred Warmuth (manfred@cse.ucsc.edu) Sue Whitesides (sue@cs.mcgill.ca) Peter Widmayer (widmayer@inf.ethz.ch) Jiri Wiederman (wieder@uivt.cas.cz) Track (2) Gabriel Baum (gbaum@info.unlp.edu.ar) Luca Cardelli (luca@microsoft.com) Frank DeBoer (frankb@cs.ruu.nl) Ursula Goltz (u.goltz@tu-bs.de) Roberto Gorrieri (gorrieri@cs.unibo.it) Jieh Hsiang (hsiang@csie.ntu.edu.tw) Takayasu Ito (ito@ito.ecei.tohoku.ac.jp) Alexander Letichevsky (letichev@carrier.kiev.ua) Jean-Jacques Levy (Jean-Jacques.Levy@inria.fr) Huimin Lin (lhm@ox.ios.ac.cn) Kim Marriott (marriott@csse.monash.edu.au) Narciso Marti-Oliet (narciso@eucmos.sim.ucm.es) John Mitchell (mitchell@cs.stanford.edu) Luis Monteiro (lm@fct.unl.pt) Peter Mosses (pdmosses@daimi.aau.dk) Prakash Panangaden (prakash@cs.mcgill.ca) Benjamin Pierce (bcpierce@cis.upenn.edu) Amir Pnueli (amir@wisdom.weizmann.ac.il) Leila Ribeiro (leila@inf.ufrgs.br) Gheorghe Stefanescu (ghstef@funinf.math.unibuc.ro) Andrzej Tarlecki (tarlecki@mimuw.edu.pl) Thiagu Thiagarajan (pst@smi.ernet.in) Organizing Committee -------------------- Amiya Nayak (nayak@nortelnetworks.com) Giuseppe Prencipe (prencipe@di.unipi.it) Web Site -------- http://www.scs.carleton.ca/~santoro/TCS2002/indexTCS2002.html Sponsors -------- The IFIP TCS2002 conference is sponsored by -- IFIP TC1 (Technical Committee on Foundations of Computer Science) in cooperation with -- EATCS (European Association for Theoretical Computer Science) -- ACM SIGACT (Special Interest Group on Algorithm and Computation Theory) IFIP TC1 Steering Committee --------------------------- Giorgio Ausiello (U. of Roma "La Sapienza", Italy) - CHAIR - Wilfried Brauer (TU Munchen, Germany) Takayasu Ito (Tohoku University, Japan) Michael O. Rabin (Harvard University, USA) Joseph Traub (Columbia University, USA) The first IFIP TCS was held in Sendai, Japan, in 2000 (http://hagi.is.s.u-tokyo.ac.jp/tcs2000/). TCS2002 will be held as part of the 17th IFIP World Computer Congress (http://www.wcc2002.org/en/index.html). List of Areas -------------- Track (1): Algorithms, Complexity and Models of Computation Analysis and design of algorithms Automata and formal languages Cellular automata and systems Combinatorial, graph and optimization algorithms Computational and mathematical finance Computational learning theory Continuous algorithms and complexity Computational complexity Computational geometry Cryptography Distributed computing Descriptional complexity Evolutionary and genetic computing Experimental algorithms Mobile computing Molecular computing and algorithmic aspects of bioinformatics Network computing Neural computing Parallel and distributed algorithms Probabilistic and randomized algorithms Quantum computing Structural information and communication complexity Track (2): Logic, Semantics, Specification and Verification Bridging semantics and complexity Concurrency theory Constructive and non-standard logics in computer science Foundations of global computing Foundations of mobile computing Foundations of security Foundations of system specification Foundations of wide area programming Logic and semantics for programs and languages Logic, specification and verification of hybrid and real-time systems Proofs and specifications in computer science Term rewriting systems Theoretical aspects of software concepts Theoretical aspects of specification, and verification of hardware and software Theoretical foundations of databases Theoretical foundations of open systems Theory of Internet languages and systems Theory of parallel and distributed systems Type and category theory in computer science -------------------------------------------------------------------------------- 23-Aug-2001 07:47:12 -0300,6657;000000000000-00000016 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7N9wZJ18597 for categories-list; Thu, 23 Aug 2001 06:58:35 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200108211537.f7LFb7W02947@pandora.cs.kun.nl> X-Mailer: exmh version 2.1.1 10/15/1999 To: categories@mta.ca Subject: categories: FMOODS 2002 -- final call; submission deadline: 2 sept. Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Tue, 21 Aug 2001 17:35:17 +0200 From: Bart Jacobs Sender: cat-dist@mta.ca Precedence: bulk [[ -- Apologies for multiple copies of this message -- ]] Final Call for Papers Fifth IFIP International Conference on Formal Methods for Open Object-based Distributed Systems FMOODS'2002 20-22 March 2002, University of Twente, the Netherlands http://trese.cs.utwente.nl/fmoods2002/ fmoods@cs.utwente.nl ------------------------------------------------------------------------ Objectives ========== Object-based Distributed Computing is being established as the most pertinent basis for the support of large, heterogeneous computing and telecommunication systems. Indeed, several important international organisations, such as ITU, ISO, OMG, TINA-C, etc. are defining similar distributed object-based frameworks as a foundation for open distributed computing. The advent of Open Object-based Distributed Systems - OODS - brings new challenges and opportunities for the use and development of formal methods. New architectures and system models are emerging (e.g., the enterprise, information, computational and engineering viewpoints of the ITU-T/ISO/IEC ODP Reference Model) which require formal notational support. Usual design issues such as specification, verification, refinement, and testing need to take into account new dimensions introduced by distribution and openness, such as quality of service and dependability constraints, dynamic binding and reconfiguration, consistency between multiple models and viewpoints, security etc. OODS is a challenging research context and a source of motivation for semantical models of object-based systems and notations, for the evolution of standardised formal description techniques, for the application and assessment of logic based approaches, for better understanding and information modeling of business requirements, and for the further development and use of Object Oriented methodologies and tools. The objective of FMOODS is to provide an integrated forum for the presentation of research in several related fields, and the exchange of ideas and experiences in the topics concerned with the formal methods support for Open Object-based Distributed Systems. Topics ====== Topics of interest include but are not limited to: * Formal models for object-based distributed computing * Specification and analysis techniques for distributed systems * Refinement and transformation of specifications * Verification, testing and validation of distributed systems * Semantics of object-based programming languages * Object-based coordination languages * Multiple viewpoint modelling and consistency between different models * Types, service types and subtyping * Quality of service: specification, verification and testing of constraints * Formal support for object life cycles * Design and software life-cycle of object-based distributed applications * Formal models for measuring the quality of object-oriented requirement or design specifications * Formal aspects of distributed real-time multimedia systems * Applications to telecommunications and related areas * Formal and rigorous specifications of business enterprises * Analysing interactions between objects / components * Formal models for security in distributed systems Conference Organizers ===================== Contact: fmoods@cs.utwente.nl Arend Rensink (general chair + local organizer) University of Twente, the Netherlands Bart Jacobs (Pc chair) University of Nijmegen, the Netherlands Invited Speakers ================ Carolyn Talcott (Stanford University, USA): "Reasoning about Distributed Middleware Services" Matthew Dwyer (Kansas State University) title to be announced Steve Schneider (University of London): "Verifying Security Protocols" Program Committee ================= Lynne Blair (U. Lancaster, UK) John Derrick (UKC, Kent, UK) Alessandro Fantechi (U. Firenze, Italy) Riccardo Focardi (U. Venice, Italy) Andrew D. Gordon (Microsoft Research, UK) Rolf Hennicker (LMU Muenchen, Germany) Bart Jacobs (U. Nijmegen, the Netherlands) Guy Leduc (U. of Liege, Belgium) Elie Najm (ENST, Paris, France) Uwe Nestmann (EPFL Lausanne) Arnd Poetzsch-Heffter (FernUniv. Hagen, Germany) Arend Rensink (U. Twente, the Netherlands) Scott Smith (Johns Hopkins Univ., USA) Perdita Stevens (U. Edinburgh) Carolyn Talcott (Stanford Univ., USA) Nalini Venkatasubramanian (UC Irvine, USA) Evaluation and Publication of Submitted Papers ============================================== Submitted manuscripts will be evaluated and selected for presentation in the conference. The proceedings of FMOODS 2002 will be published by Kluwer who are the publishers of IFIP events. The proceedings will be made available at the conference. Instructions to the Authors =========================== Authors are invited to submit full original research papers, up to 16 pages (including bibliography), 12 point, single spaced, including an informative abstract, names and affiliations of all authors, and a list of keywords facilitating the assignment of papers to referees. The use of the Kluwer styles (http://www.wkap.com/ifip/styles) and guidelines (http://www.wkap.com/ifip/guidelines.pdf) for the submission is recommended. Important Dates =============== 2 Sept 2001 Submission deadline 15 Nov 2001 Notification of acceptance 15 Dec 2001 Camera ready copy for participants proceedings due 20-22 March 2002 The conference at Univ. Twente Submission Procedure Information: at the conference website: http://trese.cs.utwente.nl/fmoods2002/ 24-Aug-2001 10:43:41 -0300,2060;000000000000-00000017 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7ODA8O29017 for categories-list; Fri, 24 Aug 2001 10:10:08 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 23 Aug 2001 14:40:00 +0200 From: Frank Atanassow To: categories@mta.ca Subject: categories: "catamorphism" Message-ID: <20010823144000.A3979@cs.uu.nl> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i Sender: cat-dist@mta.ca Precedence: bulk What is the definition/scope of the term "catamorphism"? In the calculational school of programming, I think people agree that: For every F-algebra A, the unique F-homomorphism from an initial F-algebra to A is a catamorphism. but: Is the converse true also, or is `catamorphism' more general: "a catamorphism is the unique arrow from an initial _object_ (in any category, not just categories of algebras)." I think the answer to that question is no, but is there a snappy name for such arrows? What about the universal arrows in the free algebra construction? Are those `catamorphisms' or not? If not, is there a name for those arrows? and furthermore: In the case of initial F-algebras, for F an endofunctor on category C, is the catamorphism the arrow in the category of F-algebras, or the corresponding one in C? In other words, is `catamorphism' a property of the arrow or the arrow + the category? If you compare with `monomorphism', since we speak of being `monic _in_ C', I presume the latter, and thus only one arrow would be `catamorphic', but which? Judging from the literature, I am inclined to say that the arrow in C is the catamorphism, but I would like a second opinion. -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379 24-Aug-2001 12:14:45 -0300,2712;000000000000-00000018 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7OEpYq14953 for categories-list; Fri, 24 Aug 2001 11:51:34 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 24 Aug 2001 15:16:26 +0100 (BST) Message-Id: <200108241416.PAA08662@loire.comlab> From: Jeremy Gibbons To: categories@mta.ca In-reply-to: <20010823144000.A3979@cs.uu.nl> (message from Frank Atanassow on Thu, 23 Aug 2001 14:40:00 +0200) Subject: categories: Re: "catamorphism" References: <20010823144000.A3979@cs.uu.nl> Sender: cat-dist@mta.ca Precedence: bulk > In the calculational school of programming, I think people agree that: > > For every F-algebra A, the unique F-homomorphism from an initial F-algebra to > A is a catamorphism. > > but: > > Is the converse true also, or is `catamorphism' more general: "a > catamorphism is the unique arrow from an initial _object_ (in any category, > not just categories of algebras)." I think the answer to that question is > no, but is there a snappy name for such arrows? Erik Meijer coined the name "catamorphism". According to him, the name was chosen because the Greek prefix "cata" means "downwards"; a catamorphism destructs a data structure like a list. (For example, "sum" destructs a list of numbers, yielding a number.) So I would agree with you. For example, in Set, the unique arrow from the initial object (the empty set) to any other object does not "destruct", so should not be called a catamorphism. > In the case of initial F-algebras, for F an endofunctor on category C, is the > catamorphism the arrow in the category of F-algebras, or the corresponding > one in C? In other words, is `catamorphism' a property of the arrow or the > arrow + the category? If you compare with `monomorphism', since we speak of > being `monic _in_ C', I presume the latter, and thus only one arrow would be > `catamorphic', but which? Judging from the literature, I am inclined to > say that the arrow in C is the catamorphism, but I would like a second > opinion. It is the arrow in C. In programming terms, it is the program itself (eg "sum") that destructs; the arrow in the category of F-algebras is merely an artifact of the categorical way of modelling such programs. IMHO. Jeremy -- Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html 24-Aug-2001 12:14:59 -0300,12425;000000000000-00000019 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7OErN525388 for categories-list; Fri, 24 Aug 2001 11:53:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Server: Advanced Direct Remailer v2.1 Date: Fri, 24 Aug 2001 16:06:52 +0200 From: MKM2001 X-Mailer: The Bat! (v1.53d) Reply-To: MKM2001 Organization: Risc Linz X-Priority: 3 (Normal) Message-ID: <367477116.20010824160652@risc.uni-linz.ac.at> To: categories@mta.ca Subject: categories: MKM 2001 Program MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk ------------------------------------------------------------------------ [Apologies for multiple copies] ------------------------------------------------------------------------ CALL FOR PARTICIPATION ------------------------------------------------------------------------ ========================================================================= MKM 2001 First International Workshop on Mathematical Knowledge Management & OpenMath Workshop RISC, A-4232 Schloss Hagenberg, September 24-26, 2001 http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/ ========================================================================= Mathematical Knowledge Management is an exciting new field in the intersection of mathematics and computer science. We need efficient, new techniques - based on sophisticated formal mathematics and software technology - for taking fruit of the enormous knowledge available in current mathematical sources and for organizing mathematical knowledge in a new way. The Workshop should bring together math researchers, software developers, publishing companies, librarians, math societies, and teachers for exchanging their views and approaches and for pushing the field. Whereas the workshop is designed to provide a forum for discussion and presentation of early ideas, the special issue is a forum for polished, refereed papers in the area of mathematical knowledge management. Participation and presentation of talks and papers is possible in both the workshop and the special issue, jointly or independently. ========================================================================= +----------------------+ | MKM 2001 - Program | +----------------------+ +--- Monday, September 24 ---+ 8:30- 9:00 registration 9:00- 9:15 welcome 9:15-10:00 William M. Farmer A Formal Framework for (invited talk) Managing Mathematics 10:00-10:30 break 10:30-11:00 Till Mossakowski Heterogeneous Logics for Mathematical Knowledge Representation 11:00-11:30 Michael Kohlhase Using Logic Morphisms for Language Independence in Mathematical Knowledge Bases 11:30-12:00 Jim Caldwell, Stuart Interactive Digital Libraries Allen, Bob Costable of Formalized Algorithmic Knowledge 12:00-12:30 Christoph Designing Mathematical Schwarzweller Libraries Based on Minimal Requirements for Theorems 12:30-14:00 lunch 14:00-14:30 Piotr Rudnicki, Mathematical Knowledge Andrzej Trybulec Management in Mizar 14:30-15:00 Adam Grabowski Robbins Algebra vs. Boolean Algebras 15:00-15:30 Andrea Asperti Mathematical Knowledge Management in HELM 15:30-16:00 break 16:00-16:30 Peter Baumgartner Automated Deduction Techniques for the Management of Personalized Documents 16:30-17:00 Cristoph Benzmueller Using a Blackboard Architecture for Assertion Application in Proof Planning 17:00-17:30 Manasi Athale, Exchange of Mathematical Rahul Athale Information in the Web: Present and Future +--- Tuesday, September 25 ---+ 9:00- 9:45 Gerhard O. Michler A Prototype of a Linked, (invited talk) Searchable Digital Mathematical Library 9:45-10:15 break 10:15-10:45 Therese Hardin Mathematical Knowledge Management in Foc 10:45-11:15 Carlo Traverso Managing Concrete Knowledge in Commutative Algebra 11:15-11:45 Bruno Buchberger Mathematical Knowledge Management Using Theorema 11:45-12:15 Koji Nakagawa The Role of Logicographic Symbols for Mathematical Knowledge Management 12:15-13:45 lunch 13:45-14:15 Ludovic Meunier, Automatically Generated Bruno Salvy Encyclopedia of Special Functions 14:15-14:45 Andrew Adams Using Real Number Theorem Proving to Support Maths Table 14:45-15:15 Paul Cairns, On Dynamically Presenting a Gow Jeremy Topology Course 15:15-15:45 break 15:45-16:15 Jonathan Borwein, The Work of the CEIC Martin Gr?tschel 16:15-16:45 Wolfram Sperber, Mathematical Knowledge Roland Schwaernzl Management and Math-Net: Semantics, Visualization and Internationalization of Math-Net 16:45-17:15 Terry Stanway Changing Needs and Expectations in Mathematical Knowledge Management: from GHH and Littlewood to XML and Maple 20:00 Workshop Dinner +--- Wednesday, September 26 ---+ Joint Program with the OpenMath Workshop 9:00- 9:45 Stephen Watt Title to be announced (invited talk) 9:45-10:15 break 10:15-10:45 Martijn Oostdijk, Certified and Portable Olga Caprotti, Mathematical Documents from Herman Geuvers Formal Contexts 10:45-11:15 James H. Davenport Mathematical Knowledge Representation 11:15-11:45 William Arthur Naylor Meta Style Sheets for the Conversion of Mathematical Documents into other Forms 11:45-12:15 Mike Dewar, Mathematical Software: D. Carlisle the Next Generation? 12:15-13:45 lunch 13:45-14:00 G. Stork European Funding Possibilities 14:00-14:45 Daniel Loizier The NIST Digital Library of (invited talk) Mathematical Functions Project 14:45-15:15 Bruce Miller Technical Aspects of the Digital Library of Mathematical Functions: Dreams and Realities 15:15-15:45 break 15:45-16:15 Giovanna Albano, G. Modelling for Understanding of Gargiulo, S. Salerno Scientific Knowledge 16:15-16:45 Rudolf Wille Conceptual Knowledge Systems for Mathematics 16:45-17:15 Francky Trichet Contribution of the Ontology Engineering to Mathematical Knowledge Management 17:15-18:00 Panel discussion ------------------------------------------------------------------------------ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- ------------------------------------------------------------------------------ General Information and Registration at http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/general_information.html http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/registration.html Early Registration deadline is August 31, 2001. ------------------------------------------------------------------------------ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- ------------------------------------------------------------------------------ Workshop Organizers: Bruno Buchberger (General Chair) Olga Caprotti (Managing Chair) International Program Committee: Andrea Asperti (University of Bologna, Italy) Jonathan Borwein (Simon Fraser University, Burnaby, Canada) Bruno Buchberger (RISC-Linz, Austria) Alan Bundy (University of Edinburgh, Scotland) Ingo Dahn (University of Koblenz, Germany) James Davenport (University of Bath, UK) Gaston Gonnet (ETH Z?rich, Switzerland) Therese Hardin (LIP6, Paris, France) Heinz Hauffe (University of Innsbruck, Austria) Michiel Hazewinkel (CWI, Amsterdam, The Netherlands) Clemens Heine (Springer-Verlag Heidelberg, Germany) Hoon Hong (North Carolina State University, Raleigh, NC) Tetsuo Ida (University of Tsukuba, Japan) Patrick D. F. Ion (University of Michigan, Ann Arbor, MI) Michael Kohlhase (Carnegie Mellon University, Pittsburgh, PA) Peter Michor (ESI, Vienna, Austria) Peter Paule (RISC-Linz, Austria) Carlo Traverso (University of Pisa, Italy) Andrzej Trybulec (University of Bialystok, Poland) Bernd Wegner (Technical University of Berlin, Germany) Eric W. Weisstein (Wolfram Research, Inc., Champaign, IL) Werner Winiwarter (SCCH, Hagenberg, Austria) Local Organization Betina Curtis Christian Vogt RISC, A-4232 Schloss Hagenberg Fax: +43 732 2468 9930 Sponsors NIST, National Institite of Standards and Technology SCCH, Software Competence Center Hagenberg European Commission, OpenMath Thematic Network (IST-2000-28719) European Commission, Calculemus Thematic Network 27-Aug-2001 07:06:07 -0300,7691;000000000001-0000001a Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7R9c7025030 for categories-list; Mon, 27 Aug 2001 06:38:07 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7OHOfd16796; Fri, 24 Aug 2001 14:24:41 -0300 (ADT) Date: Fri, 24 Aug 2001 14:24:41 -0300 (ADT) Message-Id: <200108241724.f7OHOfd16796@mailserv.mta.ca> X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: "F. William Lawvere" To: categories@mta.ca Subject: categories: Clarifying the classifier Date: Fri, 24 Aug 2001 08:59:13 Sender: cat-dist@mta.ca Precedence: bulk To supplement Vaughn Pratt's excellent account of the subobject classifier in the topos of directed graphs, it may help to make explicit the following: The truth object merely represents (i.e., concentrates) a notion which applies in any category. Given two maps x and y with the same codomain, x BELONGS TO y iff the Steenrod lifting problem has a solution (Exist z) x=yz. If y is monic, then of course there is at most one "proof" z of such a belonging relation. Further specializing, if x is also monic, the relation in question is usually called "inclusion of parts" ; specializing in another direction, if the domain of x is a favorite element-kind in the particular category (such as a generic arrow or generic dot in the case of graphs, or the terminal object 1), then it is called "membership". Note that pioneers such as Dedekind and Banach did NOT need to distinguish notationally between these special cases (in contrast to the Peano tradition which seems to have brought more confusion than clarification). The dual Steenrod division problem, which he called "extension", is equally important in mathematical practice; existentially quantifying it we obtain a "delta" relation dual to the epsilon relation: f IS DETERMINED BY g iff there exists (a procedure) p so that f=pg. Again if g is epic there can be at most one p, and of interest is the case where the codomain of f is restricted to a favorite "type"(=space of values for functions). Question: Are there useful categories wherein this determination relation is concentrated in one object as the belonging relation is for toposes? >From: Vaughan Pratt >To: categories@mta.ca >Subject: categories: Re: Subclassifier object question >Date: Mon, 20 Aug 2001 13:01:52 -0700 > >The direct answer to Bill Halchin's concern (`it seems like every >element will be "classified" as belonging to "subX"') is that this is >the defining characteristic of subX: subX consists of those elements >of X that belong to subX. That is, every element of subX has to be >classified as belonging to subX. > >The triviality of this answer suggests that Bill's real question is, >how does the pullback > > f > Y ----> X > | | > !| |g > | | > v z v > 1 ----> Z > >in the definition of topos work in the case of sets? Here's one answer. > >The basic idea is that there are two equally good ways of defining a >subset of a set X, in terms of functions respectively to and from X. > >TO: A function f:Y->X has an image f(Y), a subset of X. > >FROM: A function g:X->Z has an inverse image g^-1({z}) of any given >element z of Z, also a subset of X. > >Every subset of X arises in both ways (provided in the latter case that Z >has at least two elements). With a little care it can be made to arise >in a canonical way in both cases, and moreover such that these two ways >are paired up according to the subset they each determine. > >TO: Now there are many functions to X with the same image. However any >two _injections_ i:Y->X, i':Y'->X have the same image if and only if >there is a bijection j:Y->Y' for which the evident triangle commutes, >namely i'j = i. Call two such injections isomorphic. The isomorphism >classes of injections to X are then in bijection with the subsets of X. > >FROM: Even if we hold Z and an element z thereof fixed there may >still be many functions g:X->Z with the same inverse image g^-1({z}). >This happens for |Z| >= 3, where two g's can agree on the members of >a subset yet disagree about which of the non-z elements of Z to send >the nonmembers to. On the other side, if Z is a singleton we lose the >proper subsets of X, and if Z is empty we lose all subsets. > >We are now in a position to analyze the subobject classifier condition, >which can be stated for sets as follows. > > For every injection i:Y->X there exists a unique g:X->Z making the > above square a pullback. > >Existence and uniqueness each appear twice in this condition, once >explicitly, and once implicitly in the notion of pullback. > >For the former, the existence requirement ensures that Z has enough >elements to permit it to classify at all, while uniqueness prevents it >from having too many, avoiding ``overclassification.'' Thus |Z|=2 is >the only possible choice for a subobject classifier, i.e. Z (along with >its element z) is determined up to isomorphism. > >For the latter, the uniqueness requirement in the definition of pullback >ensures that i is an injection, and existence makes it the the maximal >injection into X for which g(i(y)) = z for all y in Y. Note furthermore >that g uniquely determines i up to isomorphism, i.e. the property of >being a pullback ensures that for each g there exists a unique i up to >isomorphism, giving us the other direction of our desired bijection. > >Although everything said above has been for Set, it can be lifted (with >the necessary care) to any cartesian closed category with the obvious >generalizations of set to object, function to morphism, injection to >monic, and element to morphism-from-1. > >What does not lift are properties of the topos Set not common to all >toposes, such as that Set has a natural numbers object {0,1,2,...}, >and is a Boolean topos (the logic of set membership is Boolean). > >An example of a topos with no natural numbers object is furnished by >the subtopos of Set consisting just of its finite sets. The argument >that Set is a topos shows with almost no modification (and in particular >with the same subobject classifier) that this evidently cartesian closed >subcategory is itself a topos. > >An example of a non-Boolean topos is furnished by the cartesian closed >category of directed graphs made a topos by taking Z to be the 2-clique >(two vertices and four edges) with one of its self-loops duplicated >and the duplicate taken as z (the elements of a directed graph being >its self-loops). A CCC can be made a topos in at most one way up to >isomorphism of its subobject classifier, so (given that this choice >works), this strange graph is it for this topos. > >One quick way to see that this is a topos is to present it as the >presheaf category Set^C where C is the category E=>V with two objects >E,V and two morphisms s,t:E->V. A graph is a functor from C to Set; >it assigns sets to E and V (respectively the set of edges and the set of >vertices), and functions to s and t, respectively the source and target >functions specifying the two vertices the edges run between. The relevant >theorem here is that the functor category Set^C is a topos for any small >category C. For C = E=>V the theorem automatically constructs the above >strange graph. > >Vaughan Pratt > 27-Aug-2001 07:06:29 -0300,2121;000000000001-0000001b Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7R9TM616965 for categories-list; Mon, 27 Aug 2001 06:29:22 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Originating-IP: [217.58.7.162] From: "F. William Lawvere" To: categories@mta.ca Subject: categories: Re: sum of pointed sets. Date: Sat, 25 Aug 2001 10:00:50 Mime-Version: 1.0 Message-ID: Sender: cat-dist@mta.ca Precedence: bulk The meaning of "sum" as coproduct depends on the specification of the ambient category. If we are dealing with multi-pointed sets as suggested , the following would seem reasonable : An m-pointing of a set X is an arbitrary map from m (as a set) to X, and a morphism of such is a pair consisting of a map m to m' and a map X to X' such that the equation expressed by the obvious square holds. In the category thus defined, it is easily verified that your construction indeed has the universal mapping property of coproduct. If we were to restrict m to be finite, but X arbitrary, the above discussion still applies, except that the category  would not be closed under the map-space construction although it does have a truth-value object . On the other hand, if we restrict X to be finite but leave m unrestricted, we obtain a category satisfying both of these topos axioms, yet not definable over sets nor indeed over any Boolean base topos, as Bob Pare showed some years ago. >From: peter_easthope@gulfnet.sd64.bc.ca >To: >Subject: categories: sum of pointed sets. >Date: Mon, 20 Aug 2001 11:53:33 -0300 (ADT) >Hypothesis: the sum of an m-pointed set and an >n-pointed set is an m+n-pointed set. >Is this true? I've not thought of a counterexample. >If this is a theorem, can anyone tell me where to find >a proof. Such a proof, presented by a professional >mathematician, would be interesting and instructive. >Thanks, peter_easthope@gulfnet.sd64.bc.ca 27-Aug-2001 07:30:17 -0300,17834;000000000000-0000001c Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7RA4Db11439 for categories-list; Mon, 27 Aug 2001 07:04:13 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 27 Aug 2001 19:01:48 +0900 (JST) From: Shinya MIYAKAWA Message-Id: <200108271001.TAA11553@micrus.ito.ecei.tohoku.ac.jp> To: categories@mta.ca Subject: categories: TACS2001 PROGRAM AND REGISTRATION INFORMATION Content-Type: text Sender: cat-dist@mta.ca Precedence: bulk <> PROGRAM AND REGISTRATION INFORMATION International Symposium on Theoretical Aspects of Computer Software (TACS2001) Tohoku University, Sendai, Japan October 28-31, 2001 Further information about TACS2001 can be obtained on the Web, at: http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ Any inquiry on TACS2001 Program and Registration may be directed to TACS2001@ito.ecei.tohoku.ac.jp ====================================================================== TACS2001 PROGRAM ^^^^^^^^^^^^^^^^ OCTOBER 28 SUNDAY 16:00 REGISTRATION at Sendai Tokyu Hotel till 21:00 19:30 WELCOME RECEPTION at Sendai Tokyu Hotel till 21:00 OCTOBER 29 MONDAY at Aoba Memorial Building, Tohoku University INVITED TALK 1 9:10 A Spatial Logic for Concurrency Luca Cardelli (joint work with Luis Caires) 10:10 Break SESSION 1, 10:30 - 12:00 10:30 Boxed Ambients Michele Bugliesi, Giuseppe Castagna, Silvia Crafa 11:00 A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation Daisuke Hoshina, Eijiro Sumii and Akinori Yonezawa 11:30 Formal Eavesdropping and its Computational Interpretation Martin Abadi and Jan Jurjens 12:00 Lunch Break INVITED TALK 2 13:15 Resource-Passing Concurrent Programming Kazunori Ueda 14:15 Break SESSION 2, 14:35 - 15:35 14:35 Solo Diagrams Cosimo Laneve, Joachim Parrow, Bjorn Victor 15:05 Observational Equivalence for Synchronized Graph Rewriting with Mobility Barbara Koenig and Ugo Montanari 15:35 Break SESSION 3, 15:55 - 17:25 15:55 Fixed-point Logic with the Approximation Modality and its Kripke Completeness Hiroshi Nakano 16:25 Termination Proofs and Complexity Certification Daniel Leivant 16:55 A Renee Equation for Algorithmic Complexity Keye Martin 17:25 Break OCTOBER 30 TUESDAY at Aoba Memorial Building, Tohoku University INVITED TALK 3 9:10 Nominal Logic: A First Order Theory of Names and Binding Andrew M. Pitts 10:10 Break SESSION 4, 10:30 - 12:00 10:30 A Logic Programming Language based on Binding Algebras Makoto Hamana 11:00 Proof-search and Countermodel Generation in Propositional BI Logic Didier Galmiche and Daniel Mery 11:30 Generation of a Linear Time Query Processing Algorithm based on Well-Quasi-Orders Mizuhito Ogawa 12:00 Lunch Break INVITED TALK 4 13:15 Modelisation of Timed Automata in Coq Christine Paulin-Mohring 14:15 Break SESSION 5, 14:35 - 16:05 14:35 Model-Checking LTL with Regular Valuations for Pushdown Systems Javier Esparza, Antonin Kucera, Stefan Schwoon 15:05 What Will be Eventually True of Polynomial Hybrid Automata? Martin Fraenzle 15:35 Non-Structural Subtype Entailment in Automata Theory Joachim Niehren and Tim Priesnitz 16:05 Break SESSION 6, 16:25 - 17:25 16:25 Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems Ph. Schnoebelen 16:55 Weakest Congruence Results Concerning "Any-Lock" Antti Puhakka 17:25 Break 18:30 BANQUET at Sendai Tokyu Hotel till 20:30 OCTOBER 31st WEDNESDAY at Aoba Memorial Building, Tohoku University INVITED TALK 5 9:10 Design and Correctness of Program Transformations based on Control-Flow Analysis Jon G. Riecke (joint work with Anindya Banerjee and Nevin Heintze) 10:10 Break SESSION 7, 10:30 - 12:00 10:30 Infinite Intersection and Union Types for the Lazy Lambda Calculus Marcello M. Bonsangue and Joost N. Kok 11:00 Strong Normalization of Second Order Symmetric Lambda-mu Calculus Yoriyuki Yamagata 11:30 The Girard-Reynolds Isomorphism Philip Wadler 12:00 Lunch Break INVITED TALK 6 13:15 Lightweight Analysis of Object Interactions Daniel Jackson (joint work with Alan Fekete) 14:15 Break SESSION 8, 14:30 - 15:30 14:30 Typing Assembly Programs with Explicit Forwarding Lennart Beringer 15:00 The UDP Calculus: Rigorous Semantics for Real Networking Andrei Serjantov, Peter Sewell, Keith Wansbrough 15:30 Break OPEN LECTURE 15:45 Unison: A File Synchronizer and its Specification Benjamin C. Pierce (Joint work with Jerome Vouillon) 17:00 CLOSING SESSION till 17:10 -------------------------- 18:30 Japanese Dinner Party for Participants from Abroad ============================================================================== TACS2001 is sponsored by Tohoku University, Sendai, Japan in cooperation with Information Processing Society of Japan Japan Society for Software Science and Technology Association for Symbolic Logic Association for Computing Machinery--SIGACT Symposium Chair: Takayasu Ito Tohoku University Program Chairs: Naoki Kobayashi Tokyo Institute of Technology Benjamin Pierce University of Pennsylvania Program Committee Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann University of Edinburgh Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark University of Edinburgh Makoto Tatuta National Institute of Informatics, Tokyo ========================================================================= GENERAL INFORMATION TACS2001 will be held on the campus of Tohoku University, Sendai, Japan. The invited talks and contributed talks will be presented at the Aoba Memorial Building, Faculty of Engineering located on the Aoba Hill about 3 km west of downtown Sendai. The welcome reception and banquet will be held at Sendai Tokyu Hotel, located in downtown Sendai. The TACS2001 proceedings will be available as a volume of Lecture Notes in Computer Science, Springer-Verlag, at the time of the conference. Sendai is the largest city in the northern part of Honshu Island of Japan, with a population of about a million. The city is known in Japan as the "City of Trees". It is 350 km north of Tokyo and about 2 hours away by the Tohoku Bullet Train (Tohoku Shinkansen). Sendai is a modern, safe city with a moderate climate blessed by four distinct seansons. At the end of October the weather would be mostly sunny with temperature ranging from 5 C (41 F) to 15 C (59 F), and it will be the time of beautiful autumnal tints. Conference registration is open to the public. Reservations for the Japanese dinner party (October 31st) will be limited. Register and make reservations by returning the completed form by email and fax. The registration form is attached below, and it is also available from the TACS2001 web site. There will also be on-site registration at: * Sendai Tokyu Hotel, 16:00 - 21:00, October 28, * Aoba Memorial Bldg, Tohoku Univ, 9:00 - 17:00 on October 29-31. Some information on transportation and hotels is described below. More information on TACS2001, including travel information, is available at the TACS2001 web page: http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ Transportation ^^^^^^^^^^^^^^ Conference participants arriving at the new Tokyo International (Narita) Airport are advised to take the JR Narita Express train from Narita Airport to Tokyo Station. Then take the Yamabiko super express train of Tohoku Shinkansen (Tohoku Bullet Train) from Tokyo to Sendai. Making reservation at Narita Station for the Yamabiko is strongly recommended. Those arriving at the new Osaka International (Kansai) Airport can fly to Sendai Airport, and take Limousine Bus service to Sendai Station. Alternatively, you can take a local train from the Kansai Airport to JR Shin Osaka Station, then take the Tokaido Shinkansen from JR Shin Osaka Station to JR Tokyo Station and change at Tokyo Station to Tohoku Shinkansen. Some details on transportation will be available at the TACS2001 web page. Note: (1) No flight service is available from Narita to Sendai Airport, since the train service is superior. There is another train service from Narita Airport to downtown Tokyo (Ueno) by Skyliner of the Keisei-Narita Line. At Ueno you can take the Yamabiko superexpress of Tohoku Shinkansen to Sendai, but you have to walk about 10 min from Keisei Ueno Station to JR Ueno Station to take Tohoku Shinkansen. (2) If you are going to travel in Japan by JR lines before/after the TACS2001 symposium, it will be convenient and economical to get a JR PASS before your departure. Contact your travel agent for more information on JR PASS (Japan Rail Pass). Hotels ^^^^^^ Two hotels offer discount rates to TACS2001 participants: the Sendai Tokyu Hotel, and the Sendai Washington Hotel. They are 1.2 km west of Sendai Station and about 800 Yen by taxi from the station. Two hotels are located within 5 min walk of each other. More information on TACS2001 is available at the TACS2001 web page. =========================================================================== REGISTRATION AND RESERVATION Registration Fees ^^^^^^^^^^^^^^^^^ Registration fees cover attendance in all sessions, a copy of proceedings, refreshments and snack, the welcome reception and banquet, but not the Japanese dinner party on October 31st. The reduced author rate applies to all authors of the accepted papers, and the reduced committee member rate applies to all members of the Program Committee and the Organizing Committee. The student rate applies to full time students. Registrants paying reduced rates have full privileges at the conference. The companion rate covers the welcome reception and banquet only. Through September 17 From September 18 Regular 40,000 Yen 50,000 Yen Author 30,000 Yen 40,000 Yen Committee Member 30,000 Yen 40,000 Yen Student 20,000 Yen 30,000 Yen Companion 4,000 Yen 6,000 Yen Hotels ^^^^^^ Two convenient Western style hotels offer TACS2001 discount rates. Rates are per person, per night, and include service charge and tax (not including breakfast). Single Room Twin Room Sendai Tokyu Hotel 10,185 Yen 7,560 Yen Sendai Washington Hotel II 8,000 Yen 7,000 Yen Sendai Washington Hotel I 7,000 Yen --------- Note: Twin room reservations are available for two persons. No roommate matching service is available, so twin room reservations remain registrant's responsibility. Japanese dinner party for participants from abroad ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ A Japanese dinner party for participants from abroad will be held at TOYOKAN in the evening of October 31st. The invited speakers, PC members, and some others will attend. A limited number of reservations will be available for this dinner party. The rates are as follows. Conference registrant: 10,000 Yen Companion: 6,000 Yen =================================================================================== Cut here to send your registration and reservation form after filling in the items. =================================================================================== TACS2001 REGISTRATION AND RESERVATION FORM Please register and make reservations by completing the form below and returning it by email to tcs02@thk.jtb.co.jp Registrants are advised to email a copy of their completed form to TACS2001@ito.ecei.tohoku.ac.jp They are also encouraged to send a signed, printed copy of their completed form by FAX to 022-296-3327 (domestic) +81-22-296-3327 (from abroad) which is the fax number of the following agent to take care of the conference registration and reservation. Japan Travel Bureau Group Tours Office Tohoku Tobu Sendai Daiichi Bldg, 6th Floor 4-6-1 Tsutsujigaoka, Miyagino-ku, Sendai 983-0852, Japan FAX: 022-296-3327 (domestic) +81-22-296-3327 (from abroad) PHONE: 022-296-3361 (domestic) +81-22-296-3361 (from abroad) Email: tcs02@thk.jtb.co.jp Registration and reservations will be completed by your payment, whose method is described below. "IMPORTANT NOTE" As described below, from the standpoint of the safety, registrants are advised to pay fees by Bank Transfer. When the payment is made by a credit card, they are advised to send the required information, including Credit Card numbers by FAX; that is, do NOT send Credit Card numbers by email. REGISTRATION FOR TACS2001 ^^^^^^^^^^^^^^^^^^^^^^^^^ Last (Family) Name: First (Given) Name: Middle: Affiliation: Postal Address: City/State/Zip: Country: Phone: Fax: Email: Registration Status : Number of Companions: Companions' names (if applicable): (A) Total Registration Fee(s) in Yen: HOTEL RESERVATION ^^^^^^^^^^^^^^^^^ Hotel First Choice: Hotel Second Choice: Number of Single Room(s): Number of Twin Room(s): Roommate's Name(s) for Twin Room(s): Check-in Date: Check-out Date: Number of Nights: Special Room or other Request: JAPANESE DINNER PARTY ^^^^^^^^^^^^^^^^^^^^^ A limited number of reservations are available for the Japanese dinner party to be held at TOYOKAN in the evening of October 31st, for participants from abroad. (B) 10,000 Yen x [ ] conference registrant(s): (C) 6,000 Yen x [ ] companion(s): TOTAL FEE IN YEN ^^^^^^^^^^^^^^^^ (A) + (B) + (C): Signature (not needed for email): METHOD OF PAYMENT FOR TACS2001 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From the standpoint of the safety and security, participants are encouraged to pay via Bank Transfer. When they pay via credit card, they are advised to send the required information (in particular, Credit Card numbers) by FAX; that is, do NOT send your Credit Card numbers by email. In credit card payment Visa card, MasterCard, and Diners card will be accepted. Personal checks cannot be accepted. All payments must be made in Japanese Yen. Indicate method of payment below: [ ] Bank Transfer to Bank: Tokyo Mitsubishi Bank, Sendai Branch Account Name: TACS2001 Chair Takayasu Ito Account No. 1180724 From : Date of transfer: Payer's name: Note: In Japan the bank number of Tokyo Mitsubishi Bank is 0005, and the number of its Sendai Branch is 320. [ ] Payment by Credit Card Credit Card Type : Card Number: Expiration Date: Signature (not needed for email): : When your payment is via Credit Card, send the above information by FAX to +81-22-296-3327, the fax no. of Japan Travel Bureau Group Tours Office Tohoku. Even when you send the above form by fax, send it by EMAIL without filling in Credit Card number for safety. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Registration and reservations will be confirmed upon receipt of payment. Refunds will be made upon written request received through October 15, 2001 by Japan Travel Bureau Group Tours Office Tohoku. -----*****-----*****-----*****----- 30-Aug-2001 07:11:27 -0300,1266;000000000000-0000001d Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7U9n9M30411 for categories-list; Thu, 30 Aug 2001 06:49:09 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Content-return: allowed Date: Mon, 27 Aug 2001 12:46:43 +0200 From: Elizabeth Douglas Subject: categories: book: Infinite Homotopy Theory To: "'categories@mta.ca'" Message-id: MIME-version: 1.0 X-Mailer: Internet Mail Service (5.5.2653.19) Content-type: text/plain; charset=iso-8859-1 Sender: cat-dist@mta.ca Precedence: bulk Kluwer Academic Publishers are pleased to announce the launch of Infinite Homotopy Theory edited by H-J Baues and A. Quintero. Infinite Homotopy Theory provides an up to date, comprehensive coverage of the area and deals with algebraic topology, homotopy thoery and simple homotopy theory of infinite CW-complexes with ends. More information can be found at http://www.wkap.nl/book.htm/0-7923-6982-3 Liz Douglas Product Manager Tel +31 (0)78 6392 204 Fax: +31(0)78 6392 323 e mail: elizabeth.douglas@wkap.nl http://www.wkap.nl 30-Aug-2001 07:11:39 -0300,925;000000000000-0000001e Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7U9g2I20210 for categories-list; Thu, 30 Aug 2001 06:42:02 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Originating-IP: [158.59.40.226] From: "Keith Harbaugh" To: categories@mta.ca Subject: categories: the alpha of Omega Date: Mon, 27 Aug 2001 23:28:07 +0000 Mime-Version: 1.0 Content-Type: text/plain; format=flowed Message-ID: X-OriginalArrivalTime: 27 Aug 2001 23:28:10.0534 (UTC) FILETIME=[EF369C60:01C12F4F] Sender: cat-dist@mta.ca Precedence: bulk While the topic of topos subobject classifier is current, how far back can the historical and conceptual origins of the use of "$\Omega$" as the symbol denoting such be traced? Regards, Keith Harbaugh 30-Aug-2001 07:15:05 -0300,1069;000000000000-0000001f Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7U9Ykh21135 for categories-list; Thu, 30 Aug 2001 06:34:46 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Wed, 29 Aug 2001 12:00:30 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Modules in a topos Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk What is a good source for the category of modules over a ring object in a Grothendieck topos? I am particularly interested in the question: if I is an injective module and E is an object of the topos, then there is an exponential I^E. Is it injective? Equivalently, are internal copowers left exact? Michael 30-Aug-2001 10:34:31 -0300,1968;000000000000-00000020 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f7UD0lG14717 for categories-list; Thu, 30 Aug 2001 10:00:47 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.5.32.20010830120325.007f2210@TESLA.open.ac.uk> X-Sender: sjv22@TESLA.open.ac.uk X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Date: Thu, 30 Aug 2001 12:03:25 +0100 To: categories@mta.ca From: S Vickers Subject: categories: Re: the alpha of Omega In-Reply-To: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk >While the topic of topos subobject classifier is current, >how far back can the historical and conceptual origins >of the use of "$\Omega$" as the symbol denoting such be traced? > >Regards, >Keith Harbaugh If a topos E is a generalized topological space, then Omega is the internal version of its (ungeneralized) topology, its lattice of opens: for the global elements 1 -> Omega are in bijection with the continuous maps [geometric morphisms] from E to [sheaves over] Sierpinski space. (This extends to generalized elements too. Suppose U is an object of E, a sheaf over E, and let U' -> E be the corresponding local homeomorphism. Then the morphisms U -> Omega correspond with the opens of U'.) Hence Omega can be read as an abbreviation for Open. Is this how the notation actually arose, or is it just a pleasant rationalization of my own? If X is an ordinary topological space, then Omega X is one notation used for its topology. But though I use it myself, I don't know anything about its history. Putting these together you see that when you take E as your base category of sets then Omega 1, the topology of the 1-point space, is just Omega. Steve Vickers Omega University 1-Sep-2001 10:44:02 -0300,2136;000000000000-00000021 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f81Cq4c30345 for categories-list; Sat, 1 Sep 2001 09:52:04 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Fri, 31 Aug 2001 15:12:48 -0400 (EDT) From: "Robert A.G. Seely" To: Categories List Subject: categories: Workshop: History of Categories Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=X-UNKNOWN Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id f7VKdpb14219 Sender: cat-dist@mta.ca Precedence: bulk ------------------------------------------------------------------------------- HISTOIRE DE CATEGORIES 13 ET 14 SEPTEMBRE 2001 CENTRE DE RECHERCHES MATHEMATIQUES Universite de Montreal pavillon Andre-Aisenstadt, salle 4336 SPEAKERS : Liliane Beaulieu (CRM), Christian Houzel (CNRS -Paris 7), Jim Lambek (McGill), Mihail Makkai (McGill), Colin McLarty (Case Western Reserve), Gonzalo Reyes (U. de Montréal). PROGRAMME 13 SEPTEMBRE 13h45 G. REYES, Topos theory in Montreal in the 70's: my personal involvement. 14h45 Discussion 15h00 Pause-cafe CRM 15h30 C. HOUZEL, Ehresmann sur les recollements dans la theorie des categories. 16h30 Discussion 17h00 The End 14 SEPTEMBRE 9h00 C. McLARTY, How the angel of topology and the devil of abstract algebra collaborated to make topology functorial. 10h00 Discussion 10h15 J. LAMBEK, Recollections of a reluctant categorist. 11h15 Discussion 11h30 M. MAKKAI, Categories in the foundations: a selective history. 12h30 Discussion 12h45 Lunch 14h15 L. BEAULIEU, Genese des notions de structure et (iso)morphisme chez N. Bourbaki. 15h15 Discussion 15h30 The End INFORMATION L. Beaulieu, CRM, beaulieu@crm.umontreal.ca L. Belair, UQAM, belair.luc@uqam.ca 1-Sep-2001 10:50:55 -0300,3408;000000000000-00000022 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f81D1wP22234 for categories-list; Sat, 1 Sep 2001 10:01:58 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Fri, 31 Aug 2001 19:17:19 -0400 (EDT) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Comments on diagxy Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk \documentclass{article} \input mtex \input diagxy \input xymatrix \begin{document} When I created diagxy I did not set out to make diagrams that were better than those of xy-pic, but only to make a simpler and more familiar (to users of my diagram macros) interface. Since it is based entirely on xy-pic, it is not possible in any case. But then there are defaults\ldots. A colleague asked me to look at a paper to help him choose a referee and I came on the following display: $$\xymatrix { X_{rs}\ar[rr]^{\Upsilon_{(rs,\tau)}}&& X_{^\tau(rs)}\ar[rr]^{\Upsilon_{(^\tau(rs), \sigma)}}&&X_{^{\sigma\tau}(rs)} } $$ I don't know that the above code is the exact code the authors used, but the results are identical. I call your attention to the varying heights of the three $X$'s. For an extreme example of this, consider $$\bfig \xymatrix{X^\Gamma\ar[r]&x_\gamma} \efig$$ This happens because xymatrix centers the arrow on the middle of the node. I do not know if xymatrix can be told to do otherwise, but the underlying xy-pic code certainly can be and that was the default I chose in designing my morphism macro. Look at $$\bfig \morphism<900,0>[X_{rs}`X_{^\tau(rs)};{\Upsilon_{(rs,\tau)}}] \morphism(900,0)<900,0>[X_{^\tau(rs)}`X_{^{\sigma\tau}(rs)}; {\Upsilon_{(^\tau(rs),\sigma)}}] \efig$$ by contrast. The morphism code actually raises the arrow by a fixed amount (some fraction of the xheight, a font-dependent quantity) above the baseline, which is independent of descenders, ascenders, and sub- and superscripts. Actually, I would have done this with online to, which uses xy-pic only for the arrows, not the nodes and adjusts the lengths of the arrows to fit the labels: $$X_{rs}\to^{\Upsilon_{(rs,\tau)}}X_{^\tau(rs)}\to^{\Upsilon_{(^\tau(rs), \sigma)}}X_{^{\sigma\tau}(rs)}$$ This is not intended as a criticism of xy-pic. It is very general and it would be easy to find examples in which their default was what is wanted. It is just not likely to be in commutative diagrams. They do give the option of placing the arrow with respect to the baseline, which is more than Latex' picture mode does. My old macros were based on that. I now think it may be possible to coerce the picture mode into using the baseline (by putting things into boxes and defining them to have depth 0, if you want the details), but I knew much less 15 years ago when I started using Latex. So I used a different, much less satisfactory, approach that sort of worked but caused other problems and required extensive use of phantom arguments. \kern5pt\noindent Michael \end{document}