October 2003 - Categories - categories.org.au

LICS 2004 - Call for Papers
by Alex Simpson 30 Oct '03

30 Oct '03

CALL FOR PAPERS Nineteenth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2004) July 14th - 17th, 2004, Turku, Finland http://www.lfcs.informatics.ed.ac.uk/lics/ The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense. We invite submissions on that theme. Suggested, but not exclusive, topics of interest for submissions include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, domain theory, finite model theory, proof theory, formal aspects of program analysis, formal methods, hybrid systems, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logical representation of knowledge, logics of programs, logic programming, modal and temporal logics, model checking, programming language semantics, reasoning about security, rewriting, specifications, type systems and type theory, and verification. Important Dates: Authors are required to submit electronically a paper title and a short abstract of about 100 words before submitting the extended abstract of the paper. Titles & Short Abstracts Due : January 26, 2004 Extended Abstracts Due : February 2, 2004 Author Notification : March 27, 2004 Camera-ready Papers Due : April 25, 2004 All deadlines are firm; late submissions will not be considered. Detailed information about electronic paper submission will be posted at the LICS website. Submission Instructions: Extended abstracts must be submitted electronically in the IEEE Proceedings two-column camera-ready format. Each abstract must be in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference and to computer science, all phrased for the non-specialist. Technical development directed to the specialist should follow. References and comparisons with related work should be included. Extended abstracts may be no longer than 10 pages including references, and must be formatted in the IEEE Proceedings two-column camera-ready style (IEEE style files will be accessible from the LICS website). If necessary, detailed proofs of technical results can be included in a clearly-labelled appendix in the same two-column format following the 10-page extended abstract. This material may be read at the discretion of the program committee. Extended abstracts not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. All authors of accepted papers will be expected to sign copyright release forms. One author of each accepted paper will be expected to present it at the conference. Short Presentations: LICS 2004 will have a session of short (5--10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages long), should be entered at the LICS 2004 submission site between March 27th and April 4th, 2004. Authors will be notified of acceptance or rejection by April 17th, 2004. Kleene Award for Best Student Paper: An award in honor of the late S.C. Kleene will be given for the best student paper, as judged by the program committee. For a submission to be eligible, the research presented in the paper must have been carried out while all authors were full-time students. The program committee may decline to make the award or may split it among several papers. Affiliated Workshops: As in previous years, there will be a number of workshops affiliated with LICS 2004; information will be posted at the LICS website. Program Chair: Harald Ganzinger MPI Informatik, Saarbruecken, Germany http://www.mpi-sb.mpg.de/~hg/ Program Committee: Rajeev Alur, U. of Pennsylvania Andrew Appel, Princeton U. Albert Atserias, UPC, Barcelona Franz Baader, Dresden U. Samuel Buss, U. of California, San Diego Roberto Di Cosmo, U. de Paris VII Gilles Dowek, Ecole Polytechnique, Paris Harald Ganzinger, MPI, Saarbruecken (chair) Martin Hofmann, LMU Muenchen Achim Jung, U. of Birmingham Leonid Libkin, U. of Toronto Kim Larsen, Aalborg U. Rocco de Nicola, U. di Firenze Damian Niwinski, Warsaw U. Prakash Panangaden, McGill U., Montreal Albert Rubio, UPC, Barcelona Vitaly Shmatikov, SRI International Moshe Vardi, Rice U., Houston Helmut Veith, TU Wien Andrei Voronkov, U. of Manchester Conference Chair: Lauri Hella Department of Math., Stat., and Phil. Kanslerinrinne 1 33014 University of Tampere, Finland Email: lauri.hella(a)uta.fi Workshops Chair: Phil Scott, U. of Ottawa Email: phil(a)site.uottawa.ca Publicity Chair: Alex Simpson, U. of Edinburgh Email: Alex.Simpson(a)ed.ac.uk General Chair: Phokion G. Kolaitis, UC Santa Cruz Email: kolaitis(a)cse.ucsc.edu Organizing Committee: S. Abramsky, A. Broder, E. Clarke, A. Felty, U. Furbach, H. Ganzinger, H. Gabow, J. Halpern, L. Hella, U. Kohlenbach, P. Kolaitis (chair), D. Leivant, G. Longo, H. Mairson, A. Middeldorp, J. Mitchell, M. Nielsen, P. Panangaden, G. Plotkin, P. Scott, R. Shore, A. Simpson, I.A. Stewart. Advisory Board: Y. Gurevich, C. Kirchner, D. Kozen, U. Martin, L. Pacholski, V. Pratt, A. Scedrov, M.Y. Vardi, G. Winskel. Sponsorship: The symposium is sponsored by the IEEE Technical Committee on Mathematical Foundations of Computing in cooperation with the Association for Symbolic Logic, and the European Association for Theoretical Computer Science. Collocated events: ICALP'04 will be collocated with LICS'04; for details see http://www.math.utu.fi/ICALP04/.

