December 2000 - Categories - categories.org.au

CfP CMCS2001 - Extended deadline
by Ugo Montanari 26 Dec '00

26 Dec '00

DEADLINE EXTENDED to Jan 8. ============================================================ C A L L F O R P A P E R S 4th International Workshop on Coalgebraic Methods in Computer Science (CMCS2001) Genova, Italy 6-7 April 2001 A satellite workshop of ETAPS 2001 ------------------------------------------------------------ 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 and Berlin. The proceedings appeared as ENTCS Vols. 11,19 and 33. ------------------------------------------------------------ Location CMCS2001 will be held in Genova on 6-7 April 2001, just after ETAPS2001 (European Joint Conferences on Theory and Practice of Software). ------------------------------------------------------------ Program Committee Alexandru Baltag (Amsterdam), Andrea Corradini (Pisa), Bart Jacobs (Nijmegen), Marina Lenisa (Udine), Ugo Montanari (chair, Pisa), Larry Moss (Bloomington, IN), Ataru T. Nakagawa (Tokyo), Dusko Pavlovic (Palo Alto), John Power (Edinburgh), Horst Reichel (Dresden), Jan Rutten (Amsterdam). ------------------------------------------------------------ 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 contributions, be clearly written, and include appropriate reference to and comparison with related work. Papers (of at most 15 pages) should be submitted electronically as uuencoded PostScript files at the address cmcs2001(a)di.unipi.it. 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 EXTENDED, HARD DEADLINE for submission: 8 January 2001, midnight MET. Notification of acceptance: 20 February 2001. Final version due: 10 March 2001. Workshop dates: 6-7 April 2001. ------------------------------------------------------------ Organizers Andrea Corradini (Pisa), Marina Lenisa (Udine), Ugo Montanari (Pisa). ------------------------------------------------------------ For more information: http://www.di.unipi.it/~ugo/CMCS2001.html mailto:cmcs2001@di.unipi.it ============================================================ @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Prof. Ugo Montanari Phone: +39 050 887221 Dipartimento di Informatica Fax: +39 050 887226 Universita' di Pisa Note the zero prefix in the area code. Corso Italia, 40 Email: ugo(a)di.unipi.it I-56100 Pisa, Italy http://www.di.unipi.it/~ugo/ugo.html @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

1 0

job: faculty position at Western MIchigan University
by Ajay Gupta 22 Dec '00

22 Dec '00

Our sincere apologies, if by mistake you receive it multiple times. β--------------------------------------------------------------------------- WESTERN MICHIGAN UNIVERSITY The Department of Computer Science at Western Michigan University (www.cs.wmich.edu) seeks applications for a tenure-track assistant professor position in computer science beginning August 2001. A Ph.D. in computer science or a closely related field is r equired. The development of externally funded research and participation in the department's doctoral program, as well as teaching at all levels, are expected. Applications from persons with research interests in all areas of computer science will be cons idered. Candidates with research interests in networks and systems are especially encouraged to apply. Western Michigan University, a student-centered research university, encourages applications from underrepresented groups. Send letter of application, v ita, transcripts, statements of research and teaching plans and three letters of reference to: Ajay Gupta, Chair, Department of Computer Science, Western Michigan University, 1903 W. Michigan Avenue., Kalamazoo, MI 49008-5371. Fax: (616) 387-3999; Email: ajay.gupta(a)wmich.edu. Review of applications will begin November 1, 2000, and applications will be accepted until the position is filled.

1 0

AVoCS'01 announcement
by David Nowak 22 Dec '00

22 Dec '00

ANNOUNCEMENT (Apologies if you receive multiple copies) AVoCS'01 Workshop on Automated Verification of Critical Systems Oxford, April 19-20, 2001 http://web.comlab.ox.ac.uk/oucl/conferences/wavcs2001/ This workshop continues the annual DERA/OUCL workshop series. It will combine invited presentations with accepted submissions. Motivation The aim of this workshop is to foster a research community in verification in United Kingdom through encouraging communication among researchers. Specific objectives include concrete efforts at integration as well as the transfer of methods between different groups. This year, a special session featuring security will be held. Organising Committee Marta Kwiatkowska, University of Birmingham Michael Leuschel, University of Southampton David Nowak (contact person), Oxford University Joy Reed, Oxford Brookes University Mike Reed, Oxford University Bill Roscoe, Oxford University Ulrich Ultes-Nitsche, University of Southampton Irfan Zakiuddin, DERA Contact Person David Nowak Oxford University Computing Laboratory Wolfson Building Parks Road Oxford, OX1 3QD United Kingdom David.Nowak(a)comlab.ox.ac.uk Sponsors Defence Evaluation and Research Agency (DERA) and Office of Naval Research (ONR) Topics Topics include but are not limited to: * Abstraction methods (symmetry, ...) * Applications to security * Applications to hardware * Case studies * Connections with abstract interpretation * Data independence * Integrating theorem proving and model checking * Model checking * Model checking of infinite systems * Model checking of real-time systems * Performance and dependability evaluation * Refinement checking * Software verification * Temporal and modal logic * Theorem Proving We also encourage submissions which integrate or compare these different approaches. Submissions Authors are requested to submit an abstract to the contact person (cf. above). If possible, submissions should be made electronically in postscript (or PDF format). Additional details on submission guidelines will be posted at the workshop home page. Abstracts relevant to the scope of this workshop will be selected for presentation. Submissions of work in progress talks are encouraged. Contributions will not be peer-reviewed and can thus still be submitted for publication in other fora. Proceedings Informal proceedings will be available at the workshop as a OUCL technical report. Participants are thus invited to submit working notes or abstracts for inclusion in proceedings. After the workshop, proceedings upon invitation will be published. Registration Advance enrolment is required. To enrol please send your name, affiliation, e-mail, address, phone number and fax number to the contact person (cf. above). There will be no registration fee for the workshop. Note that attendance could be restricted or limited, therefore travel plans should not be made until confirmation of your registration has been received.

