From MAILER-DAEMON Mon Nov 24 11:14:03 2003 Date: 24 Nov 2003 11:14:03 -0400 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1069686843@mta.ca> X-IMAP: 1067984347 0000000011 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Tue Nov 4 18:06:59 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 04 Nov 2003 18:06:59 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AH9Iq-0003TX-00 for categories-list@mta.ca; Tue, 04 Nov 2003 18:05:32 -0400 Date: Tue, 4 Nov 2003 19:54:30 GMT From: Paul Taylor Message-Id: <200311041954.hA4JsUc16697@primrose.cs.man.ac.uk> To: categories@mta.ca Subject: categories: natural numbers in weak logics X-Spam-Score: -4.9 (----) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 1 I wonder whether anyone has done an investigation (in either a journal paper or web-accessible lecture notes) of the way in which the natural numbers object has to be re-defined in categories with weak logic. It is well known, for example, that in a category that (has finite products but) is not cartesian closed, parameters have to be added explicitly to the definition, yielding a diagram of the form zero succ Gamma --------> N x Gamma <-------- N x Gamma || . . || . . || . rec . || . . || base V step V Gamma -----------> X <------------- N x X (where, as in proof & type theory, I use Gamma for an arbitrary object, or context of parameters). If the category is cartesian closed then this diagram may be rewritten with the exponential X^Gamma in place of X, the object Gamma itself being removed from the top line. The corresponding recursion scheme is written symbolically as Gamma |- base : X Gamma, n:N, x:X |- step (n,x) : X -------------------------------------------------------------- Gamma, n:N |- rec (n, base, step) : X with beta-rules Gamma |- rec (zero, base, step) = base : X Gamma, n:N |- rec (succ(n), base, step) = step (n, rec (n, base, step)) By the way, we call this "recursion at type X", the point being that as the class of types at which the recursion scheme is asserted grows, so considerably does the power of the logic. A similar generalisation is needed when we want to argue about equations: - I have terms Gamma, n:N, x:X |- a_n, b_n : X, - I prove a base case Gamma |- a_0 = b_0 : X - and an induction step that Gamma, n:N, x:X, a_n = b_n : X |- a_n+1 = b_n+1 : X - From these I want to deduce that Gamma, n:N, x:X |- a_n = b_n : X without assumption. Notice that I said nothing about how a_n and b_n themselves were defined. Indeed, if they had been defined by the same base and step maps on X, they would be equal by the uniqueness hypothesis of the universal property - otherwise known as the eta rule for recursion. To give a simple example to show that we need more than this uniqueness, let b_n=b be constant and a_0 = f u, a_1 = f(s u), a_2 = f(s(s(u)), etc where f: X---> Y and s : Y ---> Y so that the sequence a_n itself is not defined by an endofunction. We can apply the ordinary recursion scheme to this example by considering the subtype or equaliser f ------> Z = { y:Y | f y = b } >------> Y X ------> b since the endofunction s : Y --> Y restricts to Z. In fact, the general equational recursion scheme can be derived from a different equaliser: a_n ------> E = { n:N | a_n = b_n : X} >------> Gamma x N X ------> b_n The base case says that zero : Gamma x N -> N factors through E, whilst the induction step says that succ restricts to a map E -> E. Then the above parametric recursion scheme provides an inverse rec_E : Gamma x N ---> E to the inclusion, one equation being given by uniqueness of rec_N : Gamma x N ---> Gamma x N and the other by the fact that E >---> Gamma x N is mono. As you may have guessed, I became concerned by this issue because I am interested in a certain category that does not have general equalisers, so I will need to assert a more complicated recursion scheme in my case. These two generalisations of the beautifully simple Dedekind -- Peano -- Lawvere definition of the natural numbers are beginning to feel like the thin end of a wedge. Presumably be have to make a further alteration to the definition for every propositional and type connective in our logic. Alternatively, we can consider the situation in set theory or an elementary topos. The equational recursion scheme is valid there because we have equalisers, and we may consider in particular the case where X = Omega is the subobject classifier and b_n=true. This gives Peano induction straight away. We get from a given category to the topos situation by means of a Yoneda embedding, though unfortunately not simply into a presheaf topos or functor category. There has to be a Grothendieck topology to make the representable object N from our category coincide with the constant sheaf whose value is N from Set. Actually, we can unwind this situation and re-express it in terms of elementary category theory or type theory. Let Gamma, n:N |- phi(n) be the predicate that we want to prove generally true by induction. This predicate, like any term, may be shifted from one context Gamma to another one Delta by a multiple substitution of a term using variables from Gamma for each typed variable in Delta. Categorically, this just means the composite u x id phi Delta x N --------> Gamma x N -----> Omega Now phi may actually be true in some particular context Gamma, but not in another one Delta. Those contexts in which it is true form a category, or alternatively a sheaf or sieve on the original category. This sieve is the truth-value of phi in the sheaf topos. I think symbolic logic has language for this situation, possibly involving the word "realises", but I'm not sure at the moment what this is. Let S be this sieve. Like E above, it has a map (natural transformation) E ---> N. If the sieve S is representable by an actual subobject of N in the original category, the same argument as above provides an inverse N ---> S, whence S is the whole of N. (A sieve S is representable by an object U if S consists of all of the maps into U). We can see parametric and equational recursion in terms of this sieve. In the equational case, S consists of all maps to Gamma x N that have equal composites with a_n and b_n. The sieve is representable iff it has a terminal object, which is called the equaliser. In the parametric case, the terminal object of the sieve is the exponential X^Gamma. The general form of the recursion scheme in a category with weak logic that we do not want to embed in a topos therefore appears to be this: N admits recursion at the sieve (cf type) S for whatever generality of sieves we care to choose. Since a sieve is the external manifestation of a subset in the topos, what we have said is that any sieve (of the chosen generality) that contains zero and is closed under successor is the whole of N. In other words, N admits induction or is well founded with respect to such sieves as predicates. Maybe I've just answered my own question, but if someone else has worked on this and written it up more fully then I would like to know. Paul Taylor www.cs.man.ac.uk/~pt From rrosebru@mta.ca Tue Nov 4 18:08:06 2003 -0400 Return-path: Envelope-to: rrosebrugh@mta.ca Delivery-date: Tue, 04 Nov 2003 18:08:06 -0400 Received: from exim by mailserv.mta.ca with spam-scanned (Exim 4.10) id 1AH9LK-0003eu-00 for rrosebrugh@mta.ca; Tue, 04 Nov 2003 18:08:06 -0400 Received: from rrosebru (helo=localhost) by mailserv.mta.ca with local-esmtp (Exim 4.10) id 1AH9LJ-0003ep-00 for rrosebrugh@mta.ca; Tue, 04 Nov 2003 18:08:05 -0400 Date: Tue, 4 Nov 2003 18:08:05 -0400 (AST) From: Bob Rosebrugh To: Bob Rosebrugh Subject: categories: CFP: 10th Conference on Category Theory and Computer Science (CTCS 2004) and Summer School (fwd) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Spam-Status: No, hits=-99.6 required=5.0 tests=MAILTO_TO_SPAM_ADDR,USER_AGENT_PINE,USER_IN_WHITELIST version=2.55 X-Spam-Level: X-Spam-Checker-Version: SpamAssassin 2.55 (1.174.2.19-2003-05-19-exp) Status: RO X-Status: X-Keywords: X-UID: 2 ---------- Forwarded message ---------- Date: Mon, 27 Oct 2003 17:38:14 +0100 From: Thomas Hildebrandt To: categories@mta.ca Subject: categories: CFP: 10th Conference on Category Theory and Computer Science (CTCS 2004) and Summer School 10th CONFERENCE ON CATEGORY THEORY AND COMPUTER SCIENCE (CTCS'04) AUGUST 12-14, 2004 AND SUMMER SCHOOL AUGUST 9-11, 2004 IT University of Copenhagen (ITU) Copenhagen, Denmark FIRST CALL FOR PAPERS CTCS'04 is the 10th Conference on Category Theory and Computer Science. The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory. The emphasis is upon applications of category theory, but it is recognized that the area is highly interdisciplinary. Typical topics of interest include, but are not limited to, category-theoretic aspects of the following: coalgebras and computing concurrent and distributed systems constructive mathematics declarative programming and term rewriting domain theory and topology foundations of computer security linear logic modal and temporal logics models of computation program logics, data refinement, and specification programming language semantics type theory Previous meetings have been held in Guildford (Surrey), Edinburgh (twice), Manchester, Paris, Amsterdam, Cambridge, S. Margherita Ligure (Genova), and Ottawa. The proceedings of the conference will be published as a special issue of ENTCS (Electronic Notes in Theoretical Computer Science). Invited Speakers: Francois Bergeron Martin Hyland Robin Milner Andrew Pitts Thomas Streicher SUMMER SCHOOL Inspired by the success of the graduate student preconference of CTCS'02 in Ottawa, the CTCS of this year will have a similar event: A summer school from August 9-11. The goal is to prepare students - both graduate and undergraduate, with basic knowledge of category theory - for CTCS, through mini-courses in the basic areas underlying some of the fields of the conference. We anticipate offering courses in among others the following areas: Coalgebras Game Semantics Categorical Models for Concurrency Operational Semantics in Concurrency PROGRAMME COMMITTEE Lars Birkedal, Chair (IT University of Copenhagen) Marcelo Fiore (University of Cambridge) Masahito Hasegawa (Kyoto University) Bart Jacobs (University of Nijmegen) Ugo Montanari (University of Pisa) Valeria de Paiva (Palo Alto Research Center) Dusko Pavlovic (Kestrel Institute) John Power (University of Edinburgh) Edmund Robinson (University of London) Peter Selinger (University of Ottawa) ORGANIZING COMMITTEE E. Moggi, Chair, (Genova) S. Abramsky (Oxford) P. Dybjer (Chalmers) B. Jay (Sydney) A. Pitts (Cambridge) LOCAL ORGANIZING COMMITTEE C. Butz T. Hildebrandt A.L. Moerk SUBMISSION OF PAPERS Papers should be submitted, preferably in electronic form, to ctcs04@itu.dk. Papers are limited to 15 pages, and must be submitted in dvi, postscript, or pdf format, possibly gzipped and/or uuencoded, or sent as a standard email attachment. All submissions must be received by April 9th, 2004. If you cannot submit your paper electronically, please contact the program chair at ctcs04@itu.dk. IMPORTANT DATES April 9th, 2004: Submission deadline June 1st, 2004: Notification of authors of accepted papers July 1st, 2004: Revised Papers Due CONFERENCE HOMEPAGE Updated information is available from http://www.itu.dk/research/theory/ctcs2004 SPONSORSHIP The conference and summer school are sponsored by the FIRST graduate school (www.first.dk) and the Theory Department at the IT University of Copenhagen (www.itu.dk/English/research/theory/ From rrosebru@mta.ca Tue Nov 4 18:05:11 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 04 Nov 2003 18:05:11 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AH9Dr-00034w-00 for categories-list@mta.ca; Tue, 04 Nov 2003 18:00:23 -0400 Message-ID: <61B1A61B4F4AD711B3450008C791F6FA14901E@clearwater.unn.ac.uk> From: M Heather To: categories@mta.ca Subject: categories: Quantum logic and applied categories Date: Mon, 3 Nov 2003 15:20:19 -0000 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2657.72) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 3 The complexity of the contributions on this subject seem unlikely to encourage applicable category theory. Quantum Logic is perhaps a prime example where CT can deal directly with 'non-locality' without recourse to quasi-linear reductions like the non-distributive orthocomplemented modular lattice. That may be the accepted interpretation but not for its scientific merits more from an argument ad hominem as it arose from a particular thought experiment of von Neumann. QL in CT via Hilbert spaces is to model a model. A stream can never rise higher than its first spring, said Francis Bacon at the outset of modern science. Surely QL is much better represented by the higher internal logic of a general topos as it satisfies the correspondence principle. The non-distributive lattice version on the other hand cannot. The papers discuss for a BCS Cybernetic Machine Group publication how CT can subsume the various interpretations to help achieve quantum computation in natural computing. These draw on the neutral concept of the anticipatory system introduced by Rosen who has advocated the use of CT for representing life systems. Quantum logic is in a class of modern 'non-local' problems like natural language, information theory, globalisation, social systems, etc that could be greatly advanced by the use of applied category theory. Unfortunately there appears to be no readily available treatise on CT that is not heavily couched in 'local' set-like language and able to pass the adequacy test of Bacon. Michael Heather From rrosebru@mta.ca Thu Nov 6 08:58:35 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 06 Nov 2003 08:58:35 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AHjfK-00053M-00 for categories-list@mta.ca; Thu, 06 Nov 2003 08:55:10 -0400 Message-ID: <3FA8FF63.40802@uwo.ca> Date: Wed, 05 Nov 2003 08:47:15 -0500 From: Rick Jardine User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.2.1) Gecko/20030225 X-Accept-Language: en-us, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: "Algebraic Topological Methods in Computer Science, II" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 4 Conference Announcement: Algebraic Topological Methods in Computer Science, II Department of Mathematics University of Western Ontario London, Ontario, Canada July 16-20, 2004 This is the second installment of a conference series; the first was held at Stanford University in the summer of 2001. The main areas to be covered by this conference include computational geometry and topology, networks and concurrency theory. The meeting will consist of twenty invited lectures, with additional sessions for shorter lectures. The following mathematical scientists have been invited to speak: Saugata Basu (Georgia Tech) Marshall Bern (Xerox PARC) Herbert Edelsbrunner (CS, Duke) Robin Forman (Rice) Eric Goubault (Commissariat a l'Energie Atomique, France) Joel Hass (Math, UC Davis) Maurice Herlihy (CS, Brown) Kathryn Hess (Lausanne) Michael Joswig (Berlin) Reinhard Laubenbacher (Virginia Bioinformatics Institute) Martin Raussen (Aalborg) Vin de Silva (Stanford) Michael Stillman (Cornell) This conference has been funded by grants from the National Science Foundation and the Fields Institute. All conference announcements and information will be available at the web page http://www.math.uwo.ca/~jardine/at-csII.html. The organizers for this meeting are: Gunnar Carlsson, gunnar@math.stanford.edu Rick Jardine, jardine@uwo.ca From rrosebru@mta.ca Sat Nov 8 15:47:17 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 08 Nov 2003 15:47:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AIYzr-0000T7-00 for categories-list@mta.ca; Sat, 08 Nov 2003 15:43:47 -0400 Message-ID: <3FABF397.7982970F@mathstat.yorku.ca> Date: Fri, 07 Nov 2003 11:33:43 -0800 From: Walter Tholen X-Mailer: Mozilla 4.72 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca, tholen Subject: categories: Book announcement Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 The following book has just appeared with Cambridge University Press: Maria Cristina Pedicchio, Walter Tholen (editors): Categorical Foundations Special Topics in Order, Topology, Algebra, and Sheaf Theory The Publisher's information blurb is at http://us.cambridge.org/titles/catalogue.asp?isbn=0521834147 The book grew out of an exchange and cooperation project ("Atlantis") between two consortia of universities in Canada and Europe. It has eight independently readable chapters, as follows: 1 Ordered Sets via Adjunction (R. J. Wood) 2 Locales (J. Picado, A. Pultr, A. Tozzi) 3 A Functional Approach to General Topology (M. M. Clementino, E. Giuli, W. Tholen) 4 Regular, Protomodular, and Abelian Categories (D. Bourn, M. Gran) 5 Aspects of Monads (J. MacDonald, M. Sobral) 6 Algebraic Categories (M.C. Pedicchio, F. Rovatti) 7 Sheaf Theory (C. Centazzo, E. M. Vitale) 8 Beyond Barr Exactness: Effective Descent Morphisms (G. Janelidze, M. Sobral, W. Tholen) From rrosebru@mta.ca Sat Nov 15 14:43:37 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 15 Nov 2003 14:43:37 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AL5LR-0007CP-00 for categories-list@mta.ca; Sat, 15 Nov 2003 14:40:29 -0400 Date: Wed, 12 Nov 2003 20:40:00 +0100 From: Message-Id: <200311121940.hACJe01J007588@alboka.sen.cwi.nl> To: categories@mta.ca Subject: categories: Postdoc and PhD positions at CWI, Amsterdam Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 Position Description ==================== The Coordination and Component Based Software group in SEN3 at CWI has two open positions for: (1) a postdoc for a period of four years, and (2) a PhD student (OIO) for four years. Both positions are within the project number 600.065.120.03N02 Compositional Construction of Component Connectors (C-Quattro), recently funded by the NWO (the Dutch government's funding agency for academic scientific research), with F. Arbab (CWI) and J. Rutten (CWI and VUA) as Principal Investigators. The project C-Quattro is in fact a collaboration of SEN3 at CWI with the Section Theoretical Computer Science at the Free University of Amsterdam (VUA). The postdoc will be employed by CWI; the PhD student will be employed by the VUA but will spend part of his or her time at CWI. The main goal of the C-Quattro project is to develop an operational semantics based on a calculus of component connectors, as the foundation for further development of practical tools and programming environments for the actual deployment of Reo. Reo is a recently introduced channel-based coordination model wherein complex coordinators, called connectors, are compositionally built out of simpler ones. Reo is intended as a ``glue language'' for construction of connectors that orchestrate component instances in a component-based system. The emphasis in Reo is on connectors and their composition only, not on the components that are being connected. The activities under C-Quattro involve both system oriented and theoretical work. On the systems side, we develop tools supporting visual connector programming, as well as the automation of equivalence proofs, e.g., for optimization. On the theoretical side, the semantic modeling is based on the coalgebraic methodology, and coinduction, with its potential for automation, will be the main reasoning principle. The candidate for the postdoc position is expected to have a strong background in Software Engineering, maturity in formal methods and their practical applications, familiarity with component-based software, concurrency, and coordination. Teamwork and leadership, as well as the ability to work effectively with academic colleagues and PhD students, are all important qualifications for this position. The candidate for the PhD position should have a master degree in computer science or mathematics, with a clear interest in questions from theoretical computer science. Ideally, the candidate has a background both in mathematical disciplines such as algebra, analysis and discrete mathematics, and in such elements of theoretical computer science as automata theory and semantics. The Theme SEN3 (http://www.cwi.nl/sen3) at CWI is a dynamic group of internationally recognized researchers who work on Coordination Models and Languages and Component-Based Software Composition. The activity in SEN3 is a productive, healthy mix of theoretical, foundational, and experimental work in Computer Science, ranging in a spectrum covering mathematical foundations of models of computation, formal methods and semantics, implementation of advanced research software systems, as well as their real-life applications. General information =================== CWI is an internationally renowned research institute in mathematics and computer science, located in Amsterdam, The Netherlands. The focus is on fundamental research problems, derived from societal needs. Research is carried out in 15 research themes. More information about these themes can be found on the website www.cwi.nl where you can also take a look at our Annual Report. A substantial part of this research is carried out in the framework of national or international programs. CWI maintains excellent relations with industry and the academic world, at home as well as abroad. After their research careers at CWI, an increasing number of young staff members find employment in these sectors, for example in spin-off companies that are based on research results from CWI. Of course, library and computing facilities are first-rate. CWI's non-scientific services to its personnel include career planning, training & courses, assistance in finding housing, and tailor-made solutions to problems that may occasionally arise. Terms of employment =================== The salary is in accordance with the "CAO-onderzoekinstellingen" and is commensurate with experience. For instance, the postdoc base salary for a fresh PhD with no additional experience in scale 10 is around 2800 Euros/month, and for an experienced PhD in scale 12 it is around 4500 Euros/month. The current starting salary for a first year PhD student is around 1500 Euros/month with an incremental raise for each subsequent year. (Note: a considerable increase in the salaries of all PhD students is currently under negotiation). Besides the salary, CWI offers very attractive and flexible terms of employment, like a collective health insurance, pension-fund, etc. Application =========== For more information on these vacancies you can contact either of the PIs: F. Arbab, telephone +31-20-5924056, e-mail Farhad.Arbab@cwi.nl J. Rutten, telephone +31-20-592-4116, email Jan.Rutten@cwi.nl Official applications, together with curriculum vitae, letters of references, and lists of publications must be sent to Mrs. J. Koster, head of Personnel Department, P.O. box 94079, 1090 GB Amsterdam, The Netherlands. From rrosebru@mta.ca Tue Nov 18 08:46:58 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Nov 2003 08:46:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AM5AC-00038Q-00 for categories-list@mta.ca; Tue, 18 Nov 2003 08:41:00 -0400 Subject: categories: many object version of promonoidal category? From: Stefan Forcey To: categories@mta.ca Date: Mon, 17 Nov 2003 14:22:32 -0500 (EST) X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20031117192236Z10225-28949+90@calvin.math.vt.edu> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 7 Hello, In the following reference [1] B.J. Day, On closed categories of functors, Lecture Notes in Math 137 (Springer, 1970) 1-38 are defined promonoidal, or monoidal enriched categories. It seems that there should be some well known many object version of this, in the sense that a bicategory is the many object version of a monoidal category. Does anyone know a definition or, even better, a reference? A much later related definition is in the appendix of [2] V. Lyubashenko, Category of $A_{\infty}$--categories, Homology, Homotopy and Applications 5(1) (2003), 1-48. Here are defined enriched 2-categories. This seems to be the strict case of what I'm looking for, since a promonoidal category is a monoid in the category of enriched categories, or a one-object category enriched over V-Cat. In [2] enriched 2-categories are defined as enriched over V-Cat. Thanks, Stefan Forcey From rrosebru@mta.ca Wed Nov 19 14:33:13 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 19 Nov 2003 14:33:13 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AMX4l-0000EV-00 for categories-list@mta.ca; Wed, 19 Nov 2003 14:29:15 -0400 Mime-Version: 1.0 X-Sender: street@icsmail.ics.mq.edu.au Message-Id: In-Reply-To: <20031117192236Z10225-28949+90@calvin.math.vt.edu> References: <20031117192236Z10225-28949+90@calvin.math.vt.edu> Date: Wed, 19 Nov 2003 12:43:31 +1100 To: categories@mta.ca From: Ross Street Subject: categories: Re: many object version of promonoidal category? Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 9 Dear Stefan >[1] B.J. Day, On closed categories of functors, Lecture Notes in >Math 137 (Springer, 1970) 1-38 > >are defined promonoidal, or monoidal enriched categories. It seems that >there should be some well known many object version of this, in the sense >that a bicategory is the many object version of a monoidal category. Does >anyone know a definition or, even better, a reference? Brian Day put out a short preprint: Brian J. Day, Biclosed bicategories: localisation of convolution, Macquarie Mathematics Reports #81-0030 (April 1981) but it was (allegedly) too far ahead of its time to be published. Here "biclosed" means that all right extensions and right liftings exist. So a one-object "biclosed bicategory" is a monoidal category with both left and right internal homs. In the short paper he defines what I think is exactly what you want and calls them "probicategories". By performing convolution on the homs one obtains biclosed bicategory which is locally cocomplete. In more recent work, Brian and I have found something more general than probicategories to be useful. Again, afraid of going too general, we have concentrated on the one object case; thus we have things called "substitudes" which are lax versions of promonoidal V-categories. They also generalise Lambek's multicategories. For the promonoidal case of a substitude, the multihoms are all determined up to canonical isomorphism by the nullary, unary and binary homs. See for example: 72. (with B.J. Day) Lax monoids, pseudo-operads, and convolution, in: "Diagrammatic Morphisms and Applications", Contemporary Mathematics 318 (AMS; ISBN 0-8218-2794-4; April 2003) 75-96. 77. (with B.J. Day) Abstract substitution in enriched categories, J. Pure Appl. Algebra 179 (2003) 49-63. The natural level of generality for the subject of 70. (with G.M. Kelly, A. Labella and V. Schmitt) Categories enriched on two sides, J. Pure Appl. Algebra 168 (1) (8 March 2002) 53-98 seems to be substitudes-with-several-objects rather than bicategories. I actually wrote some draft sections on that during the writing of [70] but we chickened out. Best wishes, Ross From rrosebru@mta.ca Wed Nov 19 14:33:13 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 19 Nov 2003 14:33:13 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AMX6n-0000NE-00 for categories-list@mta.ca; Wed, 19 Nov 2003 14:31:21 -0400 Date: Wed, 19 Nov 2003 10:59:47 +0100 Message-Id: <200311190959.hAJ9xlYj006691@urano.sip.ucm.es> To: categories@mta.ca From: alberto@sip.ucm.es Subject: categories: WRLA 2004 - Last call for papers (EXTENDED DEADLINE) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 10 [[ -- Apologies for multiple copies of this message -- ]] +----------------------------------------------------------+ | | | 5th International Workshop on | | Rewriting Logic and its Applications | | | | W R L A 2004 | | | | Barcelona, Spain, March 27-28, 2004 | | | | http://www.fdi.ucm.es/wrla2004 | +----------------------------------------------------------+ The workshop will be held in conjunction with ETAPS 2004 7th European Joint Conferences on Theory and Practice of Software March 27 - April 4, 2004 http://www.lsi.upc.es/etaps04 IMPORTANT DATES December 1, 2003 Deadline for submission (EXTENDED!) January 15, 2004 Notification of acceptance February 18, 2004 Final version in electronic form March 27-28, 2004 Workshop in Barcelona AIMS AND SCOPE Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas. The topics of the workshop comprise, but are not limited to, * foundations and models of RL; * languages based on RL, including implementation issues; * RL as a logical framework; * RL as a semantic framework, including applications of RL to - object-oriented systems, - concurrent and/or parallel systems, - interactive, distributed, open ended and mobile systems, - specification of languages and systems; * extensions of RL, including - real-time and probabilistic extensions, - tile logic, - rewriting approaches to behavioral specifications; * verification techniques for RL specifications, including - equational and coherence methods, and - verification of properties expressed in modal and temporal logics; * comparisons of RL with existing formalisms having analogous aims, including - rho-calculus, - structural operational semantics, - concurrency calculi, - dynamic algebras. PAST EVENTS Previous WRLA workshops have been organized in - Asilomar, California, September 3-6, 1996, - Pont-a-Mousson, France, September 1-4, 1998, - Kanazawa, Japan, September 18-20, 2000, - Pisa, Italy, September 19-21, 2002. The proceedings of the WRLA workshops have been published as volumes 4, 15, 36, and 71 in the Elsevier ENTCS series, available at http://www.elsevier.nl/locate/entcs Selected papers from WRLA'96 have been published in a special issue of Theoretical Computer Science, Volume 285(2), 2002. LOCATION WRLA 2004 will be held in Barcelona, Spain in March 27-28, 2004. It is a satellite workshop of ETAPS 2004, the European Joint Conferences on Theory and Practice of Software. For venue, registration and suggested accommodation see the ETAPS 2004 web page http://www.lsi.upc.es/etaps04 For information about Barcelona, see among others the city web page http://www.bcn.es/english/ihome.htm PROGRAM COMMITTEE David Basin ETH Zurich Manuel Clavel Universidad Complutense de Madrid Steven Eker SRI International, Menlo Park Kokichi Futatsugi JAIST, Tatsunokuchi Fabio Gadducci Universita di Pisa Alexander Knapp LMU, Muenchen Claude Kirchner INRIA Lorraine & LORIA, Nancy Salvador Lucas Universidad Politecnica de Valencia Narciso Marti-Oliet Universidad Complutense de Madrid (Chair) Jose Meseguer University of Illinois at Urbana-Champaign Ugo Montanari Universita di Pisa Pierre-Etienne Moreau INRIA Lorraine & LORIA, Nancy Grigore Rosu University of Illinois at Urbana-Champaign Carolyn Talcott SRI International, Menlo Park SUBMISSIONS Submissions will be evaluated by the Program Committee for inclusion in the proceedings, which will be available at the time of the workshop and are expected to be published in the Elsevier ENTCS series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. They must be unpublished and not submitted simultaneously for publication elsewhere. Papers (of at most 15 pages) should be submitted electronically, preferably as PDF files, to the workshop email address wrla2004@sip.ucm.es providing also a text-only abstract, and detailed contact information of the corresponding author. The final program of the workshop will also include system demonstrations and two invited presentations by Gilles Dowek Ecole Polytechnique & INRIA, Palaiseau Mario Rodriguez-Artalejo Universidad Complutense de Madrid Based on the quality and interest of the accepted papers, the program committee will study the possibility of preparing a special issue of a scientific journal in the field. ORGANIZING COMMITTEE Narciso Marti-Oliet, Manuel Clavel, and Alberto Verdejo Departamento de Sistemas Informaticos y Programacion Universidad Complutense de Madrid, Spain CONTACT INFORMATION For more information, please contact the organizers wrla2004@sip.ucm.es or visit the workshop web page http://www.fdi.ucm.es/wrla2004 IMPORTANT DATES December 1, 2003 Deadline for submission (EXTENDED!) January 15, 2004 Notification of acceptance February 18, 2004 Final version in electronic form March 27-28, 2004 Workshop in Barcelona + + + + + WRLA'04 + + + + + LAST CALL FOR PAPERS + + + + + WRLA'04 + + + + + From rrosebru@mta.ca Fri Nov 21 17:27:55 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 21 Nov 2003 17:27:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1ANImA-0004n3-00 for categories-list@mta.ca; Fri, 21 Nov 2003 17:25:14 -0400 From: Peter Selinger Message-Id: <200311200411.hAK4B7F07182@quasar.mathstat.uottawa.ca> Subject: categories: Graduate student positions, Ottawa To: categories@mta.ca (Categories List) Date: Wed, 19 Nov 2003 23:11:07 -0500 (EST) X-Mailer: ELM [version 2.5 PL3] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 11 Dear colleagues, we're seeking applications for graduate students at the University of Ottawa (see ad below). If you know any bright students who might be interested, please encourage them to apply! Thanks, -- Peter * Graduate Student Positions in Logic, Category Theory, and Foundations of Computation, University of Ottawa, Canada The Logic Group in the Department of Mathematics and Statistics at the University of Ottawa is seeking applications from prospective graduate students for the M.Sc. and Ph.D. program, beginning in September 2004. Graduate students will be part of the activities of the Logic and Foundations of Computation Group. This group includes faculty and students from several different Ottawa-area universities. In the Math Department, the Logic Group currently includes 4 faculty members (R. Blute, A. Felty, P. Scott, P. Selinger), 3 postdocs (V. Capretta, P. Hofstra, M. Weber), and 9 graduate students. For more information about our team, see http://www.mathstat.uottawa.ca/lfc/ Members of our logic group work in the following areas: category theory, type theory, linear logic, quantum programming languages, semantics of computation, lambda calculus, proof theory, proof carrying code, theorem proving, monoidal categories in physics and computing, probabilistic concurrent systems, realizability toposes and constructive mathematics, higher-dimensional categories. Ph.D. students receive funding which covers academic fees and living expenses. The funding available for M.Sc. students varies. For further information about our graduate program and how to apply, please see http://www.mathstat.uottawa.ca/grad/. The deadline for applications for international students is January 15. Philip Scott (phil@site.uottawa.ca) Richard Blute (rblute@mathstat.uottawa.ca) Amy Felty (afelty@site.uottawa.ca) Peter Selinger (selinger@mathstat.uottawa.ca) From rrosebru@mta.ca Mon Nov 24 11:16:45 2003 -0400 Status: X-Status: X-Keywords: Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 24 Nov 2003 11:16:45 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1AOIOr-0004HX-00 for categories-list@mta.ca; Mon, 24 Nov 2003 11:13:17 -0400 To: categories@mta.ca Subject: categories: SPIN 2004 - Call for contributions - Deadline 2003/12/06 Message-Id: From: etaps02 VERIMAG Date: Sun, 23 Nov 2003 17:20:53 +0100 X-IMAG-MailScanner: Found to be clean X-IMAG-MailScanner-Information: Please contact the ISP for more information Sender: cat-dist@mta.ca Precedence: bulk SPIN 2004 11th International SPIN Workshop on Model Checking of Software April 1-3, 2004, Barcelona, Spain Associated with ETAPS 2004 CALL for PAPERS ************************************************************************* ******** Submission Deadline: Abstracts December 6, 2003 ******* ******** Full versions December 14, 2003 **** ************************************************************************* ------------------------------------------------------------------------- Solicited Contributions: Technical Papers, Tutorials, Tool Demonstrations ------------------------------------------------------------------------- Complete Call for Papers (up-to-date information and deadlines): http://www-verimag.imag.fr/SPIN-2004/ Paper Submission Web Site: http://sttt.cs.uni-dortmund.de/spin04/servlet/Conference ------------------------------------------------------------------------- Preliminary list of invited speakers (ETAPS): Robin Milner (Cambridge, GB), Mary Lou Soffa (Pittsburgh, USA) Antti Valmari (Tampere, Finland) ------------------------------------------------------------------------- Themes: The SPIN workshop is a forum for practitioners and researchers interested in model checking based techniques for the validation and analysis of communication protocols and software systems. Techniques based on explicit representations of state spaces, as implemented in the SPIN model checker or other tools, or techniques based on combination of explicit representations with symbolic representations, is the focus of this workshop.It has proven to be particularly suitable to analyze concurrent asynchronous systems. The workshop will focus on topics including theoretical and algorithmic foundations and tools, model derivation from code and code derivation from models, techniques for dealing with large and infinite state spaces, timing and applications. The workshop aims to encourage interactions and exchanges of ideas with all related areas in software engineering. ------------------------------------------------------------------------- Solicited Contributions: SPIN 2004 solicits previously unpublished, currently unsubmitted, original contributions addressing theoretical, experimental and applied problems in model checking of software artifacts. Particular topics include: - model checking based tools, tool extensions and comparative studies - theoretical & algorithmic foundations of model checking based analysis - combination of model-checking techniques with other analysis techniques - model checking of programming languages and code analysis - techniques for analyzing and testing large and infinite state systems - model checking in the system life-cycle - innovative applications of model checking, including * model checking of object-oriented and component based systems * model checking of security systems * model checking of real-time systems - engineering of model checking tools and platforms - convincing case study which apply model-checking to real sw systems ------------------------------------------------------------------------- We solicit submissions of three categories: Full papers: submissions are limited to 18 pages Tool presentations: SPIN 2004 solicits proposals for the demonstration of tools pertinent to the technical objective of this workshop. Submissions are limited to 5 pages. The title should clearly indicate that this is a tool demonstration summary. Longer tool related contributions should be submitted as technical papers. Tutorials: SPIN 2004 solicits proposals for introductory, advanced and industrial application tutorials on all topics pertinent to the technical objective of this workshop. Tutorial proposals should detail intended contents, audience and presentation length. A 1-page abstract of tutorials can be included in the proceedings. All submissions should adhere to Springer Verlag's LNCS format, preferably using LaTeX. The format of the submissions should be either pdf or postscript. ------------------------------------------------------------------------- Programme Committee: ------------------- Bernard Boigelot (Li=E8ge, B) Dragan Bosnacki (Eindhoven, NL) David Dill (Stanford, USA) Javier Esparza (Stuttgart, D) Patrice Godefroid (Bell Labs, USA) Susanne Graf (Verimag, F, chair) John Hatcliff (Kansas State, USA), Gerard Holzmann (Bell Labs, USA), Stefan Leue (Freiburg, D) Pedro Merino (M=E1laga, E) Laurent Mounier (Verimag, F) Mooly Sagiv (Tel-Aviv, Il) Scott Stoller (Stony Brook, USA) Antti Valmari (Tampere, Finnland) ------------------------------------------------------------------------- ----------- you received this e-mail via the individual or collective address categories@mta.ca to unsubscribe from ETAPS list: contact spin04@imag.fr ----------- From rrosebru@mta.ca Fri Nov 28 13:33:18 2003 -0400 Status: X-Status: X-Keywords: Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Nov 2003 13:33:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1APmPQ-0002DG-00 for categories-list@mta.ca; Fri, 28 Nov 2003 13:28:00 -0400 Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Thu, 27 Nov 2003 14:05:37 +0100 To: categories@mta.ca From: Marco Grandis Subject: categories: Preprint: Equilogical spaces, homology and noncommutative geometry X-OriginalArrivalTime: 27 Nov 2003 13:05:19.0265 (UTC) FILETIME=[1BC20110:01C3B4E7] Sender: cat-dist@mta.ca Precedence: bulk The following preprint is available (in pdf and ps): Marco Grandis Equilogical spaces, homology and noncommutative geometry Dip. Mat. Univ. Genova, Preprint 491 (2003), 24 p. Abstract. After introducing singular homology for D. Scott's equilogical spaces, we show how these structures can express 'formal quotients' of topological spaces, which do not exist as ordinary spaces and are related with well-known noncommutative C*-algebras. This study also uses a wider notion of local maps between equilogical spaces, which might be of interest for the general theory of the latter. MSC: 18B30, 54A05, 55U10, 55Nxx, 46L80. Keywords: Equilogical spaces, cubical sets, singular homology, noncommutative C*-algebras. http://www.dima.unige.it/~grandis/Eql.pdf http://www.dima.unige.it/~grandis/Eql.ps Marco Grandis Dipartimento di Matematica Universita` di Genova Via Dodecaneso 35 16146-Genova, Italy e-mail: grandis@dima.unige.it home page: http://www.dima.unige.it/~grandis/ From rrosebru@mta.ca Fri Nov 28 13:33:18 2003 -0400 Status: X-Status: X-Keywords: Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 28 Nov 2003 13:33:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1APmNZ-000201-00 for categories-list@mta.ca; Fri, 28 Nov 2003 13:26:05 -0400 Date: Tue, 25 Nov 2003 09:24:17 +0100 (CET) From: Jiri Adamek To: Subject: categories: CMCS'04: 2nd call for papers Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanned-By: MIMEDefang 2.37 Sender: cat-dist@mta.ca Precedence: bulk + + + CMCS 2004 + + + SECOND ANNOUNCEMENT + + + CALL FOR PAPERS + + +++++++++++++++++ SUBMISSION DEADLINE: JANUARY 1, 2004 ++++++++++++++++ Excuse multiple copies +----------------------------------------------------------+ | | | | | 7th International Workshop on | | Coalgebraic Methods in Computer Science | | | | C M C S 2004 | | | | | | Barcelona, March 27-29, 2004 | | http://www.iti.cs.tu-bs.de/~cmcs/ | | | +----------------------------------------------------------+ The workshop is held in conjunction with ETAPS 2004 (7th European Joint Conferences on Theory Theory and Practice of Software, March 27- April 4,2004) http://www.lsi.upc.es/etaps04/ AIMS AND SCOPE During the last few years, it is becoming increasingly clear that a great variety of state-based dynamical systems, like transition systems, automata, process calculi and class-based systems can be captured uniformly as coalgebras. Coalgebra is developing into a field of its own interest presenting a deep mathematical foundation, a growing field of applications and interactions with various other fields such as reactive and interactive system theory, object oriented and concurrent programming, formal system specification, modal logic, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications. The topics of the workshop include, but are not limited to: - the theory of coalgebras (including set theoretic and categorical approaches); - coalgebras as computational and semantical models (for programming languages, dynamical systems, etc.); - coalgebras in (functional, object-oriented, concurrent) programming; - coalgebras and data types; - (coinductive) definition and proof principles for coalgebras (with bisimulations or invariants); - coalgebras and algebras; - coalgebraic specification and verification; - coalgebras and (modal) logic; - coalgebra and control theory (notably of discrete event and hybrid systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. Previous workshops of the same series have been organized in Lisbon, Amsterdam, Berlin, Genova, Grenoble, and Warsaw. The proceedings appeared as "Electronic Notes in Theoretical Computer Science (ENTCS)", Volumes 11, 19, 33, 41, 65.1 and 82.1. Selected papers have been/are being published in Theoretical Computer Science, Theoretical Informatics and Applications, and Mathematical Structures in Computer Science. You can get an idea of the types of papers presented at previous meetings by looking at the tables of content of the above ENTCS volumes from these meetings. They are available via the ENTCS page http://www.elsevier.nl/gej-ng/31/29/23/show/Products/notes/contents.htt PROGRAM COMMITTEE Jiri Adamek, chair (Braunschweig), Corina Cirstea (Southampton), H. Peter Gumm (Marburg), Alexander Kurz (Leicester), Ugo Montanari (Pisa), Larry Moss (Bloomington, IN), Ataru T. Nakagawa (Tokyo), Dirk Pattinson (Muenchen) Grigore Rosu (Urbana, ILL), Jan Rutten (Amsterdam), James Worrell (New Orleans). LOCATION CMCS 2004 will be held in Barcelona on March 27-29, 2004. It is a satellite workshop of ETAPS 20034, the European Joint Conferences on Theory and Practice of Software. For venue, registration and suggested accommodation see the ETAPS 2004 Web page: http://www.lsi.upc.es/etaps04/ INVITED SEPAKERS Prakash Panangaden (McGill University, Montreal) Alex Simpson (University of Edinburgh) SUBMISSIONS Submissions will be evaluated by the Program Committee for inclusion in the proceedings, which will be published in the ENTCS series. Papers must contain original contribution, be clearly written, and include appropriate reference to and comparison with related work. Papers (of at most 15 pages) should be submitted electronically as PostScript files at the address J.Adamek@tu-bs.de. A separate message should also be sent, with a text-only one-page abstract and with mailing addresses (both postal and electronic), telephone number and fax number of the corresponding author. IMPORTANT DATES Deadline for submission: January 1, 2004 Notification of acceptance: February 1, 2004 Final version due: February 16, 2004 Workshop dates: March 27-29, 2004 For more information, please contact: Jiri Adamek, Technical University of Braunschweig phone: (0049) 5319521 fax: (0049) 5319529 e-mail: J.Adamek@tu-bs.de + + + CMCS '04 + + + SECOND ANNOUNCEMENT + + + CALL FOR PAPERS + +