February 2005 - Categories - categories.org.au

Announcement: TYPES Summer School, August 15 - 26
by Bengt Nordström 25 Feb '05

25 Feb '05

TYPES Summer School 2005 Proofs of Programs and Formalisation of Mathematics August 15-26 2005, Goteborg, Sweden http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/ During the last ten years major achievements have been made in using computers for interactive proof developments to produce secure software and to show interesting mathematical results. Recent major results are, for instance, the complete formalisation of a proof of the four colour theorem, and a formalisation of the prime number theorem. This two weeks' course is for postgraduate students, researchers and industrials who want to learn about interactive proof development. The present school follows the format of previous TYPES summer school (in Baastad 1993, Giens 1999, Giens 2002). There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics with relevant theoretical background. Several talks will be devoted to applications. During these two weeks we will present three proof assistants: Coq, Isabelle and Agda, which are state-of-the-art interactive theorem provers. Participants will get extensive opportunities to use the systems for developing their own proofs. No previous knowledge of type theory and lambda calculus is required. The school is organised by the TYPES working group "Types for Proofs and Programs", which is a project in the IST (Information Society Technologies) program of the European Union. A limited number of grants covering part of travel, fees and ackommodation are available. Neither participation nor grants are restricted to TYPES participants. Lecturers: --------- Jeremy Avigad, Carnegie-Mellon Connor McBride, Nottingham Yves Bertot, INRIA Sophia Alexandre Miquel, Paris 7 Thierry Coquand, Chalmers Tobias Nipkow, TU Munich Catarina Coquand, Chalmers Bengt Nordstrom, Chalmers Gilles Dowek, INRIA Futurs Erik Palmgren, Uppsala Peter Dybjer, Chalmers Christine Paulin, Paris Sud Herman Geuvers, Nijmegen Laurent Thery, INRIA Sophia John Harrison, INTEL Freek Wiedijk, Nijmegen Per Martin-Lof, Stockholm TENTATIVE PROGRAM ----------------- Introduction to Type Theory: Lambda-calculus Propositions-as-types Inductive sets and families of sets Predicative and non-predicative theories Foundations: Introduction to Systems: Coq Isabelle Agda Advanced applications and tools: Proving properties of Java programs Reasoning about Programming Languages Coinduction Correctness of floating-point algorithms Dependently typed programming: Dependently typed datastructures Compiling dependent types Formalisation of mathematics: Introduction Fundamental theorem of algebra Bishop' set theory Other examples, e.g. prime number theorem The organising committee: Andreas Abel, Ana Bove, Catarina Coquand, Thierry Coquand, Peter Dybjer and Bengt Nordstrom.

1 0

New Homology & Homotopy ?
by wlawvere＠buffalo.edu 23 Feb '05

23 Feb '05

Mike Barr's recent paper Absolute Homology (TAC 14,pp53-59) contains a very nice result. Strikingly, it is of a completely basic nature, yet seems new. Similarly, his book Acyclic Models concerns concepts partly formulated fifty yeas ago and supposedly old hat, yet demonstrates new simplifications. The point is that the foundations of homological algebra are not rigidly fixed, since new fundamental insights can be made explicit to guide teaching and research. It appears that the same is true of the foundations of homotopical algebra as well ! The recent book Homotopy Limit Functors on Model Categories and Homotopical Categories (AMS Surveys and monographs 13) by Dwyer, Hirschhorn, Kan, and Smith describes itself as "an unsuccessful attempt to give an updated account of Quillen's closed model categories". But it seems to have achieved a big simplification, in basic complications like saturation and hammock calculation. It may serve as a text for a renewed seminar for nonspecialists which tries to finally understand these matters. 25-Feb-2005 16:54:17 -0400,4056;000000000000-00000000

1 0

RTA'05: 1st Call for Participation
by Ralf Treinen 23 Feb '05

23 Feb '05