1 0

TLCA 2001 Accepted Papers
by Samson Abramsky 21 Dec '00

21 Dec '00

The list of accepted papers for TLCA 2001 is now available at http://www.ii.uj.edu.pl/zpi/tlca2001/acc_papers.html Samson Abramsky

1 0

FoSSaCS 2001 Accepted Papers
by Marino Miculan 19 Dec '00

19 Dec '00

Please post. Regards, - Marino ----------------------------------------------------------------- FoSSaCS 2001 Accepted Papers Please find enclosed the list of papers accepted at FoSSaCS 2001. The list is available also on the FoSSaCS web site at http://fossacs.dimi.uniud.it/accepted.html Furio Honsell FoSSaCS'01 Chair ----- 1.Verified Bytecode Verifiers Tobias Nipkow 2.Axioms for Recursion in Call-by-Value Masahito Hasegawa, Yoshihiko Kakutani 3.Decidability of weak bisimilarity for a subset of basic parallel processes Colin Stirling 4.On the complexity of parity word automata Valerie King, Orna Kupferman, Moshe Vardi 5.Secrecy Types for Asymmetric Communication Martin Abadi, Bruno Blanchet 6.Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the Pi-Calculus and Mechanizing the Theory of Contexts Christine RÃ¶ckl, Daniel Hirschkoff, Stefan Berghofer 7.An axiomatic semantics for the synchronous language Gentzen Simone Tini 8.Temporary Data in Shared Dataspace Coordination Languages Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro 9.Type Isomorphisms and Proof Reuse in Dependent Type Theory Gilles Barthe, Olivier Pons 10.Coalgebra of Abstract Processes Sava Krstic, John Launchbury, Dusko Pavlovic 11.On the Modularity of Deciding Call-by-Need IrÃ¨ne Durand, Aart Middeldorp 12.On Garbage and Program Logic Peter W. O'Hearn, Cristiano Calcagno 13.Axiomatizing tropical semirings Luca Aceto, Zoltan Esik, Anna Ingolfsdottir 14.On the Duality between Observability and Reachability Michel Bidoit, Rolf Hennicker, Alexander Kurz 15.The Complexity of Model Checking Mobile Ambients Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot 16.Class Analysis of Object-Oriented Programs through Abstract Interpretation Thomas Jensen, Fausto Spoto 17.Foundations for a graph-based approach to the specification of Access Control Policies Manuel Koch, Luigi Vincenzo Mancini, Francesco Parisi-Presicce 18.High-Level Petri Nets as Type Theories in the Join Calculus Maria Grazia Buscemi, Vladimiro Sassone 19.On Rational Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory Remi Morin 20.On the Decidability of the Finite Model Problem Mikolaj Bojanczyk 21.The Rho Cube Horatiu Cirstea, Claude Kirchner, Luigi Liquori 22.Computational Completeness of Programming Languages Based on Graph Transformation Detlef Plump 23.Synchronized Tree Languages Revisited and New Applications Valerie Gouranton, Helmut Seidl, Pierre Rety 24.Type inference with recursive type equations Mario Coppo 25.Model checking CTL+ and FCTL is hard Francois Laroussinie, Nicolas Markey, Philippe Schnoebelen -----------------------------------------------------------------

1 0

(-2)-categories
by pare＠mscs.cs.Dal.CA 19 Dec '00

19 Dec '00

Here are some thoughts I had on (-2)-categories. When I read John Baez's posting I thought I had missed the boat, but I guess the point is that strict n-categories are not the same as weak n-categories (surprise!). A *strong* n-category (henceforth called n-category) is a category enriched in (n-1)-Cat, the cartesian closed *category* of small (n-1)-categories. In the time honoured way, start with the empty category. It's cartesian closed (it doesn't have a terminal object but let's glance over that). A category enriched in it can have no objects, for where would their homs land. So there is only one, the empty category itself. So the category of small categories enriched in the empty category is 1, the category with one morphism, which is cartesian closed of course. A category enriched in 1 is just a class of objects, and a small one is just a set. So now the category of small categories is just Set, and we are on our way. So what's the point? A set is a 0-category, there is only one (-1)-category, the empty category, and there are no (-2)-categories. There *is* a notion of (-2)-category, viz. an object of the empty category, but there aren't many of those! I think it should be clear from this that there is not even a notion of (-3)-category so it doesn't even make sense to say there are none. Bob Pare

