February 2006 - Categories - categories.org.au

intuitionism and disjunction
by Peter Freyd 06 Mar '06

06 Mar '06

Paul Levy writes ...a model of intuitionistic logic is a *bi*cartesian closed category. I see no reason to regard disjunction as more "peripheral" to intuitionistic logic than implication. (And, likewise, no reason to regard sum types as more peripheral to simple type theory than function types.) Does anybody disagree? The original intuitionists did, of course, see such reasons. But for those who don't care about such issues as the nature of mathematical existence there's this reason: if by a *bi*cartesian closed category one were to mean a ccc category whose dual is also ccc then one would be stuck with that fact that all *bi*cartesian closed categories are just pre-ordered sets. The status of disjunction and sum types in the presence of function types is, indeed, significantly different from the status of conjunction and products types. Let me take the occasion to record a factoid I don't think I ever had an excuse to record before (and don't really have one now). Define the notion of a Heyting semi-lattice (HSL) by removing disjunction and bottom from the definition of Heyting algebra. Define a _linear_ HSL as one that satisfies the further equation ((x -> y) -> z) ^ ((y -> x) -> z) = z e.g. any linearly ordered set with top (indeed, every linear HSL is representable as a sub HSL of a product of linear ones). In a linear HSL one may construct disjunction as ((x -> y) -> y) ^ ((y -> x) -> x) The factoid of interest is this sort-of converse: the only HSL varieties in which every member is a lattice are varieties of linear HSLs.

5 8

Undirected graphs citation
by Vaughan Pratt 02 Mar '06

02 Mar '06

What would be an early reference for the representation of undirected graphs (of the set-enriched rather than {0,1}-enriched kind) as presheaves on the full subcategory 1 and 2 of Set? Vaughan Pratt

4 5

Charles Ehresmann
by Ronald Brown 28 Feb '06

28 Feb '06

This is to advertise my article: Three themes in the work of Charles Ehresmann: local-to-global; groupoids; higher dimensions. available on arXiv:math.DG/0602499 and to appear in the Proceedings of the 7th Conference on the Geometry and Topology of Manifolds: The Mathematical Legacy of Charles Ehresmann, Bedlewo 8.05.2005-15.05.2005 (Poland) Banach Centre Publications. There is a discussion on http://www.math.columbia.edu/~woit/wordpress/?p=352 Ronnie Brown www.bangor.ac.uk/r.brown

1 0

CSL'06 FINAL CALL FOR PAPERS
by Computer Science Logic '06 Conference 28 Feb '06

28 Feb '06

********************************************************************** * CSL'06 * * Annual Conference of the European Association for * * Computer Science Logic * * September 25 -- 29, 2006, Szeged, Hungary * * http://www.inf.u-szeged.hu/~csl06/ * * CALL FOR PAPERS * ********************************************************************** Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. CSL'06, the 15th annual EACSL conference will be organized by the Institute of Informatics, University of Szeged. Suggested topics of interest include: automated deduction and interactive theorem proving, constructive mathematics and type theory, equational logic and term rewriting, automata and formal logics, modal and temporal logic, model checking, logical aspects of computational complexity, finite model theory, computational proof theory, logic programming and constraints, lambda calculus and combinatory logic, categorical logic and topological semantics, domain theory, database theory, specification, extraction and transformation of programs, logical foundations of programming paradigms, verification of security protocols, linear logic, higher-order logic, nonmonotonic reasoning, logics and type systems for biology. Programme Committee: Invited speakers: Krzysztof Apt(Amsterdam/Singapore) Martin Escardo (Birmingham) Matthias Baaz (Vienna) Paul-Andre Mellies (Paris) Michael Benedikt (Chicago) Luke Ong (Oxford) Pierre-Louis Curien (Paris) Luc Segoufin (Orsay) Rocco De Nicola (Florence) Miroslaw Truszczynski(Lexington,KY) Zoltan Esik (Szeged, chair) Dov Gabbay (London) Fabio Gadducci (Pisa) Organizing Committee: Neil Immerman (Amherst) Michael Kaminski (Haifa) Bakhadyr Khoussainov (Auckland) Zoltan Esik (Szeged, co-chair) Ulrich Kohlenbach (Darmstadt) Zsolt Gazdag (Szeged) Marius Minea (Timisoara) Eva Gombas (Szeged, co-chair) Damian Niwinski (Warsaw) Szabolcs Ivan (Szeged) R. Ramanujam (Chennai) Zsolt Kakuk (Szeged) Philip Scott (Ottawa) Zoltan L. Nemeth (Szeged) Philippe Schnoebelen (Cachan) Sandor Vagvolgyi Alex Simpson (Edinburgh) (Szeged, workshop-chair) Proceedings will be published in the LNCS series. Each paper accepted by the Programme Committee must be presented at the conference by one of the authors, and final copy prepared according to Springer's guidelines. Submitted papers must be in Springer's LNCS style and of no more than 15 pages, presenting work not previously published. They must not be submitted concurrently to another conference with refereed proceedings. The PC chair should be informed of closely related work submitted to a conference or journal by 1 April, 2006. Papers authored or coauthored by members of the Programme Committee are not allowed. Submitted papers must be in English and provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewer's discretion. The title page must contain: title and author(s), physical and e-mail addresses, identification of the corresponding author, an abstract of no more than 200 words, and a list of keywords. The submission deadline is in two stages. Titles and abstracts must be submitted by 24 April, 2006 and full papers by 1 May, 2006. Notifications of acceptance will be sent by 12 June, 2006, and final versions are due 3 July, 2006. A submission server will be available from 15 March, 2006. The Ackermann Award for 2006 will be presented to the recipients at CSL'06. Important Dates: Submission - title & abstract: 24 April, 2006 - full paper: 1 May, 2006 Notification: 12 June, 2006 Final papers: 3 July, 2006 Conference address: CSL'06 c/o Prof. Zoltan Esik Institute of Informatics, University of Szeged H-6701, Szeged, P.O.B. 652, Hungary web site: http://www.inf.u-szeged.hu/~csl06/ e-mail: csl06(a)inf.u-szeged.hu phone: +36-62-544-289 or +36-62-544-205 fax: +36-62-544-895 or +36-62-546-397 ********************************************************************** **********************************************************************