************************************ * * * RTA'05 CALL FOR PARTICIPATION * * (First CFP announcement) * * * ************************************ The 16th International Conference on REWRITING TECHNIQUES AND APPLICATIONS http://www-i2.informatik.rwth-aachen.de/RTA05/ co-located with * TLCA 7th International Conference on Typed Lambda Calculi and Applications and the workshops * RULE 6th International Workshop on Rule-Based Programming * UNIF 19th International Workshop on Unification * WRS 5th International Workshop on Reduction Strategies in Rewriting and Programming * WG 1.6 IFIP Working Group 1.6 on Term Rewriting together form the Federated Conference on Rewriting, Deduction and Programming (RDP'05). RDP'05 takes place in Nara (Japan) http://www.pref.nara.jp/nara_e/index.html in the period April 18 - April 23, 2005. Registration for RTA, TLCA and the workshops is now open ! The deadline for early registration is MARCH 31, 2005. Please visit the RTA'05 or RDP'05 website below for further information: RDP'05 http://www.kurims.kyoto-u.ac.jp/rdp05/ RTA'05 http://www-i2.informatik.rwth-aachen.de/RTA05/ INVITED TALKS of RTA 2005: * Amy Felty (Ottawa) joint with TLCA'05 * Yoshihito Toyama (Sendai) * Philip Wadler (Edinburgh) INVITED TALKS of the Anniversary Session to celebrate 20 years of RTA: * Nachum Dershowitz (Tel Aviv) * Gerard Huet (Rocquencourt) * Jean-Pierre Jouannaud (Palaiseau) For further questions please contact the conference chair: RTA'05 CONFERENCE CHAIR: Hitoshi Ohsaki AIST, Japan rta05(a)m.aist.go.jp http://staff.aist.go.jp/hitoshi.ohsaki/ 25-Feb-2005 16:54:17 -0400,1585;000000000000-00000000

1 0

Etaps Workshop on Games for Logic and Programming Languages
by Dan Ghica 21 Feb '05

21 Feb '05

This is a Call for Participation for the Workshop on Games for Logic and Programming Languages to be held at Etaps, on 2-3 April, in Edinburgh. Invited speakers are: # Luke Ong, Oxford University # Luca de Alfaro, University of California, Santa Cruz More details about the workshop, including a list of accepted contributions can be found at: http://users.ox.ac.uk/%7Ecoml0074/galop.html To register for the workshop please use the following link: https://www.etaps05.inf.ed.ac.uk/Registration -- Dr. Dan Ghica, Lecturer School of Computer Science University of Birmingham Birmingham B15 2TT mailto:D.R.Ghica@cs.bham.ac.uk http://www.cs.bham.ac.uk/~drg 21-Feb-2005 15:45:38 -0400,4578;000000000000-00000000

1 0

Beth Dissertation Price - Call for Submissions
by Carlos Areces 21 Feb '05

21 Feb '05

E. W. Beth Dissertation Prize: call for submissions. Since 2002, FoLLI (the Association of Logic, Language, and Information, www.folli.org) awards the E. W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. Submissions are invited for 2005. The prize will be awarded to the best dissertation which resulted in a Ph.D. in the year 2004. The dissertations will be judged on the impact they made in their respective fields, breadth and originality of the work, and also on the interdisciplinarity of the work. Ideally the winning dissertation will be of interest to researchers in all three fields. Who qualifies: Those who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2004 and December 31st, 2004. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. However, after a careful consideration, FoLLI has decided to accept only dissertations written in English. Prize: The prize consists of · a certificate · an invitation to present the thesis during ESSLLI 05 · a donation of 2500 euros provided by the E. W. Beth Foundation. · fee waive for ESSLLI 05 attendance · the possibility to publish the thesis (or a revised version of it) in the new series of books in Logic, Language and Information to be published by Springer-Verlag as part of LNCS or LNCS/LNAI. (Further information on this series will be posted on the FoLLI site soon.) How to submit: We only accept electronic submissions. The following documents are required: 1. the thesis in pdf or ps format (doc/rtf not accepted); 2. a ten page abstract of the dissertation in ascii or pdf format; 3. a letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded; 4. two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree. All documents must be submitted electronically to beth_award(a)dimi.uniud.it . Hard copy submissions are not admitted. If you experience any problems with the email submission or do not receive a notification from us within three working days, please write to policriti(a)dimi.uniud.it or folli(a)inf.unibz.it * Important dates: Deadline for Submissions: March 15, 2005. Notification of Decision: June 30, 2005. The prize will be officially assigned to the winner at ESSLLI'05 (http://www.macs.hw.ac.uk/esslli05/) the 17th European Summer School in Logic, Language, and Information, to be held in Edinburgh, Scotland, August 9-19, 2005. Prize winner will be expected to attend the ceremony and to give a presentation of her/his Ph.D. dissertation at ESSLLI?05. Committee · Anne Abeillé (Université Paris 7) · Johan van Benthem (University of Amsterdam) · Veronica Dahl (Simon Fraser University) · Nissim Francez (The Technion, Haifa) · Valentin Goranko (University of Johannesburg) · Alessandro Lenci (University of Pisa) · Ewa Orlowska (Institute of Telecommunications, Poland) · Gerald Penn (University of Toronto) · Alberto Policriti (chair) (Università di Udine) · Christian Retoré (Université Bordeaux 1 ) · Rob van der Sandt (University of Nijmegen) · Wolfgang Thomas (RWTH Aachen) 21-Feb-2005 15:45:38 -0400,2417;000000000000-00000000