1 0

Picard group of a ringoid
by Bill Rowan 18 Dec '00

18 Dec '00

Tensor product gives a monoid structure on the class of isomorphism types of R,R-bimodules, for a ring or ringoid R. Restricting to those elements for which there is a two-sided inverse yields a group. I am inclined to call this the nonabelian Picard group and denote it by NPic(R). If we start with a commutative ring R, then the usual Picard group of R, Pic(R), can be viewed as an abelian subgroup of NPic(R). Has anyone seen this before? Does anyone have some other idea about what this should be called? Bill Rowan

2 1

reprinting my book
by maxk＠maths.usyd.edu.au 18 Dec '00

18 Dec '00

Allow me to express my thanks to the numerous colleagues who have written during the last couple of days, urging me to re-issue the book and suggesting ways and means. I have replied in person to a few who have made specific offers to participate in the process; but I am grateful to all, both for their useful suggestions and for their encouragement. I shall give more thought to the possibilities early in the new year. Max Kelly.

1 0

whoops
by Peter Freyd 17 Dec '00

17 Dec '00

There was a little trap waiting for Mike and me to fall into. We were seeking conditions on a category C that force Ab[C] to be abelian and we came up with the same condition. I wrote, "Note that the conclusion (abelian) is self-dual but the condition (effective regular) is not." The trouble is: the definition of Ab[C] is not self-dual. I suppose my assertion is true as it stands but the implicit message is wrong. Mike had no such luck; he made it explicit: "[I]t is sufficient that either C or C^op be exact." (Yes, my "effective regular" and Mike's "exact" are equivalent -- it follows just from regularity that the pullback of a cover against itself is a pushout.) It took me a while to find a counterexample and I'm not happy with the one I found. Adjoin to the equational theory of abelian groups a new constant and no further axioms. Let C be the category of finite models. As is the case for the finite models of any equational theory, C is effective regular (and Ab[C] is isomorphic to the category of finite abelian groups). But Ab[C^op] is not abelian. It's empty. (C^op doesn't have a terminator.)

2 1

(-1)-categories and (-2)-categories
by baez＠newmath.UCR.EDU 15 Dec '00

15 Dec '00

Robert Dawson wrote: Surely we should start with the set of (-1)-categories? Actually we should start at least a little bit before that, with (-2)-categories. Let me explain.... Once upon a time I showed what I called the "periodic table" to Chris Isham, a physicist who works on quantum gravity. It starts like this: k-tuply monoidal n-categories n = 0 n = 1 n = 2 k = 0 sets categories 2-categories k = 1 monoids monoidal monoidal categories 2-categories k = 2 commutative braided braided monoids monoidal monoidal categories 2-categories k = 3 " " symmetric sylleptic monoidal monoidal categories 2-categories k = 4 " " " " symmetric monoidal 2-categories k = 5 " " " " " " and it extends infinitely in both directions. The basic idea is that a "k-tuply monoidal n-category" is a weak (n+k)-category with only one j-morphism for j < k. There's a lot of evidence from homotopy theory and elsewhere that each column of this table must "stabilize" when k reaches n + 2. Of course, this observation needs to be made more precise before it can become a theorem, or even a conjecture, so James Dolan and I called it the "stabilization hypothesis". Carlos Simpson found one way to make it precise and prove it: On the Breen-Baez-Dolan stabilization hypothesis for Tamsamani's weak n-categories, math.CT/9810058. but everyone who has a definition should take a whack at it! Anyway, when I showed this pattern to Chris Isham, I was very proud of it, so I was annoyed when he instantly found fault with it. He said: what about the (-2)-categories, (-1)-categories, and monoidal (-1)-categories? You've drawn this big triangle, but it's missing the upper left-hand corner! I told him I'd have to think about that. After that, I kept trying to guess what (-2)-categories, (-1)-categories and monoidal (-1)-categories should be. Clearly a monoidal (-1)-category should be a set with just one element. But what about the other two? Later, when explaining the concepts of "property", "structure" and "stuff" to Toby Bartels, James Dolan figured out what (-1)-categories are. Toby then helped him figure out what (-2)-categories were, too. Actually, I should be a bit careful here: they really figured out what (-1)-groupoids and (-2)-groupoids are. However, I believe that these coincide with (-1)-categories and (-2)-categories. I have a lot to do today, and this article is already getting too long, so I'll stop here and leave these as a puzzle for all of you. It's sort of fun! I should however mention this: after James and I came to understand this stuff, someone pointed out an error in our definition of n-categories, and we were very perturbed until we realized it could be fixed by changing just one number in our existing definition - which would have been obvious from the start if we'd understood about (-1)-categories. John Baez

1 2