1 0

Mac Lane Conference: third announcement
by Eugenia Cheng 28 Feb '06

28 Feb '06

Dear All, This is the third announcement for the conference in memory of Saunders Mac Lane, at the University of Chicago, April 7 through April 11 2006. To register, please send an e-mail to Eugenia Cheng at the above address. ACCOMMODATION DEADLINE Please note the approaching deadline: special room rates at the Ramada are available until March 6. Note that cancellation incurs no fee provided you give at least 24 hours' notice. The phone number is +1-773-288-5800; apologies for the error in the previous announcement. For further information including updated travel information, current list of participants and previous announcements please see http://www.math.uchicago.edu/~eugenia/maclane We look forward to seeing you in April. With best regards, The organisers Peter May Eugenia Cheng

1 0

CFP: LFMTP 2006
by Alberto Momigliano 28 Feb '06

28 Feb '06

----------------------------------------------------------------------- International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06) http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html Affiliated with LICS and IJCAR at FLOC'06 Seattle, Washington, 16 August, 2006. CALL FOR PAPERS Important Dates: Submission deadline: 15 May 2006 Author Notification: 15 June 2006 Final Version: 15 July 2006 ----------------------------------------------------------------------- LFMTP'06 merges the International workshop on Logical Frameworks and Meta-languages (LFM) and the MERLIN workshop on MEchanized Reasoning about Languages with variable BIndingIN). Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on one hand and their applications, for example, to proof-carrying code have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss all aspects of logical frameworks. The broad subject areas of LFMTP'06 are: * The automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation. * The theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Case studies of meta-programming, and the mechanization of the (meta)theory of programming languages and calculi. Papers focusing on experiences with encoding programming languages theory and instances of proof-carrying code or proof-carrying authorization are particularly welcome. Topics include, but are not limited to: * logical framework design * meta-theoretic analysis * applications and comparative studies * implementation techniques * efficient proof representation and validation * proof-generating decision procedures and theorem provers * proof-carrying code * sub-structural frameworks * semantic foundations * methods for reasoning about logics * case studies. Invited Speaker: Gordon Plotkin (University of Edinburgh). Program Committee: Andrew Appel Princeton University Thierry Coquand Goteborg University Martin Hofmann LMU Munich Furio Honsell University of Udine Dale Miller Inria Futurs Brigitte Pientka McGill University Andrew Pitts Cambridge University Kevin Watkins Carnegie Mellon University Paper Submissions. Three categories of papers are solicited: * Category A: Detailed and technical accounts of new research: up to fifteen pages including bibliography. * Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: up to eight pages including bibliography. * Category C: System descriptions, presenting an implemented tool and its novel features: up to six pages. A demonstration is expected to accompany the presentation. Submission is electronic in postscript or PDF format. Submitted papers must conform to the ENTCS style, preferably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html Proceedings are to be published as a volume in the Electronic Notes in Theoretical Computer Science (ENTCS) series and will be available to participants at the workshop. Organizers: Brigitte Pientka Alberto Momigliano bpientka(a)cs.mcgill.ca amomigl1(a)inf.ed.ac.uk School of Computer Science LFCS, School of Informatics McGill University University of Edinburgh