1 0

Paper Announcement: On the Geometry of Interaction for Classical Logic
by David J. Pym 29 Oct '03

29 Oct '03

The following may be of interest to readers of this list: Carsten F=FChrmann and David Pym, ''On the Geometry of Interaction for Classical Logic''. Abstract. It is well-known that weakening and contraction cause na=EFve categorical models of the classical sequent calculus to collapse to Boolean lattices. In a previous paper, summarized herein, we provided sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. In this article, we provide concrete examples of such models, based on geometry of interaction and data-flow. Our models provide detailed analyses of the relationships between negation, weakening, and contraction under cut-reduction. Manuscript available at http://www.cs.bath.ac.uk/~pym/classical-GoI.pdf We'd be very pleased to receive comments. This paper follows on from Carsten F=FChrmann and David Pym, "Order-enriched Categorical Models of the Classical Sequent Calculus". Abstract. It is well-known that weakening and contraction cause na=EFve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations. This paper is in submission. Manscript available at http://www.cs.bath.ac.uk/~pym/oecm.pdf Again, we'd be very pleased to receive comments. Regards, David --=20 Prof. David J. Pym Telephone: +44 (0)1 225 38 3246 Professor of Logic & Computation Facsimile: +44 (0)1 225 38 3493 University of Bath Email: d.j.pym(a)bath.ac.uk Bath BA2 7AY, England, U.K. Web: http://www.bath.ac.uk/~cssdjp

1 0

Announcement: Workshop: n-Categories: Foundations and Applications.
by Peter May 27 Oct '03

27 Oct '03

There will be a two week workshop, June 7 - 18, 2004, on the topic: n-Categories: Foundations and Applications. This is the 2004 Summer Program of the Institute for Mathematics and its Applications, at the University of Minnesota. Further information may be found at: http://www.ima.umn.edu/categories Our main goal is to make progress in sorting out the basic foundational issues concerning definitions of "weak n-category", but the main areas of current and potential application will also be discussed. We have generous but limited funding from the IMA, and we have applied to the NSF for supplemental funding. Those interested are invited to register on-line at: http://www.ima.umn.edu/docs/reg_form1.html We will do the best that we can to find (partial) support. Graduate students and postdocs who are seriously interested in learning about this subject and who have some background in category theory and/or categorical homotopy theory are especially invited to register. John Baez and Peter May

1 0

CFP: 10th Conference on Category Theory and Computer Science (CTCS 2004) and Summer School
by Thomas Hildebrandt 27 Oct '03

27 Oct '03

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(a)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(a)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/

1 0

CFP: Computer Aided Verification (CAV) 2004, Boston, MA
by Doron Peled TMP ACCT 25 Oct '03

25 Oct '03

CALL FOR PAPERS COMPUTER AIDED VERIFICATION (CAV) 16th International Conference July 13 -- 17 , 2004, Omni Parker House Hotel, Boston, USA http://www.dcs.warwick.ac.uk/CAV Aims and Scope: CAV'04 conference is the 16th in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. Sample topics of interest include: o Algorithms and tools for verifying models and implementations o Deductive, compositional, and abstraction techniques for verification o Modeling and specification formalisms o Program analysis and software verification o Testing and runtime analysis based on verification technology o Applications and case studies o Verification in industrial practice Special Events: CAV'04 is colocated with the International ACM Symposium on Software Testing and Analysis, ISSTA'04. Invited speakers for CAV'04 are David Harel (Weizmann Institute, plenary speaker for the joint CAV-ISSTA session), Mary Jean Harrold (Georgia Institute of Technology), and Tom Reps (University of Wisconsin). CAV will be preceded by an invited tutorial on processor verification by Randy Bryant (Carnegie Mellon University), David Dill (Stanford University), and Warren Hunt (University of Texas, Austin). The conference will be followed by special workshops. Paper submission: There are two categories of submissions: A. Regular papers. Submissions, not exceeding thirteen (13) pages using Springer's LNCS format, should contain original research, and sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data available with their submission. Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. B. Tool presentations. Submissions, not exceeding four (4) pages using Springer's LNCS format, should describe the implemented tool and its novel features. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented in this conference before will be accepted only if significant and clear enhancements to the tool are reported and implemented. Information concerning the procedure for submissions is available on the conference home page http://www.dcs.warwick.ac.uk/CAV Important dates: Paper submission (strict): January 23, 2004 Notification of acceptance/rejection: March 29, 2004 Final version due: April 30, 2004 Program Chairs: Rajeev Alur, University of Pennsylvania alur(a)cis.upenn.edu Doron A. Peled, The University of Warwick doron(a)dcs.warwick.ac.uk Program Committee: Rajeev Alur, U Pennsylvania David Basin, ETH Zurich Armin Biere, ETH Zurich Randy Bryant, CMU Dennis Dams, Bell Labs Luca de Alfaro, UC Santa Cruz David Dill, Stanford U Allen Emerson, UT Austin Kousha Etessami, U of Edinburgh Steven German, IBM Rob Gerth, Intel Mike Gordon, U of Cambridge Aarti Gupta, NEC Labs Klaus Havelund, NASA Ames Holger Hermanns, Saarland U Pei-Hsin Ho, Synopsis Alan Hu, U of British Columbia Bengt Jonsson, Uppsala U Andreas Kuehlman, Cadence Labs Salvatore La Torre, U of Salerno Oded Maler, Verimag Pete Manolias, Georgia Tech Ken McMillan, Cadence Labs Anca Muscholl, U of Paris 7 Chris Myers, U of Utah Doron Peled, U of Warwick Fabio Somenzi, U of Colorado Amir Pnueli, NYU Shaz Qadeer, Microsoft Research Jun Sawada, IBM Frits Vaandrager, U of Nijmegen Pierre Wolper, U of Liege Sergio Yovine, Verimag\\[1mm] Steering Committee: Edmund M. Clarke, CMU Mike Gordon, U of Cambridge Robert P. Kurshan, Cadence Amir Pnueli, NYU