1 0

Grassmann Review
by F W Lawvere 20 Feb '05

20 Feb '05

My review of the English translations of Grassmann's Ausdehnungslehre A1 and A2 has finally been published in Historia Mathematica, volume 32, number 1, pages 99-106. I look forward to comments. Bill ************************************************************ F. William Lawvere Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************ 21-Feb-2005 15:45:38 -0400,1348;000000000000-00000000

1 0

lax limits
by l.stramaccia 20 Feb '05

20 Feb '05

Dear Categorists, since I'm not expert in the field, I woulde like to receive lights and references on preservation of lax (co) limits by representables. In particular : Let C be a 2-category and let [C,Cat] be the 2-category of 2-functors, lax nat transformations and modifications. If {G_a}_a\in A is a diagram in [C,Cat], does the formula [C,Cat](F,lax colim G_a) ≈ lax lim [C,Cat](F,G_a) hold, for any F? Are there sensible differences for the pseudo case? thanks in advance l.stramaccia 23-Feb-2005 15:23:41 -0400,2450;000000000001-00000000

1 0

Paper Announcement
by Francois Lamarche 18 Feb '05

18 Feb '05

We would like to make the following paper announcement. Title: Constructing free Boolean Categories Authors: Francois Lamache and Lutz Strassburber This is an expanded version of our LICS’05 submission. Mistakes have been corrected and the relative emphasis of axioms has changed, but the claims are strictly identical. Abstract: By Boolean category we mean something which is to a Boolean algebra what a category is to a poset. We propose an axiomatic system for Boolean categories, which differs in several respects from the one given very recently by Fuehrmann and Pym. In particular everything is done from the start in a *-autonomous category and not a linear distributive one, which simplifies issues like the Mix rule. An important axiom, which is introduced later, is a ``graphical'' condition, which is closely related to denotational semantics and the Geometry of Interaction. Then we show that the proof net model we presented in TLCA2005 is the free ``graphical'' Boolean category in our sense. This validates our categorical axiomatization with respect to a real-life example. Another important aspect of this work is that we do not assume a-priori the existence of units in the *-autonomous categories we use. This has some retroactive interest for the semantics of linear logic, and is motivated by the properties of our TLCA proof nets with respect to units. This paper (as well as its predecessors) is available on the following pages: http://www.ps.uni-sb.de/~lutz/ http://www.loria.fr/~lamarche/ François Lamarche and Lutz Strassburger 21-Feb-2005 15:45:38 -0400,1215;000000000000-00000000

1 0

Midlands Graduate School
by Paul B Levy 18 Feb '05

18 Feb '05

uk> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=3DISO-8859-1 Content-Transfer-Encoding: 8BIT Sender: cat-dist(a)mta.ca Precedence: bulk Dear category theorists On 11-15 April, at the University of Birmingham, the Midlands Graduate School (a consortium of theoretical CS researchers at Birmingham, Nottingham, Leicester and Warwick) will be holding a spring school. It is aimed at first-year PhD students, but is open to other participants as well. http://www.cs.bham.ac.uk/~pbl/mgs/ The core courses will be Category theory, Graham Hutton Typed lambda-calculus, Paul Levy Denotational semantics, Achim Jung Students can select any combination of the following optional courses that fits the schedule. Programming stream Quantum programming, Thorsten Altenkirch Epigram, Conor McBride Functional reactive programming, Henrik Nilsson Logic and model-checking stream Modal logic, Natasha Alechina Game semantics for software verification, Dan Ghica Verifying security protocols, Mark Ryan Semantics stream Operational domain theory and topology, Mart=EDn Escard=F3 Abstract Stone duality, Paul Taylor Game semantics for software verification, Dan Ghica And all that for just =A340. University accommodation (=A325 per night) ca= n also be booked. Too much? Funding is available from EPSRC (UK) and APPSEM (EU), see http://www.cs.bham.ac.uk/~pbl/mgs/ for more details, and for a registration form. See you there Paul P.S. Students will also be able to attend a Workshop on Logic and Control on 16 April, for an additional fee. Details yet to be finalized. 18-Feb-2005 12:18:20 -0400,6577;000000000000-00000000