1 0

WS-FM 2006 Call For Papers
by Mario Bravetti 27 Feb '06

27 Feb '06

3rd International Workshop on Web Services and Formal Methods (WS-FM 2006) 8-9 September 2006, Vienna, Austria http://cs.unibo.it/ws-fm06 Official event of "The Process Modelling Group" http://www.process-modelling-group.org Co-located with BPM 2006 4th International Conference on Business Process Management http://bpm2006.tuwien.ac.at SCOPE Web Services technology aims at providing standard mechanisms for describing the interface and the services available on the web, as well as protocols for locating such services and invoking them (e.g. WSDL, UDDI, SOAP). Innovations are mainly devoted to the definition of standards that support the specification of complex services out of simpler ones (the so called Web Service orchestration and choreography). Several proposals have been already set up: BPML, XLANG and BizTalk, WSFL, WS-BPEL, WS-CDL, etc... Formal methods, which provide formal machinery for representing and analysing the behavior of communicating concurrent/distributed systems, are playing a fundamental role in the development of such innovations. First of all they are exploited to understand the basic mechanisms (in terms of semantics) which characterize different orchestration and choreography languages and to focus on the essence of new features that are needed. Secondly they provide a formal basis for reasoning about Web Service semantics (behaviour and equivalence): e.g. for realizing registry services where retrieval is based on the meaning and behaviour of a service and not just a Web Service name. Thirdly, the studies on formal coordination paradigms can be exploited for developing mechanisms for complex run-time Web Service coordination. Finally, given the importance of critical application areas for Web Services like E-commerce, the development of the Web Service technology can certainly take advantage from formal analisys of security properties and performance in concurrency theory. The aim of the workshop is to bring together researchers working on Web Services and Formal Methods in order to facilitate fruitful collaboration in this direction of research. This, potentially, could also have a great impact on the current standardization phase of Web Service technologies. LIST OF TOPICS The topics of interest include, but are not limited to: - Protocols and standards for WS (SOAP, WSDL, UDDI, etc... ) - Languages and description methodologies for Coreography/Orchestration/Workflow (BPML, XLANG and BizTalk, WSFL, WS-BPEL, WS-CDL, YAWL, etc... ) - Coordination techniques for WS (transactions, agreement, coordination services, etc...) - Semantics-based dynamic WS discovery services (based on Semantic Web/Ontology techniques or other semantic theories) - Security, Performance Evaluation and Quality of Service of WS - Semi-structured data and XML related technologies SUBMISSIONS Submissions must be original and should not have been published previously or be under consideration for publication while being evaluated for this workshop. We encourage also the submission of tool papers, describing tools based on formal methods, to be exploited in the context of Web Services applications. Papers are to be prepared in LNCS format and must not exceed 15 pages. Accepted papers will be published in the workshop proceedings as a volume of Lecture Notes in Computer Science (LNCS). As done for previous editions of the workshop, we intend to publish a journal special issue inviting full versions of papers selected among those presented at the workshop. IMPORTANT DATES April 21, 2006: Submission deadline June 6, 2006: Notification of acceptance June 20, 2006: Camera ready September 8-9, 2006: Workshop dates PROGRAM COMMITTEE Co-Chairs Mario Bravetti University of Bologna, Italy Gianluigi Zavattaro University of Bologna, Italy Board of "The Process Modelling Group" Wil van der Aalst Eindhoven Univ.of Technology, The Netherlands Rob van Glabbeek NICTA, Sydney, Australia Keith Harrison-Broninski Role Modellers Ltd. Robin Milner Cambridge University, UK Roger Whitehead Office Futures Other PC members Marco Aiello University of Trento, Italy Farhad Arbab CWI, The Netherlands Matteo Baldoni University of Torino, Italy Jean-Pierre Banatre University of Rennes1 and INRIA, France Boualem Benatallah University of New South Wales, Australia Karthik Bhargavan Microsoft research Cambridge, UK Roberto Bruni University of Pisa, Italy Michael Butler University of Southampton, UK Fabio Casati HP Labs, USA Rocco De Nicola University of Florence, Italy Marlon Dumas Queensland University of Technology, Australia Schahram Dustdar Wien University of Technology, Austria Gianluigi Ferrari University of Pisa, Italy Jose Luiz Fiadeiro University of Leicester, UK Stefania Gnesi CNR Pisa, Italy Reiko Heckel University of Leicester, UK Kohei Honda Queen Mary, University of London, UK Nickolas Kavantzas Oracle Co., USA Leila Kloul Université de Versailles, France Cosimo Laneve University of Bologna, Italy Mark Little JBoss Inc Natalia López University Complutense of Madrid, Spain Roberto Lucchi University of Bologna, Italy Jeff Magee Imperial College London, UK Fabio Martinelli CNR Pisa, Italy Manuel Mazzara University of Bolzano, Italy Ugo Montanari University of Pisa, Italy Shin Nakajima National Institute of Informatics and JST, Japan Manuel Nunez University Complutense of Madrid, Spain Fernando Pelayo University of Castilla-La Mancha, Albacete,Spain Marco Pistore University of Trento, Italy Wolfgang Reisig Humboldt University, Berlin, Germany Vladimiro Sassone University of Southampton, UK Marjan Sirjani Tehran University, Iran Friedrich Vogt Technical University of Hamburg-Harburg, Germany Martin Wirsing Ludwig-Maximilians University Munchen, Germany