1 0

regular, geometric, and coherent categories
by John Baez 25 Oct '03

25 Oct '03

I wrote: > Here's some stuff I think I know. I know the definitions of > the above concepts, as long as I have the book open to the > right page... but I left it at home, so these could be wrong! Some were. > Cartesian categories have finite limits. Regular categories > are cartesian categories with regular epi/mono factorizations, > which must be stable under pullbacks. Fine. > Geometric categories are > regular categories admitting arbitrary unions of subobjects, > which must be stable under pullbacks. Coherent categories > are geometric categories where pullback of subobjects has a > right adjoint (which plays the role of "for all"). These were mixed up.

1 0

Upgrade of diagxy
by Michael Barr 25 Oct '03

25 Oct '03

I have just posted a minor upgrade of diagxy. At the suggestion of a graduate student at Kent State named Gerd Zeibig, I have added a new feature that allows to identify nodes of a diagram with short identifiers and then draw arrows between those nodes. He had implemented this and asked me what I thought. I found a simpler way than he (he had defined over 100 new counters and the number of counters that tex allows is 256, so they are considered a rare commodity; my code uses only 2 new counters). This kind of reintroduces the matrix mode except with absolute positioning of the vertices. The results are found, as usual, in ftp.math.mcgill.ca/pub/barr/diagxy.zip.

1 0

quantum logic
by John Baez 24 Oct '03

24 Oct '03

Dear Categorists - Do any of you know particularly insightful treatments of quantum logic via category theory? I'm more or less familiar with quantum logic as the theory of the complete orthocomplemented lattice of closed subspaces of a given Hilbert space. But now I'm interested in developing quantum logic starting as much as possible from general properties of and structures on the category of Hilbert spaces and bounded linear maps - for example, the fact that it's an abelian category, and becomes a *-category and symmetric monoidal category in a nice way (with Hilbert tensor product as the monoidal structure). And I'm interested in things like how the 2-dimensional Hilbert space acts a bit like a subobject classifier. I don't mind sticking with finite-dimensional Hilbert spaces for now to avoid certain subtleties. On a related note: I've repeatedly heard people say something like "the multiplicative fragment of linear logic is the internal logic of (closed symmetric?) monoidal categories", but I've never heard a precise result along these lines. Has anyone worked out a sufficiently general concept of "the internal logic of a category" or "the internal logic of a certain 2-category of categories" so that one could take something like a monoidal category, or a symmetric monoidal category, or a closed symmetric monoidal category - or maybe the 2-category of all such - and extract by some systematic method the corresponding "internal logic"? I'm vaguely imagining some class of generalizations of the Mitchell-Benabou language of a topos, or something like that - but I'm really interested in the nonCartesian case. The reason I ask this is that it would be nice if you could throw the (closed, symmetric, monoidal, *, etcetera...) category of Hilbert spaces into some big machine and have "quantum logic" pop out - and then throw in other similar categories, and have other kinds of logic pop out. Best, jb

8 12

QAPL 2004: Call for Papers
by Antonio Cerone 24 Oct '03

24 Oct '03