1 0

CFP: CONCUR 2005 - Concurrency Theory
by CONCUR 2005 Announcements 18 Feb '05

18 Feb '05

CONCUR 2005 16th International Conference on Concurrency Theory San Francisco, CA, USA, August 23-26, 2005 Call for Papers CONCUR 2005, the 16th International Conference on Concurrency Theory, will take place in San Francisco, California, on August 23-26, 2005. Eleven workshops will be held in affiliation with CONCUR 2005. Further information is available at the web site: http://www.soe.ucsc.edu/concur05/ The purpose of the CONCUR conferences is to bring together researchers working on the theory of concurrency and its applications. Submissions are solicited in all areas of semantics, logics, and verification techniques for concurrent systems. The principal topics include (but are not limited to): - Basic models and logics of concurrent and distributed computation (such as process algebras, Petri nets, domain theoretic or game theoretic models, modal and temporal logics). - Specialized models or classes of systems (such as circuits, synchronous systems, real time and hybrid systems, stochastic systems, data bases, mobile and migrating systems, parametric protocols, security protocols). - Related verification techniques and tools (such as state-space exploration, model-checking, synthesis, abstraction, automated deduction, testing). - Related programming models (such as distributed, constraints or object oriented, graph rewriting, as well as associated type systems, static analyses, abstract machines, and environments). Authors are invited to submit an extended abstract; submissions will be evaluated by the program committee for inclusion in the proceedings, which will be published by Springer-Verlag in the Lecture Notes in Computer Science series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Simultaneous submission to other conferences with published proceedings is not allowed. Authors are required to submit a paper title and a short abstract before submitting the extended abstract. The short abstract should not exceed 200 words, and it should be entered in ASCII at the conference web site. The extended abstract should not exceed 15 pages, and it should be formatted according to Springer-Verlag LNCS guidelines. If necessary, the extended abstract may be supplemented with a clearly marked appendix, which will be reviewed at the discretion of the program committee. Invited speakers: Rajeev Alur UPenn (joint CONCUR/SPIN speaker) Dawson Engler Stanford University (joint CONCUR/SPIN speaker) Christos Papadimitriou UC Berkeley Luca Cardelli Microsoft Research, Cambridge Important dates: Short Abstract Submission: March 28, 2005 Extended Abstract Submission: April 1, 2005 4pm UTC Notification: May 18, 2005 Final version due: June 8, 2005 Affiliated workshops: Eleven workshops will be affiliated with CONCUR 2005: BioCONCUR, DisCoVeri, EXPRESS, FIT, FOCLASA, GETCO, GT-VC, INFINITY, MoChArt, SecCo, and SPIN. Organisers: General chair: Luca de Alfaro Programme Committee co-chairs: Martín Abadi, Luca de Alfaro Program Committee: Martín Abadi (co-chair) UC Santa Cruz Christel Baier Universität Bonn Jos Baeten Eindhoven University of Technology Albert Benveniste IRISA/INRIA Luis Caires Universidade Nova de Lisboa Giuseppe Castagna CNRS/École Normale Supérieure Marsha Chechik University of Toronto Vincent Danos CNRS/Université Paris VII Luca de Alfaro (co-chair) University of California, Santa Cruz Javier Esparza University of Stuttgart Cédric Fournet Microsoft Research, Cambridge Dimitra Giannakopoulou NASA Ames Research Center Anna Ingólfsdóttir Aalborg University Radha Jagadeesan DePaul University Bengt Jonsson Uppsala University Antonin Kucera Masaryk University Orna Kupferman Hebrew University Cosimo Laneve Università di Bologna Kim Larsen Aalborg University John Mitchell Stanford University Ugo Montanari Università di Pisa Catuscia Palamidessi INRIA Futurs & LIX Prakash Panangaden McGill University Shaz Qadeer Microsoft Research, Redmond Vijay Saraswat IBM TJ Watson Research Lab Vladimiro Sassone University of Sussex Philippe Schnoebelen CNRS/École Normale Supérieure de Cachan Frits Vaandrager Radboud University Nijmegen Mahesh Viswanathan University of Illinois at Urbana Champaign Igor Walukiewicz Université Bordeaux Glynn Winskel University of Cambridge ---------------- CONCUR 2005 - concur05(a)soe.ucsc.edu 18-Feb-2005 12:18:20 -0400,2995;000000000001-00000000

1 0