1 0

Voevodsky on the homotopy lambda calculus
by John Baez 26 Feb '06

26 Feb '06

As has already been pointed out here, Vladimir Voevodsky is giving lectures at Stanford on the "homotopy lambda calculus": http://math.stanford.edu/distinguished_voevodsky.htm Can anyone report on what he said? Phil Scott has been teaching me about the lambda calculus and related stuff. He noted that in getting a cartesian closed category from intuitionistic logic, one takes sequents Gamma |- Delta as objects and *equivalence classes* of proofs as morphisms. One needs to take equivalence classes to get composition of morphisms to be associative, etc. From an n-categorical viewpoint it's natural to avoid working with equivalence classes and instead use 2-morphisms between morphisms, like associators, and so on, thus getting a "weak cartesian closed omega-category" - a concept which, alas, has probably not been defined yet. For someone like Voevodsky it would be natural to use ideas from homotopy theory instead and define something like a "cartesian closed category up to coherent homotopy". Such a thing should be lurking in the ordinary typed lambda calculus. Is this what Voevodsky is talking about? Or...? Best, jb

3 2

CT06: Deadlines approaching!
by Robert J. MacG. Dawson 25 Feb '06

25 Feb '06

To all planning to attend CT06: Please note that the general deadline for abstracts, February 27th, is almost here. There appears to be a significant number of people intending to speak who have not yet submitted their abstracts. Legitimate submissions for the Eilenberg-Mac Lane commemorative session are welcome up to March 15th. However, we would ask people wishing to talk on a topic without particularly strong "Eilenberg-Mac Lane" connections (and category theory has taken many new directions since the heyday of our founders) not to use this as an excuse for late submission; it is not fair to the hard-worked scientific committee. Also, while the list of participants who have already booked at White Point has gratifyingly many familiar names (thank you!), we have noted that many who we expect to see in June have _not_ yet booked. The management at White Point may not be as used as we are to the categorical habit of leaving these things till the last minute, and are starting to get a little concerned, wondering if they will have to release some of the rooms in our block booking to the general public. Remember, the earlier you book, the better the choice of rooms/cabins; this will be especially true if White Point do have to release some units, when the choice available may drop sharply. With apologies, The Organizing Committee

1 0

multicategory algebras
by Urs Schreiber 24 Feb '06

24 Feb '06

Dirk Kreimer and Alain Connes have developed a Hopf algebraic description of the process of renormalization in quantum field theory. Their starting point is the definition of a certain algebra structure on the space of all (Feynman-)graphs. The definition can be found, for instance, in equation (6) of http://arxiv.org/abs/hep-th/0510202 . I suspect that this algebra is most elegantly expressed as the "multicategory algebra" of the obvious multicategory of (Feynman-)graphs. This multicategory should be the obvious slight generalization of example 4.2.14 in Tom Leinster's book http://arxiv.org/abs/math.CT/0305049 . Here by "multicategory algebra" I mean a generalization to multicategories of the concept "category algebra" or "path algebra" of an ordinary category. I.e. the algebra generated by the morphisms in the category with the product derived from the composition law in the category. (Hence, in particular I am *not* referring to the concept "algebra *for* a multicategory" as in "algebra for an operad", discussed in section 4.3 of Leinster's book.) I would think such a concept of a multicategory(-path-)algebra should exist and should be given by the obvious generalization of formula (6) in the above cited paper. This concept seems to be so natural that I expect it must have been considered before. If so, could anyone point me to relevant sources?

1 0