From MAILER-DAEMON Sat Jul 27 09:44:15 2002 Date: 27 Jul 2002 09:44:15 -0300 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1027773855@mta.ca> X-IMAP: 1027773848 0000000036 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 Mon Oct 1 18:40:00 2001 -0300 >From cat-dist@mta.ca Mon Oct 01 18:40:00 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 01 Oct 2001 18:40:00 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15oAZD-0002tL-00 for categories-list@mta.ca; Mon, 01 Oct 2001 18:25:36 -0300 Message-ID: <217F6DFA440ED111ACDA00A0C906B00601AAE73A@arsenic.rcp.co.uk> From: Michael Abbott To: categories@mta.ca Subject: categories: Is Set lfp, intuitionistically? Date: Mon, 1 Oct 2001 09:02:30 +0100 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 Status: O X-Status: X-Keywords: X-UID: 1 Or, I hope this is the same question, is an elementary topos with a natural numbers object internally locally finitely presentable? Are there any references for this? From rrosebru@mta.ca Mon Oct 1 20:34:10 2001 -0300 >From cat-dist@mta.ca Mon Oct 01 20:34:10 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 01 Oct 2001 20:34:10 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15oCXk-0001u5-00 for categories-list@mta.ca; Mon, 01 Oct 2001 20:32:12 -0300 From: Steve Lack MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15288.62780.881015.61513@milan.maths.usyd.edu.au> Date: Tue, 2 Oct 2001 08:59:08 +1000 To: categories@mta.ca Subject: categories: Re: Only two SMC structures on Cat? In-Reply-To: References: X-Mailer: VM 6.90 under 21.1 (patch 7) "Biscayne" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 2 Jason C Reed writes: > Power, A.J. and Robinson, E.P. Premonoidal categories and notions of > computation (ftp://ftp.dcs.qmw.ac.uk/pub/lfp/edmundr/premoncat.ps.gz) in > section 2 asserts that there is excatly one symmetric monoidal closed > structure on Cat besides the cartesian one. Does anyone know [the location > of] a proof? > > ---Jason > It's Proposition 4 of: Foltz, Lair, and Kelly, Algebraic categories with few moniodal biclosed structures or none, J. Pure Appl. Alg. 17:171-177, 1980. Steve Lack. From rrosebru@mta.ca Tue Oct 2 08:56:34 2001 -0300 >From cat-dist@mta.ca Tue Oct 02 08:56:34 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 02 Oct 2001 08:56:34 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15oO6q-0007O5-00 for categories-list@mta.ca; Tue, 02 Oct 2001 08:53:12 -0300 Date: Tue, 2 Oct 2001 10:44:37 +0100 (BST) From: "Dr. P.T. Johnstone" To: categories@mta.ca Subject: categories: Re: Is Set lfp, intuitionistically? In-Reply-To: <217F6DFA440ED111ACDA00A0C906B00601AAE73A@arsenic.rcp.co.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanner: exiscan *15oM6K-00064b-00*9yGrPezGdUg* http://duncanthrax.net/exiscan/ Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 3 On Mon, 1 Oct 2001, Michael Abbott wrote: > Or, I hope this is the same question, is an elementary topos with a natural > numbers object internally locally finitely presentable? Are there any > references for this? > The answer is yes, but (like a great many such things) I don't think it is written down anywhere. Finite cardinals are internally finitely presentable (the proof of this is similar to the proof that they are internally projective, see 6.25 in "Topos Theory"), and the fact that every object is internally a filtered colimit of finite cardinals is implicit in the construction of the object classifier (cf. 6.32 in the same reference). Peter Johnstone From rrosebru@mta.ca Tue Oct 2 15:34:46 2001 -0300 >From cat-dist@mta.ca Tue Oct 02 15:34:46 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 02 Oct 2001 15:34:46 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15oUGr-0003OA-00 for categories-list@mta.ca; Tue, 02 Oct 2001 15:27:57 -0300 To: categories@mta.ca Subject: categories: is Set LFP? Message-Id: From: Paul Taylor Date: Tue, 02 Oct 2001 15:46:38 +0100 X-Ident: pt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 Michael Abbott asked whether Set is lfp, intuitionistically. > Or, I hope this is the same question, is an elementary topos with a natural > numbers object internally locally finitely presentable? Are there any > references for this? Peter Johnstone said that > the answer is yes, but (like a great many such things) I don't think > it is written down anywhere. Finite cardinals are internally finitely > presentable (the proof of this is similar to the proof that they are > internally projective, see 6.25 in "Topos Theory"), and the fact that > every object is internally a filtered colimit of finite cardinals > is implicit in the construction of the object classifier (cf. 6.32 > in the same reference). Regarding the notion of LFP category as one way (amongst many) of formulating a generalised (but finitary) algebraic theory, Set is the category of models of the theory with one sort, no operations and (of course) no equations. However, one must be careful. Is the category Set^N lfp? The idea is that an object X is finitely presentable if homming from it preserves filtered colimits. (It is also interesting to investigate directed unions, and filtered colimits of surjections.) But which homming functor do we mean? - the external one C(X,-) : C -> Set - or the internal one (-)^X : C -> C (if C is a CCC or a topos). An object X=(X_n) of Set^N is - externally FP iff sum_n X_n is finite, so Some m.All n>n. X_n=0, - internally FP iff each X_n is finite. So there are far more internally FP objects than externally FP ones. This comes from Section 6.6 of "Practical Foundations of Mathematics", http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations/html/s66.html Paul From rrosebru@mta.ca Wed Oct 3 09:49:10 2001 -0300 >From cat-dist@mta.ca Wed Oct 03 09:49:10 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 03 Oct 2001 09:49:10 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15olMh-0006VQ-00 for categories-list@mta.ca; Wed, 03 Oct 2001 09:43:07 -0300 Date: Wed, 3 Oct 2001 10:35:30 -0400 (GMT) From: Mamuka Jibladze Reply-To: Mamuka Jibladze To: Category theory Subject: categories: Re: is Set LFP? In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 5 One more variation on the ``internal lfp'' theme. Continuing Paul Taylor's > The idea is that an object X is finitely presentable if homming from > it preserves filtered colimits. (It is also interesting to > investigate directed unions, and filtered colimits of surjections.) > > But which homming functor do we mean? , one might also ask - which filteredness do we mean? In other words, in the condition `all finite diagrams can be coned', there might be several inequivalent finiteness notions to consider. For example, several such notions appeared in early works by Kock, Lecouturier and Mikkelsen, by Johnstone and Linton; Japie Vermeulen was investigating embeddability into a K-finite object; and, as far as I know, Richard Squire has discovered a whole infinite sequence of (intuitionistically, but not classically) inequivalent finiteness notions. I would appreciate references to any other investigations of finite presentability in this context. Mamuka Jibladze From rrosebru@mta.ca Wed Oct 3 09:49:07 2001 -0300 >From cat-dist@mta.ca Wed Oct 03 09:49:07 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 03 Oct 2001 09:49:07 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15olJW-00089G-00 for categories-list@mta.ca; Wed, 03 Oct 2001 09:39:50 -0300 Message-Id: From: grandis@dima.unige.it (Marco Grandis) To: categories-list@mta.ca Date: Wed, 03 Oct 2001 09:39:50 -0300 Subject: categories: an unpublished text by Grothendieck Status: RO X-Status: X-Keywords: X-UID: 6 Dear colleagues, an unpublished text by Grothendieck is gradually appearing at http://www.math.jussieu.fr/~maltsin/groth/Derivateurs.html At present, the first five chapters are there and can be downloaded. Here below is a copy of the presentation of this "edition" With best wishes Marco _________________________________ Les D=E9rivateurs Texte d'Alexandre Grothendieck =C9dit=E9 par M. K=FCnzer, J. Malgoire, G. Maltsiniotis "Les d=E9rivateurs" est un texte qu'Alexandre Grothendieck a =E9crit en 199= 0, et qui est rest=E9 in=E9dit jusqu'=E0 pr=E9sent. Ce manuscrit de 2000 pages= est consacr=E9 aux fondements de la th=E9orie de l'homotopie. La pr=E9sente ver= sion =E9lectronique n'aurait jamais vu le jour sans l'immense travail de d=E9chiffrage, de transcription en LaTeX, et d'=E9dition de Matthias K=FCnz= er. Je lui exprime ma profonde gratitude. Je tiens =E0 remercier Jean Malgoire de m'avoir fourni une copie du manuscrit que Grothendieck lui a confi=E9 au milieu des ann=E9es 90, et d'avoir pass=E9 d'innombrables heures avec moi = =E0 comparer l'original =E0 la version en TeX. La transcription est aussi fid=E8le que possible au manuscrit. Pour les quelques corrections =E9videntes, ou les rares commentaires des =E9diteurs, ainsi que pour la num=E9rotation originale des pages du manuscrit, les caract=E8res de machine =E0 =E9crire entre crochets sont utilis=E9s. Un poi= nt d'interrogation entre crochets signifie que l'on n'est pas s=FBr du mot qui pr=E9c=E8de. Les chapitres para=EEtront au rythme d'un par mois. Les liens =E9ventuels doivent pointer sur cette page, et non pas directement sur les fichiers ps, dont les noms changeront lors des versions successives. Pour s'inscrire =E0 la liste d'information, pour toute remarque, commentaire, ou correction, envoyer un message =E0 Georges Maltsiniotis ___ From rrosebru@mta.ca Tue Oct 9 16:35:25 2001 -0300 >From cat-dist@mta.ca Tue Oct 09 16:35:25 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 09 Oct 2001 16:35:25 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15r2Tx-0008Dd-00 for categories-list@mta.ca; Tue, 09 Oct 2001 16:24:07 -0300 To: categories@mta.ca Subject: categories: Abstract Stone Duality - manifesto and draft paper Message-Id: From: Paul Taylor Date: Tue, 09 Oct 2001 15:47:38 +0100 X-Ident: pt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 7 http://www.dcs.qmul.ac.uk/~pt/ASD/ I have now written a 7-page "manifesto" that gives a non-technical introduction to the ideas behind Abstract Stone Duality, summarises the four (draft or published) papers that I have written so far, and describes the directions for further work. In particular, "Subspaces in Abstract Stone Duality" is the successor to "Sober Spaces and Continuations", which I advertised on 1 September. It shows how any category with an exponentiable object Sigma can be completed to one in which the adjunction Sigma^(-) -| Sigma^(-) is monadic. This is done in three ways: using the algebras directly, by formally adjoining Sigma-split equalisers, and by extending the lambda-calculus with an "axiom of comprehension". This last, and the normalisation theorem that erases the subtype information, is what I presented at the APPSEM workshop in Darmstadt in March. However, although the mathematical details are more or less all present, the paper is a long way from being finished. As usual, all comments are welcome. Paul From rrosebru@mta.ca Tue Oct 9 16:35:31 2001 -0300 >From cat-dist@mta.ca Tue Oct 09 16:35:31 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 09 Oct 2001 16:35:31 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15r2TT-00088c-00 for categories-list@mta.ca; Tue, 09 Oct 2001 16:23:34 -0300 To: categories@mta.ca Subject: categories: Re: is Set LFP? Message-Id: From: Paul Taylor Date: Tue, 09 Oct 2001 15:36:41 +0100 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 8 (I meant to send this to "categories" last week - by mistake it only went to Mamuka. Sorry if it's now out of context.) Mamuka Jibladze added to my comments on finite presentability, > one might also ask - which filteredness do we mean? In other words, in > the condition `all finite diagrams can be coned', there might be several > inequivalent finiteness notions to consider. Indeed so. That's why I cited Section 6.6 ("Finiteness") of my book - I should have been more explcit about that. Not, of course, that I mean that to be an exhaustive account of the various notions of finiteness. There was a stress on "intuitionistic" in Michael Abbott's original email, which has perhaps got lost in the ensuing discussion. I remember getting very worried about being careful about this, and for example my unpublished paper "The Synthetic Plotkin Powerdomain" with Wesley Phoa was more complicated than it needed to be because I didn't at the time have his confidence in discussing finiteness intuitionistically (= in an elementary topos). However, what I found in writing "Practical Foundations" (with regard to many things but especially) about finiteness is that the traditional ("classical") idioms of mathematical argument are perfectly valid, once one understands the way in which they are idioms for using the rules of natural deduction. The rules for the existential quantifier apparently look very different from the vernacular use of the phrase "there exists" (in which one goes on to make use of the witness), but the correspondence is very clear and natural when you think about it - see Section 1.6. Paul From rrosebru@mta.ca Thu Oct 11 17:18:49 2001 -0300 >From cat-dist@mta.ca Thu Oct 11 17:18:49 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 11 Oct 2001 17:18:49 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15rm64-0006Do-00 for categories-list@mta.ca; Thu, 11 Oct 2001 17:06:24 -0300 Date: Thu, 11 Oct 2001 17:56:09 +0200 (MEST) Message-Id: <200110111556.f9BFu9I07955@pierramenta.imag.fr> From: etaps02.VERIMAG@imag.fr To: categories@mta.ca Subject: categories: CFP: ETAPS 2002, CALL FOR SUBMISSIONS -- DEADLINE OCT 19, 2001 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 9 We apologize if you receive multiple copies of this message. ********************************************************** *** ETAPS 2002 *** *** APRIL, 6-14, 2002 *** *** GRENOBLE, FRANCE *** *** *** *** CALL FOR PAPERS, TOOL DEMOS and TUTORIALS *** *** *** !!!!!!!!!! DEADLINE : OCTOBER 19 !!!!!!!! *** *** ********************************************************** The European Joint Conferences on Theory and Practice of Software ETAPS is a loose and open confederation of conferences and other events that has become the primary European forum for academic and industrial researchers working on topics relating to Software Science. ****************************** * http://www-etaps.imag.fr/ * ****************************** ----------------------------------------------------------------------- 5 Conferences - 13 Satellite Events - Tutorials - Tool Demonstrations ----------------------------------------------------------------------- ----------------------------------------------------------------------- IMPORTANT DATES ----------------------------------------------------------------------- October 19, 2001: Submissions Deadline for the Main Conferences, Demos and Tutorials December 14, 2001: Notification of Acceptance/Rejection January 18 2002: Camera-ready Version Due April 8-12, 2002: ETAPS main Conferences in GRENOBLE April 6-14, 2001: Satellite Events (different submission deadlines) ----------------------------------------------------------------------- ----------------------------------------------------------------------- Main Conferences ----------------------------------------------------------------------- CC 2002: International Conference on Compiler Construction Chair: Nigel Horspool http://www.csr.UVic.CA/cc2002/ ESOP 2002, European Symposium On Programming Chair: Daniel Le Metayer FASE 2002, Fundamental Approaches to Software Engineering Chairs: Ralf-Detlef Kutsche and Herbert Weber http://www.cis.cs.tu-berlin.de/~fase2002/index_general.html FOSSACS 2002 Foundations of Software Science and Computation Structures Chair: Mogens Nielsen http://www.brics.dk/fossacs02/ TACAS 2002, Tools and Algorithms for the Construction and Analysis of Systems Chairs: Perdita Stevens and Joost-Pieter Katoen Tool chair: Hubert Garavel http://www.dcs.ed.ac.uk/tacas2002/ ----------------------------------------------------------------------- Tutorials ----------------------------------------------------------------------- Proposals for half-day or full-day tutorials related to ETAPS 2001 are invited. Tutorial proposals will be evaluated on the basis of their assessed benefit for prospective participants to ETAPS 2001. Contact: Saddek Bensalem, Verimag, Saddek.Bensalem@imag.fr ----------------------------------------------------------------------- Tool Demonstrations ----------------------------------------------------------------------- Demonstrations of tools presenting advances on the state of the art are invited. Submissions in this category should present tools having a clear connection to one of the main ETAPS conferences, possibly complementing a paper submitted separately. Contact: Peter D. Mosses, etaps2002-demo@brics.dk ----------------------------------------------------------------------- Satellite Events ----------------------------------------------------------------------- ACL2: Third Workshop on the ACL2 Theorem Prover and its Applications Contact: Matt Kaufmann, matt.kaufmann@amd.com http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/ AGT: APPLIGRAPH Workshop on Applied Graph Transformation Contact: Hans-Joerg Kreowski, kreo@informatik.uni-bremen.de http://www.informatik.uni-bremen.de/theorie/AGT2002 CMCS: Coalgebraic Methods in Computer Science Contact: Larry Moss, University of Indiana, lsm@cs.indiana.edu http://www.cs.indiana.edu/cmcs COCV: Compiler Optimization Meets Compiler Verification Contact: Jens Knoop, knoop@ls5.cs.uni-dortmund.de http://sunshine.cs.uni-dortmund.de/~knoop/cocv02.html DCC: Designing Correct Circuits Contact: Mary Sheeran, ms@cs.chalmers.se http://www.cs.chalmers.se/~ms/DCC02/ INT: Second Workshop on Integration of Specification Techniques for Applications in Engineering Contact: Martin Grosse-Rhode, mgr@cs.tu-berlin.de http://tfs.cs.tu-berlin.de/~mgr/int02/ LDTA: Second Workshop on Language Descriptions, Tools and Applications Contact: Marjan Mernik, marjan.mernik@uni-mb.si http://www.cwi.nl/conferences/LDTA2002/ SC: Software Composition Contact: Elke Pulvermueller, pulvermueller@acm.org http://i44www.info.uni-karlsruhe.de/~pulvermu/workshops/SC2002 SFEDL: Semantic Foundations of Engineering Design Languages Contact: Gerald Luttgen, g.luettgen@dcs.shef.ac.uk http://www.dcs.shef.ac.uk/~sfedl SLAP: Synchronous Languages, Applications, and Programming Contact: Florence Maraninchi, Florence.Maraninchi@imag.fr http://www.inrialpes.fr/bip/people/girault/Publications/Slap02 SPIN: 9th International SPIN Workshop on Model Checking of Software Contact: Stefan Leue, spin2002@informatik.uni-freiburg.de http://tele.informatik.uni-freiburg.de/spin2002 TPTS: Theory and Practice of Timed Systems Contact: Oded Maler, Oded.Maler@imag.fr http://www-verimag.imag.fr/~maler/TPTS.html VISS: Validation and Implementation of Scenario-based Specifications Contact: Anca Muscholl, muscholl@liafa.jussieu.fr http://www.liafa.jussieu.fr/~anca/VISS02.html ----------------------------------------------------------------------- INVITED SPEAKERS ----------------------------------------------------------------------- Bruno Courcelle, LaBRI, Bordeaux, France Patrick Cousot, ENS Paris, France John Daniels, Syntropy Limited, London, UK Daniel Jackson, Massachusetts Institute of Technology, USA Michael Lowry, NASA Ames Research Center, USA Greg Morrisett, Cornell University, USA Mary Shaw, Carnegy Mellon University, USA Manfred Broy (TU Munich, VISS workshop) Giorgio Buttazzo (University of Pavia, TPTS workshop) Ed Clarke (CMU, SPIN workshop) Charles Concel (Labri, Bordeaux, LDTA workshop) Avi Efrati (Intel Haifa, TPTS workshop) John Hooker (John Hooker, CMU, TPTS workshop) Doron Peled (Bell Labs, VISS workshop) ----------- you received this e-mail via the individual or collective address categories@mta.ca to unsubscribe from ETAPS list: contact etaps02@ormelune.imag.fr ----------- From rrosebru@mta.ca Fri Oct 12 08:29:11 2001 -0300 >From cat-dist@mta.ca Fri Oct 12 08:29:11 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 12 Oct 2001 08:29:11 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15s0PS-00064U-00 for categories-list@mta.ca; Fri, 12 Oct 2001 08:23:22 -0300 Message-ID: From: S.J.Vickers@open.ac.uk To: categories@mta.ca Subject: categories: Re: Abstract Stone Duality - manifesto and draft pape r Date: Wed, 10 Oct 2001 09:59:00 +0100 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 Status: RO X-Status: X-Keywords: X-UID: 10 > In particular, > "Subspaces in Abstract Stone Duality" > is the successor to > "Sober Spaces and Continuations", > which I advertised on 1 September. > > It shows how any category with an exponentiable object Sigma can be > completed to one in which the adjunction Sigma^(-) -| Sigma^(-) is monadic. Should this be exponentiating rather than exponentiable? That was my reading of the version of the paper that I saw - what's postulated is the ability to form Sigma^X for every X rather than X^Sigma. Incidentally, this points up the fact that, as an approach to topology, ASD limits itself to locally compact spaces (or - let us focus on - locales). I know Paul has his own justifications for this limitation. However, some of the features Paul mentioned actually work more generally. For instance, I have recently found that there is a monad PP on the category Loc of all locales that agrees with Sigma^(Sigma^(-)) on the locally compact ones (Sigma = Sierpinski locale). Then if you define Coloc ("colocales") to be the opposite of the category of PP-algebras you get an adjunction Sigma^(-) -| Sigma^(-) analogous to Paul's but between Loc and Coloc. PP is the composite of the upper and lower powerlocales and the construction is mentioned briefly in my paper with Peter Johnstone, "Preframe presentations present". Steve Vickers. From rrosebru@mta.ca Fri Oct 12 17:03:32 2001 -0300 >From cat-dist@mta.ca Fri Oct 12 17:03:32 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 12 Oct 2001 17:03:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15s8TT-0005hf-00 for categories-list@mta.ca; Fri, 12 Oct 2001 17:00:03 -0300 X-Authentication-Warning: gem.dcs.warwick.ac.uk: lazic owned process doing -bs Date: Fri, 12 Oct 2001 16:06:02 +0100 (BST) From: Ranko Lazic X-Sender: lazic@gem To: Ranko Lazic Subject: categories: job: Research position available Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 11 [apologies for multiple copies] Research Officer - Exploiting Data Independence The Oxford University Computing Laboratory seeks a Research Officer to work on an EPSRC-funded research project `Exploiting Data Independence', which is led by Professor A.W. Roscoe (University of Oxford) and Dr R.S. Lazic (University of Warwick). The object of the research is to increase the scope of automated verification of infinite-state systems, in particular where the cause of the infinite or parameterised aspects is the data. The theoretical or applied nature of the contribution of the Research Officer can be suited to your preferences. The post would suit a candidate with a PhD in Computer Science or an equivalent research experience, who has knowledge of one or more of the following areas: * model checking * process algebra * type theory The appointment is for twelve months, starting as soon as possible. Salary is on the age and experience related RSIA grade, currently 17,451 to 26,229 GBP per annum. The Research Officer will be employed by the University of Oxford, but there will be an opportunity to spend a significant part of the appointment at the Department of Computer Science, University of Warwick. More information about the project and the two departments can be found at: http://www.comlab.ox.ac.uk/oucl/research/grants/be.html http://www.comlab.ox.ac.uk/oucl http://www.dcs.warwick.ac.uk/dcs/index.html Applications should state clearly the title of the post, and consist of a full curriculum vitae with supporting letter, together with the names and contact details of two referees. They can either be in electronic form (most formats accepted) and sent to jobs@comlab.ox.ac.uk, or in paper form and addressed to the Administrator, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD, UK. The closing date for receipt of applications is 26 October 2001. Formal selection criteria are available on request or from http://www.comlab.ox.ac.uk/jobs.html. From rrosebru@mta.ca Fri Oct 12 17:03:32 2001 -0300 >From cat-dist@mta.ca Fri Oct 12 17:03:32 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 12 Oct 2001 17:03:32 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15s8SX-0005id-00 for categories-list@mta.ca; Fri, 12 Oct 2001 16:59:05 -0300 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <15298.65494.327038.370859@chtapach.loria.fr> Date: Tue, 9 Oct 2001 15:47:02 +0200 (MEST) From: Christophe Ringeissen To: categories@mta.ca Subject: categories: CFP: AMAST'2002 X-Mailer: VM 6.75 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Reply-To: amast@loria.fr Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 12 [Apologies if you receive this more than once] AMAST 2002 FIRST CALL FOR PAPERS 9-th International Conference on Algebraic Methodology And Software Technology AMAST 2002, September 9-13, 2002 St. Gilles les Bains, Reunion Island, France Important Dates: Paper submissions February 1, 2002 Notification of paper acceptance April 27, 2002 Camera ready papers June 1, 2002 AMAST 2002 conference September 9-13, 2002 Goals: The major goal of the AMAST Conferences is to promote research that may lead to the setting of software technology on a firm, mathematical basis. This goal is achieved by a large international cooperation with contributions from both academia and industry. The virtues of a software technology developed on a mathematical basis have been envisioned as being capable of providing software that is (a) correct, and the correctness can be proved mathematically, (b) safe, so that it can be used in the implementation of critical systems, (c) portable, i.e., independent of computing platforms and language generations, and (d) evolutionary, i.e., it is self-adaptable and evolves with the problem domain. All previous editions of the AMAST Conference, which were held at Iowa City (1989,1991), Twente (1993), Montreal (1995), Munich (1996), Sydney (1997), Manaus (1999), and Iowa City (2000), made contributions to the AMAST goals by reporting and disseminating academic and industrial achievements within the AMAST area of interest. During these meetings, AMAST attracted an international following among researchers and practitioners interested in software technology, programming methodology and their algebraic and logical foundations. In addition, starting with the 1993 edition, the first day of each conference was dedicated to Mathematics Education for Software Engineers. Submissions: As in previous years, we invite papers reporting original research on setting software technology on a firm mathematical basis. We expect two kinds of submissions for this conference: technical papers and system demonstrations. Of particular interest is research on using algebraic, logic, and other formalisms suitable as foundations for software technology, as well as software technologies developed by means of logic and algebraic methodologies. Submissions should not have been published and should not be under consideration for publication elsewhere. Topics of interest include, but are not limited to, the following: SOFTWARE TECHNOLOGY: systems software technology application software technology concurrent and reactive systems formal methods in industrial software development formal techniques for software requirements, design. PROGRAMMING METHODOLOGY: logic programming, functional programming, object paradigms constraint programming and concurrency program verification and transformation programming calculi specification languages and tools formal specification and development case studies. ALGEBRAIC AND LOGICAL FOUNDATIONS: logic, category theory, relation algebra, computational algebra algebraic foundations for languages and systems, coinduction theorem proving and logical frameworks for reasoning logics of programs. SYSTEMS AND TOOLS (for system demonstrations or ordinary papers): software development environments support for correct software development system support for reuse tools for prototyping component based software development tools validation and verification computer algebra systems theorem proving systems. We invite prospective authors to submit electronically previously unpublished papers of high quality. Papers must be no longer than 15 pages (6 pages for system demonstrations) and should be prepared using LaTeX and the LNCS style that can be downloaded from the URL: http://www.springer.de/comp/lncs/authors.html Please send a fully self-contained PostScript file to amast@loria.fr If for any reason it is impossible to submit a paper electronically, authors should send six copies of their submission to the program chair at the address below. All papers will be refereed by the programme committee, and will be judged based on their significance, technical merit, and relevance to the conference. As in the past, the AMAST'2002 proceedings are expected to be published by Springer-Verlag in the Lecture Notes in Computer Science Series. Papers should be received by February 1, 2002. Address for non-electronic submissions: Helene Kirchner Program Chair of AMAST'2002 LORIA and INRIA-Lorraine Campus Scientifique BP 239 54506 Vandoeuvre-les-Nancy Cedex France Program Committee: V.S. Alagar, E. Astesiano, M. Bidoit, D. Bolignano, M. Broy, J. Fiadeiro, B. Fischer, K. Futatsugi, A. Haeberer, N. Halbwachs, A. Haxthausen, D. Hutter, P. Inverardi, B. Jacobs, M. Johnson, H. Kirchner (PC chair), P. Klint, T. Maibaum, Z. Manna, J. Millen, P. Mosses, F. Orejas, R. de Queiroz, T. Rus, C. Ringeissen (PC chair assistant), D. Sannella, P.-Y. Schobbens, G. Scollo, A. Tarlecki, M. Wirsing Local Organization Chair: Teodor Knapik, Univ. de la Reunion Further information: For regularly updated details of the conference organization send email to amast@loria.fr or visit the AMAST'2002 web page: http://www.loria.fr/conferences/amast2002 From rrosebru@mta.ca Fri Oct 12 17:03:35 2001 -0300 >From cat-dist@mta.ca Fri Oct 12 17:03:35 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 12 Oct 2001 17:03:35 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15s8Rg-0005MQ-00 for categories-list@mta.ca; Fri, 12 Oct 2001 16:58:12 -0300 From: Don Sannella MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Message-ID: <15297.35638.843437.237173@haggis.dcs.ed.ac.uk> Date: Mon, 8 Oct 2001 12:17:10 +0100 To: categories@mta.ca Subject: categories: jobs: FOUR research positions in Edinburgh and Munich X-Mailer: VM 6.89 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 13 We apologize if you have received multiple copies of this message. Please forward to potential applicants. ---------------------------------------------------------------------- FOUR research positions available Laboratory for Foundations of Computer Science, University of Edinburgh and Institut fur Informatik, Ludwig-Maximilians-Universitat Munchen on the "Mobile Resource Guarantees" project http://www.lfcs.ed.ac.uk/mrg Closing date: 31 October 2001 The University of Edinburgh and LMU Munich are beginning a joint project entitled "Mobile Resource Guarantees" (MRG) funded by the European Commission under the Global Computing initiative. The project aims to build foundational and practical infrastructure for endowing mobile code with independently verifiable certificates as to its resource consumption. These certificates take the form of condensed formal proofs, generated from typing derivations in linear type systems for describing resource bounds of high-level code. A wide variety of technical work is involved, ranging from theory to development of prototype implementations. We seek applicants who are willing and able to contribute to a team effort, with a strong background in some combination of the following areas: program logic and proof systems, formal methods type systems and static analysis semantics of programming languages (concrete) computational complexity theory compilation techniques for functional and OO programs programming of embedded systems and/or smartcards Alternatively, applicants may have a strong general CS background and be willing to invest some time and energy to catch up on a new and exciting topic. A PhD or equivalent research background is required. The project is scheduled to start in January 2002 and run for three years. Two research positions are available in Edinburgh and two in Munich. In appointing to these positions, we will attempt to optimize the mix of backgrounds and interests at each site and across the project as a whole. It is expected that appointments will be for three years at one site or the other, but there may be scope for shorter appointments as well as for slightly longer appointments involving another closely related project, and also for appointments for part of the time at each of the two sites. Candidates should apply to either Edinburgh or Munich by 31 October 2001. Applicants who are willing to work at either site should apply to Edinburgh, and clearly indicate this willingness on their application. Applicants should send a CV, a statement of the relevance of their background to the MRG project, and contact information for 2-3 referees. Applications to Edinburgh should quote reference 310850 and be sent to Personnel Department, University of Edinburgh, 9-16 Chambers Street, Edinburgh EH1 1HT (fax +44 131 650 6509, or apply on-line at www.jobs.ed.ac.uk). Applications to Munich should be sent to Professor Martin Hofmann, Institut fur Informatik, Oettingenstrasse 67, 80538 Munchen, Germany (fax +49 89 2178 2238, e-mail mhofmann@informatik.uni-muenchen.de). Appointments in Edinburgh will be on the AR1A scale, 17451-26229 per annum. Appointments in Munich will be on the BATIIa scale, 4000-6253DM per month plus a supplement from 1034DM per month depending on family circumstances. For more information, visit http://www.lfcs.ed.ac.uk/mrg. In Edinburgh, contact Don Sannella , telephone +44 131 650 5184. In Munich, contact Martin Hofmann , telephone +49 89 2178 2144. Edinburgh and Munich are both wonderful cities to live in, with a dynamic cultural life as well as easy access to spectacular countryside. Edinburgh: http://www.geo.ed.ac.uk/home/tour/edintour.html LFCS: http://www.lfcs.informatics.ed.ac.uk/ Munich: http://www.muenchen.de/ TCS group at LMU Munchen: http://www.tcs.informatik.uni-muenchen.de From rrosebru@mta.ca Fri Oct 12 17:04:54 2001 -0300 >From cat-dist@mta.ca Fri Oct 12 17:04:54 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 12 Oct 2001 17:04:54 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15s8VA-0005e9-00 for categories-list@mta.ca; Fri, 12 Oct 2001 17:01:48 -0300 Message-ID: <3BC7276C.3FBDE02B@di.unipi.it> Date: Fri, 12 Oct 2001 19:25:00 +0200 From: Roberto Bruni X-Mailer: Mozilla 4.72 [en] (X11; U; Linux 2.2.14-5.0smp i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: just an addendum on bimonoids 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: 14 Dear friends, a short follow-up to the discussion thread initiated by Jules Bean. The history of categories where each object is also a bimonoid (that is, as Tom Leinster pointed out, those self dual categories such that for each object "a" there is an arrow "a -> a \otimes a" and an arrow "a -> e", wher "e" is the unit of the tensor product \otimes) is quite a long one. They appeared with various names (and eventually with just either the monoid or the co-monoid structure) such as categories of relations, Cartesian bicategories, etc, etc... We tried to give some references to all that in a recent, applicative paper of ours, "Some algebraic laws for Spans (and their connections with Multirelations)", call it [SAL] for short, and more are present in the papers of the our group mentioned there (see also the forthcoming paper "normal form for algebras of connections", to appear in TCS, and the references in there). @inproceedings{BG:SAL, author = {Bruni, R. and Gadducci, F.}, title ={Some algebraic laws for spans (and their connections with multirelations)}, booktitle = {Proceedings of RelMiS 2001, Relational Methods in Software}, editor = {Kahl, W. and Parnas, D.L. and Schmidt, G.}, series = {ENTCS}, volume = {44}, number = {3}, year = {2001}, } The paper [SAL] is just a straighforward exercise in Set theory. Nevertheless, it gives concrete, and very simple examples, of categories where objects are bimonoids, but the axioms these two structures satisfy are different. On the one hand, you find what could be called the generalization of Frobenious algebras, where the axiom F indeed holds > > * * * * > \/ |\ | > | = | \ | > | | \| > /\ | | > * * * * > and what could be called the generalization of Hopf algebras, where instead a different axiom holds, as represented by > > * * * * > \/ |\ /| > | = | \/ | > | | /\ | > /\ |/ \| > * * * * > Hope it may be of help. Fabio and Roberto PS Note that any category where each object is a bimonoid, satisfying the F axiom, is also compact closed: a new thread in itself... :-) PPS About analogies for the differences between the axiomatisations, Jules proposed > > I have an intuitive justification for wanting these to be different, > if people aren't offended by slightly silly analogies. Think of the > networks (which is what I call them) as river networks. They have to > flow downhill (down the page). They can join as tributaries do, or > split into distributaries. Then in the 'X' all the water has possibly > mixed; we can't assume it will divide the same way. In the 'N' on the > other hand, all of the water which came in on the right, has > definitely gone out on the right. > Or just think about relations and equivalence relations: in the latter, you always need to close by transitivity. Less of an analogy, in fact, than of a theorem... Anyhow, for the network analogy, see in particular the book "Network Algebra" by Stefanescu, Springer, 2000. From rrosebru@mta.ca Mon Oct 15 17:08:24 2001 -0300 >From cat-dist@mta.ca Mon Oct 15 17:08:24 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 15 Oct 2001 17:08:24 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15tDsH-0002DF-00 for categories-list@mta.ca; Mon, 15 Oct 2001 16:58:09 -0300 Message-Id: <200110151506.RAA04282@rietgras.sen.cwi.nl> X-Authentication-Warning: rietgras.sen.cwi.nl: janr owned process doing -bs To: Jan.Rutten@cwi.nl Subject: categories: preprint: Elements of stream calculus Date: Mon, 15 Oct 2001 17:06:19 +0200 From: Jan Rutten Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 15 The following technical report is now available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R0120.ps.Z (also via my home page: http://www.cwi.nl/~janr): J.J.M.M. Rutten Elements of stream calculus (an extensive exercise in coinduction) Technical Report SEN-R0120, CWI, Amsterdam, 2001. Abstract: Based on the presence of a final coalgebra structure on the set of streams (infinite sequences of real numbers), a coinductive calculus of streams is developed. The main ingredient is the notion of stream derivative, with which both coinductive proofs and definitions can be formulated. In close analogy to classical analysis, the latter are presented as behavioural differential equations. A number of applications of the calculus are presented, including difference equations, analytical differential equations, continued fractions, and some problems from discrete mathematics and combinatorics. The report will also appear in Volume 45 of Elsevier's ENTCS series, which contains the proceedings of MFPS 17. From rrosebru@mta.ca Mon Oct 15 17:08:27 2001 -0300 >From cat-dist@mta.ca Mon Oct 15 17:08:27 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 15 Oct 2001 17:08:27 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15tDsw-0002ca-00 for categories-list@mta.ca; Mon, 15 Oct 2001 16:58:50 -0300 From: Thomas Streicher Message-Id: <200110151604.SAA28474@fb04209.mathematik.tu-darmstadt.de> Subject: categories: job: Announcement TU Darmstadt To: categories@mta.ca Date: Mon, 15 Oct 2001 18:04:56 +0200 (CEST) X-Mailer: ELM [version 2.4ME+ PL66 (25)] 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: 16 The Maths Department of the Technical University Darmstadt has to fill a position (Professor C3) in the area of Logic and Mathematical Foundations of Computer Science Further information can be obtained from www.mathematik.tu-darmstadt.de/Math-Net/Dekanat/Ausschreibungen/c3_de.html The deadline for application is 26.10.2001. Thomas Streicher From rrosebru@mta.ca Thu Oct 18 22:00:12 2001 -0300 >From cat-dist@mta.ca Thu Oct 18 22:00:12 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 18 Oct 2001 22:00:12 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15uNsF-0003Wn-00 for categories-list@mta.ca; Thu, 18 Oct 2001 21:50:55 -0300 Message-ID: <3BCEED78.840D282C@ens.fr> Date: Thu, 18 Oct 2001 16:55:52 +0200 From: Giuseppe Castagna X-Mailer: Mozilla 4.77 [en] (X11; U; SunOS 5.6 sun4u) X-Accept-Language: en, it, fr MIME-Version: 1.0 Subject: categories: job: POSITION AT ENS PARIS Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Bcc: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 RESEARCH/POSTDOC POSITION AT ENS PARIS A research position for one to three years will be available in Ecole Normale Superieure in Paris from beginning of 2002. This position is opened in the context of an European project on formal models for mobility and security. It will corresponds to the position of an average CNRS's CR2 researcher, that is, the retribution of a young tenure researcher with few years of post-doc career. Applicants should have (or expect soon to have) a Ph.D. and justify experience with at least one of these themes: - concurrency and process calculi - type systems - formal verification - static analysis - language-based security - security protocols - proof systems - formal methods For application and further information please contact Giuseppe Castagna (Giuseppe.Castagna@ens.fr) and consult the following page http://www.cogs.susx.ac.uk/projects/myths/ Similar positions are available at the University of Venice and at University of Sussex, as well. Ecole Normale Superieure is one of the most prestigious universities and research center in France. Sited in the center of Paris it prepares few highly selected students, and it counts among its former students several Nobel awards and Field medalists. The computer science department counts groups on cryptology, abstract interpretation, languages and logics, networks, computational geometry, and reconfigurable systems. From rrosebru@mta.ca Sun Oct 21 19:33:03 2001 -0300 >From cat-dist@mta.ca Sun Oct 21 19:33:03 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 21 Oct 2001 19:33:03 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15vQuw-0007FF-00 for categories-list@mta.ca; Sun, 21 Oct 2001 19:18:02 -0300 Date: Fri, 19 Oct 2001 19:05:32 +0100 Message-Id: <200110191805.f9JI5WX14334@tosca.crn.cogs.susx.ac.uk> From: Vladimiro Sassone To: categories@mta.ca Subject: categories: jobs: Research Positions at Sussex Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 18 RESEARCH FELLOWSHIPS / PhD / VISITING PhD POSITIONS AT SUSSEX on projects: DisCo | Mikado | MyThS The Foundations of Computation group (FoC) at the University of Sussex offers positions for a Research Fellow, a PhD student, and at least two visiting PhD students. Full details can be found at: \vs [ -- With apologies for multiple copies of this message -- ] From rrosebru@mta.ca Sun Oct 21 19:33:06 2001 -0300 >From cat-dist@mta.ca Sun Oct 21 19:33:06 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 21 Oct 2001 19:33:06 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15vQxG-0005W9-00 for categories-list@mta.ca; Sun, 21 Oct 2001 19:20:26 -0300 Subject: categories: MFPS 18 + Clifford Lectures From: Michael Mislove To: categories Content-Type: text/plain Content-Transfer-Encoding: 7bit X-Mailer: Evolution/0.16.99+cvs.2001.10.18.15.19 (Preview Release) Date: 19 Oct 2001 16:55:02 -0500 Message-Id: <1003528503.1843.6.camel@linus.math.tulane.edu> Mime-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 Dear Colleagues, Below is the first announcement of this year's MFPS meeting, which is being coordinated with the 2002 Clifford Lectures. The Clifford Lectures will take place on the campus of Tulane University, New Orleans, LA USA from midday, March 20 through midday, March 23, 2002. The Eighteenth Workshop on the Mathematical Foundations of Programming Semantics will then follow, taking place on the Tulane campus from midday, March 23 through March 26, 2002. This year's MFPS will be held in conjunction with the Tulane Mathematics Department's 2002 Clifford Lectures. This annual series of lectures is named in honor of A. H. Clifford, noted algebraist and longtime member of the Tulane Mathematics Department. The 2002 Clifford Lecturer is Sergei N. Artemov, Gaduate Center, CUNY. Professor Artemov will deliver three lectues, and the remainder of the Clifford Lectures program will be comprised of lectures by other invited speakers. All MFPS participants are invited to attend the Clifford Lectures. Since this is a workshop year for MFPS, contributions by participants of talks are welcome on a first come, first serve basis. Detailed information about both the Clifford Lectures and about MFPS 18, as well as updates about the meetings, can be found at the web page http://www.math.tulane.edu/~mfps/mfps18.html An announcement providing registration details and more information about the program will be forthcoming. If you have any questions about MFPS, you can send email to mfps@math.tulane.edu. Please pass this announcement on to those who you think would have an interest in participating. Best regards, Mike Mislove ============================================================= Michael W. Mislove Professor and Chairman Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University Email: mwm@math.tulane.edu New Orleans, LA 70118 URL: http://www.math.tulane.edu/~mwm USA ============================================================= First Announcement 2002 Clifford Lectures and Eighteenth Workshop on the Mathematical Foundations of Programming Semantics Tulane University New Orleans, LA USA March 20 - 26, 2002 The 2002 Clifford Lectures will take place from midday, March 20 through midday, March 23, 2002 on the campus of Tulane University, New Orleans, LA USA. The 2002 Clifford Lecturer is Sergei N. Artemov Graduate Center CUNY Professor Artemov will deliver three lectures during in the series. In addtion, the following have agreed to give lectures during the series: Samson Abramsky (Oxford) Yuri Gurevich (Microsoft) Henk Narendregt (Nijmegen) Joshua Guttman (Mitre) Samuel Buss (UCSD) Dexter Kozen (Cornell) Nachum Dershowitz (Tel Aviv) John Mitchell (Stanford) Helmut Schwichtenberg (Munich) Following the Clifford Lectures, the Eighteenth Workshop on the Mathematical Foundations of Programming Semantics will take place on the Tulane campus from midday, March 23 through March 26, 2002. The invited speakers for MFPS 18 are Rajeev Alur (Penn) John Mitchell (Stanford) Patrick Cousot (ENS, Paris) John Reynolds (CMU) John Hatcliff (Kansas State) Doug Smith (Kestrel) In addition to the invited talks, there will be three special sessions at the meeting. The first will be devoted to abstract interpretation, and is being organized by Radhia Cousot (Ecole Polytechnique) and David Schmidt (Kansas State). The second is on spatial logics, and is being organized by Philippa Gardner (Imperial) and Peter O'Hearn (QMW). The third is on security, and it is being organized by Catherine Meadows (NRL). The remainder of the MFPS program will consist of talks contributed by the participants at the meeting. Those interested in contributing a talk at the meeting should send a title and short abstract to mfps@math.tulane.edu. The available slots will be allocated on a first come, first served basis. The MFPS conferences are devoted to those areas of mathematics, logic and computer science which are related to the semantics of programming languages. The series particularly has stressed providing a forum where both mathematicians and computer scientists can meet and exchange ideas about problems of common interest. We also encourage participation by researchers in neighboring areas, since we strive to maintain breadth in the scope of the series. The Organizing Committee for MFPS consists of Stephen Brookes (CMU), Michael Main (Colorado), Austin Melton (Kent State University), Michael Mislove (Tulane) and David Schmidt (Kansas State). The Co-chairs for MFPS XVIII are Michael Mislove and Stephen Brookes. The Local Arrangements Chairman is Michael Mislove (Tulane). Additional information about the meeting will be posted at the MFPS 18 home page http://www.math.tulane.edu/~mfps/mfps18.html as it bcomes available. This information also will be sent via email to those who request it. To put your name on the MFPS mailing list, send email to mfps@math.tulane.edu. General inquiries about MFPS XVIII can be addressed to mfps@math.tulane.edu. Registration Information Detailed information about registration and accommodations will available shortly. Please check the MFPS XVIII home page http://www.math.tulane.edu/~mfps/mfps18.html for updates. Support We expect to receive support from the US Office of Naval Research. Because of this, we are able to provide limited support for participants. We will focus the available funds on supporting participation by graduate students, and on helping support attendance by members of minorities and women who are contributing a talk at the meeting. If you are a member of one of these groups and are interested in obtaining suppport to attend the meeting, send email to mfps@math.tulane.edu. From rrosebru@mta.ca Sun Oct 21 19:33:09 2001 -0300 >From cat-dist@mta.ca Sun Oct 21 19:33:09 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 21 Oct 2001 19:33:09 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15vQu6-0006zO-00 for categories-list@mta.ca; Sun, 21 Oct 2001 19:17:10 -0300 Message-ID: <3BD0439A.83BF80E9@cogs.susx.ac.uk> Date: Fri, 19 Oct 2001 16:15:38 +0100 From: Bernhard Reus Organization: COGS, University of Sussex X-Mailer: Mozilla 4.76 [en] (X11; U; SunOS 5.7 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: online tutorials Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 20 On the website http://www.pst.informatik.uni-muenchen.de/spring-school99/ of the Spring School on Categorical Methods in Logic and Computer Science held in Munich in 1999 you can now find two online tutorials Sheaves by Giuseppe Rosolini Fibred Categories by Thomas Streicher that can be downloaded in PostScript format. The tutorials are introductory but assume some basic knowledge of category theory. On behalf of the organizing committee, Bernhard Reus From rrosebru@mta.ca Wed Oct 24 20:41:35 2001 -0300 >From cat-dist@mta.ca Wed Oct 24 20:41:35 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 24 Oct 2001 20:41:35 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15wXV3-0007bo-00 for categories-list@mta.ca; Wed, 24 Oct 2001 20:31:53 -0300 Message-ID: <3BD5302C.21893501@dsi.unive.it> Date: Tue, 23 Oct 2001 10:54:04 +0200 From: Michele Bugliesi X-Mailer: Mozilla 4.76 [en] (X11; U; Linux 2.4.2-2 i586) X-Accept-Language: en MIME-Version: 1.0 Subject: categories: job: RESEARCH FELLOWSHIP AT "CA' FOSCARI", VENEZIA Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-MIME-Autoconverted: from 8bit to quoted-printable by localhost.localdomain id f9N8s4u14678 Bcc: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 RESEARCH FELLOWSHIP AT "CA' FOSCARI", VENEZIA The Department of Computer Science at the University "Ca' Foscari" of Venice, Italy, offers a research fellowship on MyThS, a project on types and formal models for mobility and security funded by the European Commission. Full details on the project can be found at http://www.cogs.susx.ac.uk/projects/myths/. The fellowship in Venice is tenable for three years, starting Jan 2002, but applications for shorter appointments of, e.g. one year, are just as welcome. Applicants should have a Ph.D. or equivalent research background in at least one of the following areas: - concurrency and process calculi - type systems - formal verification - static analysis - language-based security - security protocols - proof systems - formal methods The salary for the fellowship will be up to 30000 euros per year, according to qualification. For contacts and inquiries about the application procedure, please contact Michele Bugliesi (michele@dsi.unive.it). The successful candidate will be working with the full-time members of the "Formal Methods and Semantics" research group http://www.dsi.unive.it/~forms. The group is actively engaged in high-quality research in several areas of the theory of programming languages, concurrent systems and security. The Department of Computer Science in Venice is located on the main land, facing the beautiful lagoon and the old part of town. [ -- with apologies for multiple copies of this message --] -- Michele Bugliesi Dipartimento di Informatica, Universit=E0 Ca' Foscari Via Torino 155, Venezia-Mestre Tel: +39 (041) 2908 437 Fax: +39 (041) 2908 419 e-mail: michele@dsi.unive.it http://www.dsi.unive.it/~michele From rrosebru@mta.ca Thu Oct 25 18:28:07 2001 -0300 >From cat-dist@mta.ca Thu Oct 25 18:28:07 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 25 Oct 2001 18:28:07 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15wryU-0002y9-00 for categories-list@mta.ca; Thu, 25 Oct 2001 18:23:38 -0300 Date: Thu, 25 Oct 2001 07:16:15 -0400 (EDT) From: Peter Freyd Message-Id: <200110251116.f9PBGF403849@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Professor Pitts Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 22 Andy Pitts has been awarded a personal chair. Congratulations to the University of Cambridge! From rrosebru@mta.ca Fri Oct 26 16:15:37 2001 -0300 >From cat-dist@mta.ca Fri Oct 26 16:15:37 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 26 Oct 2001 16:15:37 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15xCDO-0002ku-00 for categories-list@mta.ca; Fri, 26 Oct 2001 16:00:22 -0300 Message-Id: To: categories-list@mta.ca Date: Fri, 26 Oct 2001 18:20:58 +0100 Message-Id: <200110261720.f9QHKwJ09639@tosca.crn.cogs.susx.ac.uk> From: Vladimiro Sassone To: categories@mta.ca Subject: categories: CFP: F-WAN: Foundations of Wide Area Network Computing Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 31 =09 F-WAN: Foundations of Wide Area Network Computing =09=09 =09=09 co-located with ICALP2002 =09=09 12-13 July 2002, M=E1laga Spain =09=09First announcement and Call for papers ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Aims and Scope The growing diffusion of internet services and applications is promoting global computing as an emerging model of computation. Based on mobility of code and computation on networks with highly dynamic topologies, the model needs effective infrastructures to support the coordination and control of components loaded at runtime from untrusted sources, as well as semantic frameworks to reason on the behaviour and properties of applications.=20 Foundations of Wide Area Network Computing focuses on semantics aspects of global computing, and invites submissions of original scientific work thereof. A non-exclusive list of topics includes: calculi, models, and semantic theories of concurrent, distributed, mobile, global-computingsystems; languages, security and types for global computing.=20 The workshop proceedings will be published in the ENTCS series and a selection of papers will appear in a special issue of the Journal of Theoretical Computer Science. It will be held as a ICALP2002 satellite event under the auspices of the EATCS.=20 Invited Speakers * Mart=EDn Abadi (UC Santa Cruz) * Luca Cardelli (Microsoft) * Matthew Hennessy (Sussex) * Jim Waldo (SUN Microsystems) Programme Committee * C=E9dric Fournet (Microsoft) * Andrew Gordon (Microsoft) * Alan Jeffrey (De Paul, Chicago) * Ugo Montanari (Pisa) * Catuscia Palamidessi (PennState) * Benjamin Pierce (UPenn) * Davide Sangiorgi (INRIA) * Vladimiro Sassone (Sussex, chair) * Peter Sewell (Cambridge) Important Dates Submission 29 Mar 2002 Notification 18 Jun 2002 PreFinal version 1 Jul 2002 Final version 31 Jul 2002 Submissions Authors are invited to submit an extended abstract of their papers, presenting original contributions to the workshop themes. Submissions should be in English and not exceed 15 standard pages. They should be sent as PS or PDF files to fwan@cogs.susx.ac.uk and be accompanied by a text-only message containing: title, abstract and keywords, the authors' full names, and address and e-mail for correspondence.=20 Simultaneous submission to other meetings with published proceedings is not allowed. =20 Organising Committee * Inmaculada Fortes Ruiz, Llanos Mora, Rafael Morales, Francisco Triguero (M=E1laga)=20 Sponsors The workshop will be held under the auspices of EATCS, the European Association of Theoretical Computer Science.=20 From rrosebru@mta.ca Fri Oct 26 16:20:02 2001 -0300 >From cat-dist@mta.ca Fri Oct 26 16:20:02 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 26 Oct 2001 16:20:02 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15xCRu-0003pL-00 for categories-list@mta.ca; Fri, 26 Oct 2001 16:15:23 -0300 Date: Fri, 26 Oct 2001 17:52:43 +0200 Message-Id: <200110261552.RAA25459@beyond.di.unipi.it> To: categories@mta.ca From: wrla2002@Di.Unipi.IT Subject: categories: CFP: WRLA 2002 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 32 [[ -- Apologies for multiple copies of this message -- ]] ============================================================ C A L L F O R P A P E R S 4th International Workshop on Rewriting Logic and its Applications (WRLA2002) Pisa, Italy 19-21 September, 2002 ------------------------------------------------------------ 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 framework for representing logics. Several languages based on RL (ASF+SDF,CafeOBJ, ELAN, Maude, etc.) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications. The topics of the workshop include, but are not limited to: o foundations, models, and extensions of RL; o languages based on RL; o RL as a logical framework; o applications of RL to: - object-oriented systems; - concurrent and/or parallel systems; - interactive, distributed, open ended and mobile systems; - specification of languages and systems; o rewriting approaches to behavioral specifications; o comparisons of RL with existing formalisms having analogous aims. In addition to the presentations of research results, the program will include tutorials and invited presentations, system demonstrations and panel discussions on specific research topics. Previous workshops of the same series have been organized in Asilomar, Pont-a-Mousson and Kanazawa. The proceedings appeared as ENTCS Vols. 4, 15 and 36. ------------------------------------------------------------ Location WRLA2002 will be held in Pisa on 19-21 September, 2002, at the congress center (ex Convento delle Benedettine) of the local bank (Cassa di Risparmio di Pisa). ------------------------------------------------------------ Program Committee David Basin University of Freiburg Jose Fiadeiro University of Lisbon Kokichi Futatsugi JAIST, Tatsunokuchi Fabio Gadducci University of Pisa Claude Kirchner INRIA Lorraine & LORIA, Nancy Narciso Marti-Oliet Univ. Complutense, Madrid Jose Meseguer U. of Illinois at Urbana-Champaign Ugo Montanari (Chair) University of Pisa Pierre-Etienne Moreau INRIA Lorraine & LORIA, Nancy Peter Mosses BRICS & Univ. of Aarhus Carolyn Talcott Stanford University, Palo Alto Martin Wirsing LMU, Muenchen ------------------------------------------------------------ Submissions Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Papers (of at most 12 pages) should be submitted electronically. The proceedings will be available at the time of the workshop and will be published in the ENTCS series. ------------------------------------------------------------ Important Dates May 24, 2002 Deadline for submission July 24, 2002 Notification of acceptance August 20, 2002 Final version in electronic form September 19-21, 2002 Workshop in Pisa ------------------------------------------------------------ Organizing Committee Roberto Bruni, Fabio Gadducci (Chair) and Ugo Montanari (University of Pisa). ------------------------------------------------------------ Chair for Tutorials and System Demonstrations Narciso Marti-Oliet, Univ. Complutense, Madrid. ------------------------------------------------------------ For more information: Home page: http://www.di.unipi.it/wrla2002 Contact e-mail: wrla2002@di.unipi.it ============================================================ From rrosebru@mta.ca Wed Oct 31 14:36:23 2001 -0400 >From cat-dist@mta.ca Wed Oct 31 14:36:22 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 31 Oct 2001 14:36:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15z03X-00024V-00 for categories-list@mta.ca; Wed, 31 Oct 2001 14:25:39 -0400 Message-ID: <3BE0262D.8020805@bu.edu> Date: Wed, 31 Oct 2001 11:26:21 -0500 From: Saul Youssef Organization: Boston University User-Agent: Mozilla/5.0 (X11; U; Linux 2.2.17-14 i686; en-US; rv:0.9.1) Gecko/20010607 Netscape6/6.1b1 X-Accept-Language: en-us MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Computing with Category Theory Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 33 Greetings to all, I'm a big fan of category theory, but doesn't it seem strange that after all this time there is no programming language that let's you organize things around categorical ideas? I've semi-seriously tried to find out about this ( http://physics.bu.edu/~youssef/aldor/aldor.html ) but I basically don't have an answer. I'd be very interested to hear if anyone is working in this direction or comments about why this hasn't happened. Saul Youssef http://physics.bu.edu/~youssef/ From rrosebru@mta.ca Wed Oct 31 20:06:30 2001 -0400 >From cat-dist@mta.ca Wed Oct 31 20:06:30 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 31 Oct 2001 20:06:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15z5H4-0002fO-00 for categories-list@mta.ca; Wed, 31 Oct 2001 19:59:58 -0400 Date: Wed, 31 Oct 2001 14:08:37 -0500 (EST) From: Phil Scott X-Sender: phil@dinats To: categories@mta.ca Subject: categories: Re: Computing with Category Theory In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 34 Dear Saul: There are several category-based programming languages, but they may be a bit hard to find on first glance. Here are three that come to mind, but I'm sure you will hear about more: 1. The most famous is CAML, which stands for Categorical Abstract Machine Language, and is a variant of ML, a well-known and robust polymorphic functional language. The original implementations arose from work on categorical combinators, but now is an autonomous programming language by itself. http://caml.inria.fr/ 2. Two category theorists who have developped programming languages are: (i) Robin Cockett, with his language Charity: http://www.cpsc.ucalgary.ca/Research/charity/home.html (ii) Barry Jay, with his language FISh: http://www-staff.it.uts.edu.au/~cbj/FISh/ Philip Scott Dept. of Math & Stats U. Ottawa > > > Greetings to all, > > I'm a big fan of category theory, but doesn't it seem strange > that after all this time > there is no programming language that let's you organize things around > categorical ideas? > I've semi-seriously tried to find out about this ( > http://physics.bu.edu/~youssef/aldor/aldor.html ) > but I basically don't have an answer. I'd be very interested to hear if > anyone > is working in this direction or comments about why this hasn't happened. > > Saul Youssef > http://physics.bu.edu/~youssef/ > > > > > > > > > From rrosebru@mta.ca Thu Nov 1 16:31:51 2001 -0400 >From cat-dist@mta.ca Thu Nov 01 16:31:51 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 01 Nov 2001 16:31:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15zOHL-0004HQ-00 for categories-list@mta.ca; Thu, 01 Nov 2001 16:17:35 -0400 Date: Wed, 31 Oct 2001 21:02:13 -0500 (EST) From: Jason C Reed Reply-To: To: Subject: categories: Re: Computing with Category Theory In-Reply-To: <3BE08AB3.969A3A84@it.uts.edu.au> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 35 On Thu, 1 Nov 2001, Barry Jay wrote: > Dear Saul, > > I can envisage at least two distinct ways of computing with categories. > One is for category theorists to use computers to do their calculation > or perhaps even provide formal proofs of theorems. This is actually quite feasible using existing tools. For instance, that we don't need to put the existence of exponentials in the definition of a topos (i.e. a terminal object, subobject classifier, power objects, and pullbacks suffice to construct exponentials) can be proved formally. see http://functor.org/math/cd01.ps. ---Jason From rrosebru@mta.ca Thu Nov 1 16:32:00 2001 -0400 >From cat-dist@mta.ca Thu Nov 01 16:32:00 2001 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 01 Nov 2001 16:32:00 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 3.33 #2) id 15zOGo-0004u3-00 for categories-list@mta.ca; Thu, 01 Nov 2001 16:17:00 -0400 Date: Wed, 31 Oct 2001 16:34:36 -0800 (PST) From: mjhealy@redwood.rt.cs.boeing.com (Michael Healy 425-865-3123) Message-Id: <200111010034.QAA14394@lilith.rt.cs.boeing.com> To: categories@mta.ca Subject: categories: Re: Computing with Category Theory X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 36 Saul, We've applied The Kestrel Institute's Specware package, which implements category-theoric constructs to derive software from knowledge structures. We've demonstrated that we can generate engineering design software. We've also applied Specware in an investigation of mathematically-defined ontologies as a language-neutral knowledge repository for knowledge-based systems. Some references to our work are [1] Unpublished paper describing systems synthesis (written by my colleague Keith Williamson), which can be found in the following page: http://www.kestrel.edu/home/techtransfer.html [2] Applied research with Specware in an industrial setting: K. Williamson, M. Healy and R. Barker (2001) "Industrial Applications of Software Synthesis via Category Theory-Case Studies Using Specware", Journal of Automated Software Engineering, vol. 8, no. 1, pp. 7-30. K. Williamson and M. Healy (2000) "Deriving engineering software from requirements", Journal of Intelligent Manufacturing, vol. 11, no. 1, pp. 3-28. M. Healy and K. Williamson (2000) "Applying Category Theory to Derive Engineering Software from Encoded Knowledge" (Invited Paper), in G. Goos, J. Hartmanis and J. van Leeuwen, ed., Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 2000, Proceedings. Lecture Notes in Computer Science, Springer-Verlag:New York. pp. 484-498. Regards, Mike > > I'm a big fan of category theory, but doesn't it seem strange > that after all this time > there is no programming language that let's you organize things around > categorical ideas? > I've semi-seriously tried to find out about this ( > http://physics.bu.edu/~youssef/aldor/aldor.html ) > but I basically don't have an answer. I'd be very interested to hear if > anyone > is working in this direction or comments about why this hasn't happened. > > Saul Youssef > http://physics.bu.edu/~youssef/ > -- =========================================================================== e Michael J. Healy A FA ----------> GA (425)865-3123 | | FAX(425)865-2964 | | Ff | | Gf c/o The Boeing Company | | PO Box 3707 MS 7L-66 \|/ \|/ Seattle, WA 98124-2207 ' ' USA FB ----------> GB -or for priority mail- e "I'm a natural man." 2760 160th Ave SE MS 7L-66 B Bellevue, WA 98008 USA michael.j.healy@boeing.com -or- mjhealy@u.washington.edu ============================================================================