------------------------------------------------------------------------- Call for Papers ------------------------------------------------------------------------- Q A P L 2 0 0 4 ------------------------------------------------------------------------- 2nd Workshop on QUANTITATIVE ASPECTS OF PROGRAMMING LANGUAGES Barcelona - Spain 27th - 28th March, 2004 Satellite Event of ETAPS 2004 http://qapl04.di.unipi.it ------------------------------------------------------------------------- SCOPE Quantitative aspects of computation are important and sometimes essential in characterising the behaviour and determining the properties of systems. They are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, risk and trust). Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems. In particular, the workshop focuses on - the design of probabilistic and real-time languages and the definition of semantical models for such languages; - the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. security, safety, schedulability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g., worst-case memory/stack/cache requirements); - the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis); - applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues. ------------------------------------------------------------------------- TOPICS Topics include (but are not limited to) probabilistic, timing and general quantitative aspects in Language design Performance analysis Language extension Program analysis Language expressiveness Verification Hardware description languages Asynchronous hardware analysis Logic Refinement Semantics Automated reasoning Coordination models Model-checking Distributed systems Security Time-critical systems Safety Embedded systems Risk and Hazard Analysis Multi-tasking systems Scheduling theory Information systems Testing ------------------------------------------------------------------------- INVITED SPEAKERS R. Gorrieri (University of Bologna, Italy) P. Harrison (Imperial College London, UK) P. Panangaden (McGill University, Canada) W. Yi (Uppsala University, Sweden) ------------------------------------------------------------------------- SUBMISSION Authors are invited to submit papers up to 15 pages long in the ENTCS style format. Papers should clearly state the topics covered. Electronic submission is highly recommended. Detailed information is available on the web site http://qapl04.di.unipi.it. In case of problems with access to internet, it is possible to submit 3 copies of the paper to one co-chairperson of the program committee. ------------------------------------------------------------------------- IMPORTANT DATES Deadline for submission: 14 November, 2003 Notification to authors: 13 January, 2004 Final version: 13 February, 2004 Workshop: 27-28 March, 2004 ------------------------------------------------------------------------- PROCEEDINGS Accepted papers will be published in Elsevier's ENTCS (Electronic Notes in Theoretical Computer Science). Publication of a selection of the papers in a special issue of Theoretical Computer Science is currently under negotiation. ------------------------------------------------------------------------- ORGANISERS Antonio Cerone Alessandra Di Pierro School of ITEE Dipartimento di Informatica The University of Queensland University of Pisa Australia Italy Phone: +61 7 33651651 Phone: +39 050 2212779 Fax: +61 7 33651533 Fax: +39 050 2212726 ------------------------------------------------------------------------- PROGRAM COMMITTEE G. Bernat (York, UK) F. de Boer (Utrecht, The Netherlands) A. Cerone (PC co-chair) L. de Alfaro (Santa Cruz, USA) A. Di Pierro (PC co-chair) C. Fidge (Queensland, Australia) M. Gabbrielli (Bologna, Italy) M. Huth (IC London, UK) S.D. Johnson (Indiana, USA) M.Z. Kwiatkowska (Birmingham, UK) J. Ostroff (York, Canada) H. Wiklicky (IC London, UK) W. Yi (Uppsala, Sweden) ------------------------------------------------------------------------- -- Antonio Cerone antonio(a)itee.uq.edu.au School of ITEE The University of Queensland, QLD 4072 Ph. +61-7-33651651 Australia Fax +61-7-33651533

1 0

regular, geometric and coherent categories
by John Baez 23 Oct '03

23 Oct '03

Dear Categorists - In my quest to understand how various flavors of monoidal category can be seen as having various flavors of "internal language" and "internal logic", I've been enjoying the section in Johnstone's "Sketches of an Elephant" where he discusses different fragments of first-order logic and how they can be interpreted in categories with different properties. Of course, this being a book on topos theory, none of this deals with monoidal categories where the tensor product is not cartesian - my main interest, for applications to quantum logic. But, it's still lots of fun. I'd like to get a better feel for some of these things. For example, he talks about "cartesian categories" "regular categories", "geometric categories", "coherent categories" and describes which fragment of first-order logic can be interpreted in each of these things: "cartesian logic", "regular logic", "geometric logic" "coherent logic". Here's some stuff I think I know. I know the definitions of the above concepts, as long as I have the book open to the right page... but I left it at home, so these could be wrong! Cartesian categories have finite limits. Regular categories are cartesian categories with regular epi/mono factorizations, which must be stable under pullbacks. Geometric categories are regular categories admitting arbitrary unions of subobjects, which must be stable under pullbacks. Coherent categories are geometric categories where pullback of subobjects has a right adjoint (which plays the role of "for all"). I have a fairly good feel for categories with finite limits and "finite limits theories"; the others seem more mysterious to me, since I don't know enough examples illustrating the distinctions. Categories monadic over Set are regular, so AbGp is regular - but it's not coherent, since in a coherent category every morphism to the initial object is an isomorphism. What are some other examples of all these things?

1 0