From MAILER-DAEMON Mon Jun 2 22:01:01 2008 Date: 02 Jun 2008 22:01:01 -0300 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1212454861@mta.ca> X-IMAP: 1207089658 0000000025 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 Tue Apr 1 19:23:23 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 01 Apr 2008 19:23:23 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jgolk-0007Ts-QE for categories-list@mta.ca; Tue, 01 Apr 2008 19:15:52 -0300 Date: Mon, 31 Mar 2008 22:50:39 -0700 From: Vaughan Pratt Reply-To: pratt@cs.stanford.edu MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: exploiting similarities and analogies Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 1 Al Vilcius wrote: > Has anyone explored, either formally or informally, the connection between > the Melzak Bypass Principle (MBP) and adjoints? Considering that Google returned 'Your search - "Melzak Bypass Principle" - did not match any documents,' the acronym might be a tad premature. But in the spirit of the question the connection I'd be tempted to make (predictably given my biases) would be with duality rather than adjunction. Thus floor: R --> Z as right adjoint to the inclusion of Z into R is a (posetal) example of adjunction (with the numerical inequalities x <= y as the morphisms) that in this case forgets the continuum structure of R, whereas duality being an involution (at least up to equivalence) necessarily retains all the categorical structure in mirror image. For example to understand finite distributive lattices, transform them to finite posets, work on them in that guise, and transform back at the end. Being a categorical duality, the resulting understanding of distributive lattices includes their homomorphisms, which under this duality become monotone functions. Complete atomic Boolean algebras are even simpler: viewed in the duality mirror they are just ordinary sets transforming by functions. Hence the homset CABA(2^X,2^Y) of complete Boolean homomorphisms from 2^X to 2^Y as complete atomic Boolean algebras is (representable as) the set X^Y of functions f:X --> Y (so for example there are 5^3 = 125 Boolean homomorphisms from 2^5 to 2^3). Likewise one can understand Boolean algebras and their homomorphisms in terms of their dual Stone spaces and continuous functions, while the self-duality of any category of finite-dimensional vector spaces over a given field is a linchpin of matrix algebra and essential to the linear algebra examples you cited for "MBP." There is such a diversity of fruitful dualities, of widely varying characters, that one despairs of finding any uniformity to them. For me this is where Chu spaces enter. What I find so appealing about Chu spaces is that they tap into a vein of uniformity running through these disparate examples whose global structure is that of *-autonomous categories, or linear logic when seen "in the light of logic." (One can view *-autonomous categories as being to *-autonomous categories of Chu spaces roughly as Boolean algebras are to fields of sets and toposes to toposes of presheaves.) All of the dualities listed above and many more can be exhibited as (usually not *-autonomous) subcategories of Chu(Set,K) for a suitable set K, with each such category and its dual connected by the self-duality of the *-autonomous category Chu(Set,K) itself. http://www.tac.mta.ca/tac/index.html#vol17 , the special issue of TAC on Chu spaces that Valeria de Paiva and I edited, conveys some of the flavor of this. Mike Barr gives a history of Chu spaces at http://www.tac.mta.ca/tac/volumes/17/1/17-01.pdf, while the preface at http://www.tac.mta.ca/tac/volumes/17/pref/17-pref.pdf supplements Mike's history and gives an overview of the papers in the volume. My 1997 Coimbra notes http://boole.stanford.edu/pub/coimbra.pdf on Chu spaces play a more introductory role (the first half anyway, the second half emphasized linear logic more than I would have if I were writing it today). The Chu space scene has been a bit quiet lately. I'm hopeful it will see a revival at some point as it's a great framework for viewing many specific dualities, as well as being a fruitful alternative to the more traditional tools of algebra and coalgebra for representational applications, see e.g. http://boole.stanford.edu/pub/seqconc.pdf . Vaughan Pratt > > The MBP (aka "the conjugacy principle" which embraces and generalizes > Jacobi inversion) Ref MR696771 > http://www.ams.org/mathscinet/pdf/696771.pdf (and no, it does not appear > in either Wikipedia or PlanetMath, yet) is somewhat heuristic in > character, suggesting : Transform the problem (T), Solve(S), Transform > back(T^1), as a "bypass" given by (T^1)ST, which looks like conjugation. > Melzak himself refers to adjoints (quite tangentially) as "being bypasses, > though dressed up and served forth exotically" p.106 ibid. (I do recall > that adjoints were generally seen as pretty exotic in the early 1970's > when I was a graduate student at UBC, to my great chagrin). [...] From rrosebru@mta.ca Wed Apr 2 20:18:15 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 02 Apr 2008 20:18:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JhC3K-0002KM-Oa for categories-list@mta.ca; Wed, 02 Apr 2008 20:07:34 -0300 Date: Wed, 2 Apr 2008 14:59:22 -0400 (EDT) Subject: categories: Re: exploiting similarities and analogies From: "Al Vilcius" To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 2 Sorry to be misleading with MBP; perhaps I should have said Melzak's "Bypass Principle", or Melzak's "Bypass" principle, rather than using the MBP abbreviation for typing convenience, because both Google and Google Scholar provide lots of relevant hits to searches without the quotes. Anyway, the basic reference I have in mind is: Z. A. Melzak, "Bypasses, A simple approach to complexity" John Wiley & Sons (1983) ISBN 0-471-86854-= X The connection with duality is very appealing, thank you, because dualities certainly offer some very profound insights. However, I have no intuition as to why an adjunction suggested by a (Melzak's) Bypass should have unit and counit as isomorphisms? Should there be a "dualizing object= " lurking about? Are there any known dualities for presheaf categories=20 Set^(C^op) where C is something simple like (1 --> 1) or (2 <-- 1 --> 2) or (1 --> 2 --> 3 <-- 1) etc. (identities omitted). What I'm looking for is a bypass for gluing presheaves. Thank you for your kind comments. ...... Al Al Vilcius Campbellville, Ontario, Canada On Tue, April 1, 2008 1:50 am, Vaughan Pratt wrote: > Al Vilcius wrote: >> Has anyone explored, either formally or informally, the connection >> between >> the Melzak Bypass Principle (MBP) and adjoints? > > Considering that Google returned 'Your search - "Melzak Bypass > Principle" - did not match any documents,' the acronym might be a tad > premature. But in the spirit of the question the connection I'd be > tempted to make (predictably given my biases) would be with duality > rather than adjunction. Thus floor: R --> Z as right adjoint to the > inclusion of Z into R is a (posetal) example of adjunction (with the > numerical inequalities x <=3D y as the morphisms) that in this case > forgets the continuum structure of R, whereas duality being an > involution (at least up to equivalence) necessarily retains all the > categorical structure in mirror image. > > For example to understand finite distributive lattices, transform them > to finite posets, work on them in that guise, and transform back at the > end. Being a categorical duality, the resulting understanding of > distributive lattices includes their homomorphisms, which under this > duality become monotone functions. Complete atomic Boolean algebras ar= e > even simpler: viewed in the duality mirror they are just ordinary sets > transforming by functions. Hence the homset CABA(2^X,2^Y) of complete > Boolean homomorphisms from 2^X to 2^Y as complete atomic Boolean > algebras is (representable as) the set X^Y of functions f:X --> Y (so > for example there are 5^3 =3D 125 Boolean homomorphisms from 2^5 to 2^3= ). > Likewise one can understand Boolean algebras and their homomorphisms > in terms of their dual Stone spaces and continuous functions, while the > self-duality of any category of finite-dimensional vector spaces over a > given field is a linchpin of matrix algebra and essential to the linear > algebra examples you cited for "MBP." > > There is such a diversity of fruitful dualities, of widely varying > characters, that one despairs of finding any uniformity to them. For m= e > this is where Chu spaces enter. What I find so appealing about Chu > spaces is that they tap into a vein of uniformity running through these > disparate examples whose global structure is that of *-autonomous > categories, or linear logic when seen "in the light of logic." (One ca= n > view *-autonomous categories as being to *-autonomous categories of Chu > spaces roughly as Boolean algebras are to fields of sets and toposes to > toposes of presheaves.) All of the dualities listed above and many mor= e > can be exhibited as (usually not *-autonomous) subcategories of > Chu(Set,K) for a suitable set K, with each such category and its dual > connected by the self-duality of the *-autonomous category Chu(Set,K) > itself. > > http://www.tac.mta.ca/tac/index.html#vol17 , the special issue of TAC o= n > Chu spaces that Valeria de Paiva and I edited, conveys some of the > flavor of this. Mike Barr gives a history of Chu spaces at > http://www.tac.mta.ca/tac/volumes/17/1/17-01.pdf, while the preface at > http://www.tac.mta.ca/tac/volumes/17/pref/17-pref.pdf supplements Mike'= s > history and gives an overview of the papers in the volume. My 1997 > Coimbra notes http://boole.stanford.edu/pub/coimbra.pdf on Chu spaces > play a more introductory role (the first half anyway, the second half > emphasized linear logic more than I would have if I were writing it > today). > > The Chu space scene has been a bit quiet lately. I'm hopeful it will > see a revival at some point as it's a great framework for viewing many > specific dualities, as well as being a fruitful alternative to the more > traditional tools of algebra and coalgebra for representational > applications, see e.g. http://boole.stanford.edu/pub/seqconc.pdf . > > Vaughan Pratt > >> >> The MBP (aka "the conjugacy principle" which embraces and generalizes >> Jacobi inversion) Ref MR696771 >> http://www.ams.org/mathscinet/pdf/696771.pdf (and no, it does not >> appear >> in either Wikipedia or PlanetMath, yet) is somewhat heuristic in >> character, suggesting : Transform the problem (T), Solve(S), Transform >> back(T^1), as a "bypass" given by (T^1)ST, which looks like >> conjugation. >> Melzak himself refers to adjoints (quite tangentially) as "being >> bypasses, >> though dressed up and served forth exotically" p.106 ibid. (I do recal= l >> that adjoints were generally seen as pretty exotic in the early 1970's >> when I was a graduate student at UBC, to my great chagrin). [...] > > > > > From rrosebru@mta.ca Wed Apr 2 20:18:15 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 02 Apr 2008 20:18:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JhC1a-00029g-Oe for categories-list@mta.ca; Wed, 02 Apr 2008 20:05:46 -0300 Date: Wed, 02 Apr 2008 17:44:05 +0200 From: Category Theory 2008 MIME-Version: 1.0 To: categories@mta.ca Subject: categories: CT08 - Registration and accommodation deadlines Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 3 - REMINDER - International Category Theory Conference 2008, June 22-28, 2008, at the=20 Universit=E9 du Littoral C=F4te d'Opale, Calais, France. Invited Speakers: Stephen Bloom (Stevens Institute of Technology, USA) Claude Cibils (Universit=E9 Montpellier 2, France) Maria Manuel Clementino (Universidade de Coimbra, Portugal) Andreas D=F6ring (Imperial College, United Kingdom) Stephen Lack (University of Western Sydney, Australia) Ross Street (Macquarie University, Australia) Walter Tholen (York University, Canada) Scientific Committee: Clemens Berger (Universit=E9 de Nice, France) Dominique Bourn (Universit=E9 du Littoral C=F4te d'Opale, France) George Janelidze (University of Cape Town, South Africa) Peter Johnstone (University of Cambridge, United Kingdom) Manuela Sobral (Universidade de Coimbra, Portugal) Robert Walters (Universit=E0 dell'Insubria, Italy) Registration is open at the web page:=20 http://www-lmpa.univ-littoral.fr/CT08/ (now also available in French) Please keep in mind that the registration fees will change after April=20 15 as follows: =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D Before April 15 Regular: 180 euros Students: 120 euros =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D From April 16 to June 1 Regular: 250 euros Students: 170 euros =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D Fees include conference documentation, a welcome reception, the=20 conference dinner, an excursion, coffee breaks and lunches at the=20 University Self-Service Restaurant. The deadline for the submission of abstracts is APRIL 15. Accommodation: special rates have been reserved for a total of one=20 hundred rooms at the hotels suggested on the CT08 website for the=20 participants at the Conference. If you wish to benefit from these=20 special rates, you have to book directly your room by APRIL 15 annd=20 mention explicitly that you are participating in CT08. We are looking forward to seeing you in Calais! The Organizing Committee, Dominique Bourn, Marino Gran and Shalom Eliahou From rrosebru@mta.ca Wed Apr 2 20:18:15 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 02 Apr 2008 20:18:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JhBzz-0001x3-1q for categories-list@mta.ca; Wed, 02 Apr 2008 20:04:07 -0300 To: LICS List From: Kreutzer + Schweikardt Subject: categories: LICS Newsletter 115 Date: Wed, 2 Apr 2008 12:38:48 +0200 (CEST) Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 4 Newsletter 115 April 1, 2008 ******************************************************************* * Past issues of the newsletter are available at http://www.informatik.hu-berlin.de/lics/newsletters/ * Instructions for submitting an announcement to the newsletter can be found at http://www.informatik.hu-berlin.de/lics/newsletters/inst.html * To unsubscribe, send an email with "unsubscribe" in the subject line to lics@informatik.hu-berlin.de ******************************************************************* TABLE OF CONTENTS * LICS 2008 MATTERS Call for Short Talks Affiliated Workshops - Submission Deadlines Preliminary Program Invited Talks - Title and Abstracts * AWARDS Beth Dissertation Prize - Call for Submissions * CONFERENCES AND WORKSHOPS FCS-ARSPA-WITS 2008 - Call for Papers LFMTP 2008 - Call for Papers PCC 2008 - Call for Papers FORMATS'08 - Second Call for Papers FMCAD 2008 - Call for Papers PerMIS'08 - Call for Papers DDBP 2008 - Call for Papers ICLP'08 - Call for Workshop Proposals * BOOK ANNOUNCEMENT Principles of Model Checking - Christel Baier and Joost-Pieter Katoen * POSITIONS POSTDOCTORAL POSITION IN DATABASE THEORY AT OXFORD UNIVERSITY FULLY FUNDED PhD STUDENTSHIPS IN INFORMATION SYSTEMS AT OXFORD LOGIC IN COMPUTER SCIENCE (LICS) 2008 Call for Short Talks Submission Deadline: April 21, 2008 * Following a now established tradition, there will be two short talk sessions during LICS 2008. You may submit a 1-2 page abstract to give a 5-10 minute talk during one of two sessions described below. You must clearly indicate which session you would like to speak at. Short talks may be trailers for longer presentations at one of the affiliated workshops, or stand entirely on their own. Abstracts are made available on the LICS website but are not published in the conference proceedings. Provocative and programmatic presentations are welcome! Note that speakers in either session must be registered for LICS or CSF. * Session 1 (Tue Jun 24): Logic and Security (joint session with CSF) Talks should be of interest to the security and logic communities, ideally building bridges or proposing new points of intersection or applications of one area in the other. * Session 2 (Thu Jun 26): Logic in Computer Science (LICS-only session) Talks can be of any topic related to logic in computer science as summarized in the LICS call for papers. * Abstracts can be submitted at http://www.easychair.org/conferences/?conf=3Dlicscsfshorts2008 Please check the appropriate box, if you would like your talk to be considered for the joint CSF/LICS session. * Important Dates Submission: April 21, 2008 Notification: April 28, 2008 * Paper submission site The URL for submitting papers is http://www.easychair.org/conferences/?conf=3Dlicscsfshorts2008. This link will bring you to a page labelled Submission Page for LICS/CSF Shorts 2008. * There are two zones: (1) Registered User and (2) New User. The first time you use the system you will have to use the New User fields. Shortly after that a password will be emailed to you. You can use this password to access the system thereafter as a registered user. * On this page you can enter the title, authors, contact author information and plain text abstract. The plain text abstract has to be under 300 words. It can be typed in directly or pasted in with a browser. You can upload your talk abstract using the web page. Using this submission system you can manage your short talk abstract submitted to LICS 2008. You can submit new papers, resubmit previously submitted papers, or change information about authors. * Abstracts for proposed short talks must be in pdf format and should be 1-2 pages long. LOGIC IN COMPUTER SCIENCE 2008 - AFFILIATED WORKSHOPS Deadlines for Submissions See http://www2.informatik.hu-berlin.de/~lics/lics08/ for links to the workshop homepages and call for papers. * FCS-ARSPA-WITS Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (L.Bauer, S.Etalle, J.den Hartog, L.Vigano) Submission deadline: April 10, 2008 (Deadline extended) * Security and Rewriting, SecRet2008 (Dan Dougherty, Santiago Escobar) Abstract Submission=09 March 31, 2008 (passed) Full Paper Submission=09 April 6, 2008 * Proof-Carrying Code (PCC08) (Ian Stark, David Aspinall) Abstract submission:=0918=09April=092008 Paper submission:=0925=09April=092008 * Intuitionist Modal Logics and Applications (IMLA08) (Valeria de Paiva, Aleks Nanevski) Paper submission: April 25, 2008 * LFMTP International Workshop on Logical Frameworks and MetaLanguages (Andreas Abel, Christian Urban) Abstracts: 14 April Submission: 21 April LOGIC IN COMPUTER SCIENCE 2008 - PRELIMINARY PROGRAM The preliminary propgram for LICS 2008 is now available at http://www.cs.cmu.edu/~fp/lics08/program.txt LOGIC IN COMPUTER SCIENCE 2008 - INVITED TALKS Title and abstracts of the invited talks at LICS 2008 are now available at http://www2.informatik.hu-berlin.de/~lics/lics08/invited08.h= tml E. W. BETH DISSERTATION PRIZE: 2008 CALL FOR SUBMISSIONS * Since 2002, FoLLI (the European Association for 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. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2007. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of the three fields of Logic, Language, and Computation. Inter-disciplinarity is an important feature of the theses competing for the E. W. Beth Dissertation Prize. * Who qualifies Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2007 and December 31st, 2007. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2007 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for 2008). Respectively, nominations of full English translations of theses originally written in other language than English and defended in 2006 and 2007 will be accepted for consideration this year, too. * Prize The prize consists of: - a certificate - a donation of 2500 euros provided by the E. W. Beth Foundation. - an invitation to submit the thesis (or a revised version of it) to 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 is available on the FoLLI site) * How to submit Only electronic submissions are accepted. 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 bethaward2008@gmail.com. Hard copy submissions are not admitted. In case of any problems with the email submission or a lack of notification within three working days after submission, nominators should write to goranko@maths.wits.ac.za or policriti@dimi.uniud.it. * Important dates Deadline for Submissions: April 30th, 2008. Notification of Decision: July 15th, 2008. * Committee : - Anne Abeill?? (Universit?? Paris 7) - Natasha Alechina (University of Nottingham) - Didier Caucal (IGM-CNRS) - Nissim Francez (The Technion, Haifa) - Valentin Goranko (chair) (University of the Witwatersrand, Johannesburg) - Alexander Koller (University of Edinburgh) - Alessandro Lenci (University of Pisa) - Gerald Penn (University of Toronto) - Alberto Policriti (Universit?? di Udine) - Rob van der Sandt (University of Nijmegen) - Colin Stirling (University of Edinburgh) FOUNDATIONS OF COMPUTER SECURITY, AUTOMATED REASONING FOR SECURITY PROTOCOL ANALYSIS AND ISSUES IN THE THEORY OF SECURITY (FCS-ARSPA-WITS 2008= ) Call for Papers * Background, aim and scope Computer security is an established field of computer science of both theoretical and practical significance. In recent years, there has been increasing interest in logic-based foundations for various methods in computer security, including the formal specification, analysis and design of security protocols and their applications, the formal definition of various aspects of security such as access control mechanisms, mobile code security and denial-of-service attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis. * WITS is the official annual workshop organised by the IFIP WG 1.7 on "Theoretical Foundations of Security Analysis and Design", established to promote the investigation on the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications. This is the eighth meeting in the series. * The workshop FCS continues a tradition, initiated with the Workshops on Formal Methods and Security Protocols (FMSP) in 1998 and 1999, then with the Workshop on Formal Methods and Computer Security (FMCS) in 2000, and finally with the LICS satellite Workshop on Foundations of Computer Security (FCS) in 2002 through 2005, of bringing together formal methods and the security community. * ARSPA is a series of workshops on Automated Reasoning for Security Protocol Analysis, bringing together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. The first two ARSPA workshops were held as satellite events of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04) and of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), respectively. * FCS and ARSPA have been joining forces since 2006: FCS-ARSPA'06 was affiliated with LICS'06, in the context of FLoC'06, and FCS-ARSPA'07 was affiliated with LICS'07 and ICALP'07. * The aim of the joint workshop FCS-ARSPA-WITS'08 is to provide a forum for continued activity in different areas of computer security, bringing computer security researchers in closer contact with the LICS community and giving LICS attendees an opportunity to talk to experts in computer security, on the one hand, and contribute to bridging the gap between logical methods and computer security foundations, on the other. * Possible topics include, but are not limited to: Automated reasoning techniques Composition issues Formal specification Foundations of verification Information flow analysis Language-based security Logic-based design Program transformation Security models Static analysis Statistical methods Tools Trust management=09for=09Access control and resource usage control Authentication Availability and denial of service Covert channels Confidentiality Integrity and privacy Intrusion detection Malicious code Mobile code Mutual distrust Privacy Security policies Security protocols * Submission Submissions should be at most 15 pages (a4paper, 11pt), including references. The cover page should include title, names of authors, co-ordinates of the corresponding author, an abstract, and a list of keywords. Submissions that are clearly too long may be rejected immediately. Additional material intended for the referees but not for publication in the final version - for example details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. Authors are invited to submit their papers electronically, as portable document format (pdf) or postscript (ps); please, do not send files fomatted for work processing packages (e.g., Microsoft Word or Wordperfect files). * The only mechanism for paper submissions is via the electronic submission web-site powered by easychair. Please, follow the instructions given there. * Important dates Papers due:=09April 10, 2008 (extended) Notification of acceptance: May 16, 2008 Final papers:=09June 01, 2008 INTERNATIONAL WORKSHOP ON LOGICAL FRAMEWORKS AND META-LANGUAGES: THEORY AND PRACTICE (LFMTP'08) http://www4.in.tum.de/~lfmtp Pittsburgh, PA, USA, 23 June 2008 Affiliated with Logic in Computer Science (LICS 2008) CALL FOR PAPERS * Important dates: Abstract submission: 14 April 2008 Paper submission: 21 April 2008 Author notification: 19 May 2008 Final version: 2 June 2008 Workshop day: 23 June 2008 * The LFMTP workshop continues 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 the one hand and their applications in for example 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 and variable binding. * The broad subject areas of LFMTP'08 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 descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory 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 - substructural frameworks - semantic foundations - methods for reasoning about logics - formal digital libraries * Program Committee: Andreas Abel (LMU Munich) Peter Dybjer (Chalmers University of Technology) Alberto Momigliano (University of Edinburgh) Brigitte Pientka (McGill University) Randy Pollack (University of Edinburgh) Carsten Schuermann (IT University of Copenhagen) Peter Sewell (University of Cambridge) Aaron Stump (Washington University) Christian Urban (TU Munich) * 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 and appendices. - 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. Authors are required to submit a paper title and a short abstract of about 100 words before submitting the paper. * Papers are to be submitted in postscript or PDF format and must conform to the ENTCS style preferably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www4.in.tum.de/~lfmtp * The organizers: Andreas Abel Christian Urban Theoretical Computer Science Institute for Computer Science Ludwig-Maximilians-University Munich Technical University of Munich Email: andreas.abel@ifi.lmu.de Email: urbanc@in.tum.de SECOND INTERNATIONAL WORKSHOP ON PROOF-CARRYING CODE (PCC 2008) Call for Papers 22 June 2008 Carnegie Mellon University Pittsburgh, Pennsylvania, USA http://workshops.inf.ed.ac.uk/pcc08/ * PCC 2008 is a joint LICS and CSF affiliated workshop on Proof-Carrying Code. * Proof-carrying code is an important and distinctive approach to enhancing trust in programs. It provides a practical framework for independent assurance of program behaviour; especially where source code is not available, or the code author and user are unknown to each other. * The workshop will address theoretical foundations of proof-carrying code as well as practical examples and work on alternative application domains. Here "proof" is construed broadly, to include not just mathematical derivations but any formal evidence that supports the static analysis of programs. That is, evidence about an intrinsic property of code and its behaviour that can be independently checked by any user, intermediary, or third party. These manifest guarantees mean that PCC raises trust in the code itself, distinct from and complementary to any existing trust in the creator of the code, the process used to produce it, or its distributor. * Topics include: - PCC addressing properties of safety, security, and correctness such as: Memory safety, information flow, declassification, resource management, access control, protocol enforcement, functional correctness. - Examples of PCC in application domains, including but not limited to: Mobile code, mobile devices, operating systems, grid computing, peer-to-peer computing, active networks, embedded systems, cloud computing, databases, e-Science. - Probabilistically-checkable proofs, zero-knowledge proofs, proof-on-demand. - Trust and policy frameworks; supporting modular and extensible systems; compositionality in code and proofs. - Certifying compilation, proof-transforming compilation, certified verifiers. - Logics and notions of certificate specific to proof-carrying frameworks. * Programme Committee * David Aspinall, University of Edinburgh (co-chair) * Gilles Barthe, INRIA Sophia-Antipolis / IMDEA Software, Madrid * Nick Benton, Microsoft Research Cambridge * Adriana Compagnoni, Stevens Institute of Technology * Karl Crary, Carnegie Mellon University * Ewen Denney, NASA Ames * Hans-Wolfgang Loidl, LMU Munich * George Necula, UC Berkeley / Rinera Networks * Ian Stark, University of Edinburgh (co-chair) * Stephanie Weirich, University of Pennsylvania * Important Dates Abstract submission:=0918=09April=092008 Paper submission:=0925=09April=092008 Author notification:=0923=09May=092008 Final versions:=097=09June=092008 Workshop:=09=0922=09June=092008 Submission * Papers should be in the form of a PDF file using the ENTCS style and must not exceed 15 pages. Submission is via the EasyChair system. Links: ENTCS style http://www.entcs.org/ EasyChair submission page http://www.easychair.org/conferences/?conf=3Dpcc08 * All submissions will be reviewed by the programme committee. There will be an informal proceedings distributed at the workshop, with final proceedings to appear as a volume of ENTCS. * Organisers David Aspinall and Ian Stark Laboratory for Foundations of Computer Science School of Informatics The University of Edinburgh 6TH INTERNATIONAL CONFERENCE ON FORMAL MODELLING AND ANALYSIS OF TIMED SYSTEMS (FORMATS'08) Saint-Malo, France, September 15--17, 2008 (Co-Located with QEST'08 : www.qest.org) http://formats08.inria.fr * Submission Deadline : **May 12th**, 2008 Submission is now open http://www.easychair.org/conferences/?conf=3Dformats08 * Objectives and Scope of the Conference Timing aspects of systems from a variety of computer science domains have been treated independently by different communities. Researchers interested in semantics, verification and performance analysis study models such as timed automata and timed Petri nets. The digital design community focuses on propagation and switching delays while designers of embedded controllers have to take account of the time taken by controllers to compute their responses after sampling the environment. Timing related questions in these separate disciplines do have their particularities. However, there is a growing awareness that there are basic problems that are common to all of them. In particular, all these sub-disciplines treat systems whose behaviour depends upon combinations of logical and temporal constraints; namely, constraints on the temporal distances between occurrences of events. The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share interests in modelling and analysis of timed systems. Typical topics include (but are not limited to): - Foundations and Semantics: Theoretical foundations of timed systems and languages; comparison between different models (timed automata, timed Petri nets, hybrid automata, timed process algebra, max-plus algebra, probabilistic models). - Methods and Tools: techniques, algorithms, data structures, and software tools for analyzing timed systems and resolving temporal constraints (scheduling, worst-case execution time analysis, optimisation, model-checking, testing, constraint solving, etc). - Applications: adaptation and specialization of timing technology in application domains in which timing plays an important role (real-time software, hardware circuits, and problems of scheduling in manufacturing and telecommunication). * Submission and Publication: The proceedings of FORMATS'08 will be published by Springer in the Lecture Notes in Computer Scienceseries. Papers must contain original contributions, be clearly written, and include appropriate references to and comparison with related work. Simultaneous submission to other conferences with published proceedings is not allowed. Submissions should not exceed 15 pages, and should be formatted according to Springer LNCS guidelines. If necessary, the submission may be supplemented with a clearly marked appendix, which will be reviewed at the discretion of the program committee. * Program Committee: - Eug=C3=A8ne Asarin, LIAFA, Univ. Paris 7 and CNRS, France - Patricia Bouyer, CNRS, LSV, France - Ed Brinksma, ESI, Univ. of Twente & Eindhoven Univ. of Technology, The Netherlands - Franck Cassez, CNRS/IRCCyN, Nantes, France - Flavio Corradini, Univ. Camerino, Italy - Deepak D'Souza, CSA, IISc, Bangalore, India - Martin Fr=C3=A4nzle, Univ. of Oldenbourg, Germany - Goran Frehse, Univ. Grenoble 1, Verimag, France - Claude Jard, ENS Cachan/IRISA, Rennes, France - Joost-Pieter Katoen RWTH Aachen Univ., Germany - Bruce Krogh, CMU, USA - Salvatore La Torre, Univ. of Salerno, Italy - Insup Lee, Univ. of Pennsylvania, USA - Rupak Majumdar, UCLA, USA - Brian Nielsen, CISS & Aalborg Univ., Denmark - Jo=C3=ABl Ouaknine, Oxford Univ., UK - Paritosh Pandya, TIFR, Bombay, India - Paul Pettersson, M=C3=A4lardalen Univ., Sweden - Jean-Fran=C3=A7ois Raskin, ULB, Belgium - P.S. Thiagarajan, National Univ. of Singapore - Stavros Tripakis, Cadence Research Labs and Verimag/CNRS, Berkeley, USA - Frits Vaandrager, Radboud Univ. Nijmegen, The Netherlands - Farn Wang, National Taiwan Univ., Taiwan - Wang Yi, Uppsala Univ., Sweden - Tomohiro Yoneda, NII, Tokyo, Japan * Chairs: - Franck Cassez (CNRS/IRCCyN, Nantes, France) - Claude Jard (ENS Cachan/IRISA, Rennes, France) * Important Dates: - Submission Deadline: May 12th, 2008 - Notification: June 23rd, 2008 INTERNATIONAL CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2008) Call for Papers http://fmcad.org/2008 November 17-18, 2008 Embassy Suites Portland--Downtown Portland, Oregon * Important Dates (firm) Paper Submission Deadline: May 12, 2008 Author Feedback: June 19-22, 2008 Acceptance Notification: July 3, 2008 Final Version Due: August 17, 2008 (To be confirmed) Early Registration Deadline: October 14, 2008 Hotel Registration Deadline: October 17, 2008 (To be confirmed) * SCOPE OF CONFERENCE FMCAD 2008 is the eighth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. In 2005, the bi-annual FMCAD and sister conference CHARME decided to merge to form an annual conference with a unified community. The resulting unified FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for formally reasoning about computing systems, as well as open challenges therein. Topics of interest for the technical program include, but are not limited to: - Foundations: advancing industrial-strength technologies in model checking, theorem proving, equivalence checking, abstraction and refinement techniques, property-preserving reduction techniques, compositional methods, decision procedures, SAT- and BDD-based methods, combining deductive methods with decision procedures, and probabilistic methods. - Verification applications: tools, industrial experience reports, and case studies. We encourage the submission of materials relating to novel and challenging industrial-scale applications of formal methods, including problem domains where formal methods worked well or even fell short. We also encourage submissions relating to the development and execution of methodologies for formal and informal verification strategies. - Applications of formal methods in design: topics relating to the application and applicability of assertion-based verification, equivalence checking, transaction-level verification, semi-formal verification, runtime verification, simulation and testcase generation, coverage analysis, microcode verification, embedded systems, software verification, concurrent systems, timing verification, and formal approaches to performance and power. - Model-based approaches: modeling and specification languages, system-level design and verification, design derivation and transformation, and correct-by-construction methods. - Formal methods for the design and verification of emerging and novel technologies: nano, quantum, biological, video, gaming, and multimedia applications. * Paper Submission Submissions must be made electronically in PDF format through the FMCAD'08 web site, http://fmcad.org/2008. The proceedings will be published by ACM and will be available online in the ACM Digital Library and the IEEE Xplore Digital Library. Two categories of papers can be submitted: regular papers (8 pages), containing original research that has not been previously published, nor concurrently submitted for publication; and short papers (4 pages), describing applications, case studies, industrial experience reports, emerging results, or implemented tools with novel features. Regular and short papers must use the IEEE Transactions format on letter-size paper with a 10-point font size (see http://www.ieee.org/portal/pages/pubs/transactions/stylesheets.html). We recommend that self-citations be written in the third person, though authors will be required to identify themselves on their submissions. Submissions must contain original research that has not been previously published, nor concurrently submitted for publication. Any partial overlap with any published or concurrently submitted paper must be clearly indicated. If experimental results are reported, authors are strongly encouraged to provide adequate access to their data so that results can be independently verified. A small number of accepted papers will be considered for a distinguished paper award. * Program Committee - Mark Aagaard, University of Waterloo, Canada - Jason Baumgartner, IBM Corporation, USA - Valeria Bertacco, University of Michigan, USA - Armin Biere, Johannes Kepler University, Austria - Per Bjesse, Synopsys, USA - Roderick Bloem, TU Graz, Austria - Dominique Borrione, Grenoble University, France - Gianpiero Cabodi, Politecnico di Torino, Italy - Alessandro Cimatti (co-chair), FBK-irst, Trento, Italy - Koen Claessen, Chalmers University of Technology, Sweden - Ganesh Gopalakrishnan, University of Utah, USA - Aarti Gupta, NEC Laboratories America, USA - Alan J. Hu, University of British Columbia, Canada - Robert Jones (co-chair), Intel Corp., USA - Daniel Kroening, ETH Zurich, Switzerland - Andreas Kuehlmann, Cadence Laboratories, USA - Wolfgang Kunz, University of Kaiserslautern, Germany - Shuvendu Lahiri, Microsoft, USA - Jeremy Levitt, Mentor Graphics, USA - Panagiotis Manolios, Northeastern University, USA - Andy Martin, IBM Research Division, USA - Tom Melham, Oxford University, UK - Ken McMillan, Cadence Labs, USA - John O'Leary, Intel Corp., USA - Lee Pike, Galois Inc., USA - Rajeev Ranjan, Jasper Design Automation, USA - Sandip Ray, University of Texas at Austin, USA - Fei Xie Portland State U., USA - Alper Sen, Freescale Austin, USA - Natasha Sharygina, University of Lugano, Switzerland - Eli Singerman, Intel Corp., USA - Karen Yorav, IBM Haifa Research Laboratory, Israel PERFORMANCE METRICS FOR INTELLIGENT SYSTEMS WORKSHOP (PERMIS'08) Call for Papers August 19-21, 2008 http://www.isd.mel.nist.gov/PerMIS_2008 Washington DC, U.S.A. * PerMIS'08 will be the eighth in the series that started in 2000, targeted at defining measures and methodologies of evaluating performance of intelligent systems. The workshop has proved to be an excellent forum for discussions and partnerships, dissemination of ideas, and future collaborations in an informal setting. Attendees usually include researchers, graduate students, practitioners from industry, academia, and government agencies. * PerMIS'08 aims at identifying and quantifying contributions of functional intelligence towards achieving success. Our working definition of functional intelligence is the ability to act appropriately in an uncertain environment, where appropriate action is that which increases the probability of success, and success is the achievement of behavioral goals (J. Albus, 1991). In addition to the main theme, as in previous years, the workshop will focus on applications of performance measures to practical problems in commercial, industrial, homeland security, and military applications. * Topic areas include, but are not limited to: - Defining and measuring aspects of a system: The level of autonomy Human-robot interaction Collaboration & Coordination Taxonomies - Evaluating components within intelligent systems: Sensing and perception Knowledge representation, world models, ontologies Planning and control Learning and adapting Reasoning - Infrastructural support for performance evaluation: Testbeds and competitions for intercomparisons Instrumentation and other measurement tools Simulation and modeling support - Technology readiness measures for intelligent systems - Applied performance measures in various domains, e.g., Intelligent transportation systems Emergency response robots (search and rescue, bomb disposal) Homeland security systems De-mining robots Defense robotics Hazardous environments (e.g., nuclear remediation) Industrial and manufacturing systems Space/Aerial robotics Medical Robotics & assistive devices * Submission Information Prospective authors are requested to submit a draft paper (max. 8 pages) or an extended abstract (1-2 pages) for review. Invited session proposals can also be submitted as draft papers but should contain 1) a session title and a brief statement of purpose, 2) name and affiliation of the organizer(s), and 3) a preliminary list of speakers. All submissions must be written in English, starting with a succinct statement of the problem, the results achieved, their significance, and a comparison with previous work. Papers are to be submitted at www.isd.mel.nist.gov/PerMIS_2008/submission.htm/ using the specified templates. * Important Dates Submission of full papers May 29, 2008 Proposal for invited sessions June 06, 2008 Notification of acceptance June 27, 2008 Final papers due July 25, 2008 * Program Committee S. Balakirsky NIST USA R. Bostelman NIST USA F. Bonsignorio Heron Robots Italy G. Berg-Cross EM & I USA J. Bornstein ARL USA P. Courtney PerkinElmer UK J. Evans USA D. Gage XPM Tech. USA J. Gunderson GammaTwo USA L. Gunderson GammaTwo USA S.K. Gupta UMD USA A. Jacoff NIST USA S. Julier Univ. College London UK M. Lewis UPitt USA T. Kalmar-Nagy Texas A& M USA A. del Pobil Univ. Jaume-I Spain S. Ramasamy UALR USA L. Reeker NIST USA C. Schlenoff NIST USA M. Shneier NIST USA E. Tunstel JHU-APL USA DDBP 2008 - 1ST INTERNATIONAL WORKSHOP ON DYNAMIC AND DECLARATIVE BUSINESS PROCESSES Call for Papers September 15/16, 2008, Munich, Germany http://www.leduotang.com/sylvain/ddbp2008/ http://www.lrz-muenchen.de/~edoc2008/ Affiliated workshop of the 12th IEEE International EDOC Conference * DESCRIPTION The capability of rapidly adapting systems and processes to an ever-changing environment to leverage existing resources has become a crucial factor of an organization's agility. The traditional approach to process management is only partially appropriate to this new context, and calls for the advent of new, dynamic business processes. Broad business policies or narrower constraints of technical nature make dynamic business process particularly suited to a declarative approach to their modelling and design. * TOPICS Topics of the workshop include but are not limited to: - Dynamic business process modelling - Implementation issues for dynamic processes - Tools for dynamic processes - Use cases of dynamic processes - Business and technical requirements for dynamic processes - Declarative model specification - Mathematical and logical foundations of declarative business processes - Formal models of declarative business processes - Monitoring of declarative business processes - Validation of declarative business processes - Tools for declarative business processes * PUBLICATION The papers accepted for the workshop will be published with their own ISBN by the IEEE in the IEEE Digital Library. * IMPORTANT DATES - Paper submission: June 13th, 2008 - Paper notification: July 18th, 2008 - Camera ready: July 28th, 2008 - Workshop: September 15th or 16th (to be confirmed) * WORKSHOP CO-CHAIRS - Dragan Gasevic, Athabasca University and Simon Fraser University, Canada - Tobias Graml, ETH Z=C3=BCrich, Switzerland - Sylvain Halle, Universit=C3=A9 du Qu=C3=A9bec =C3=A0 Montr=C3=A9al, Cana= da * PROGRAM COMMITTEE (to be completed) - Colin Atkinson, Universit=C3=A4t Mannheim, Germany - Claudio Bartolini, HP Labs Palo Alto, USA - Thomas Bauer, DaimlerChrysler Group Research and Advanced Engineering, Germany - Andrew Berry, Deontik, Australia - Kamal Bhattacharya, IBM Watson, USA - Domenico Bianculli, University of Lugano, Switzerland - Franck van Breugel, York University, Canada - Christoph Bussler, Cisco Systems, Inc, USA - Sanjay Chaudhary, Dhirubhai Ambani Institute of Information and Communication Technology, India - Marlon Dumas, University of Tartu, Estonia - Dragan Gasevic, Athabasca University, Canada - Xiang Fu, Georgia Southwestern State University, USA - Karthik Gomadam, Wright State University, USA - Guido Governatori, University of Queensland, Australia - Reiko Heckel, University of Leicester, UK - Jana Koehler, IBM Z=C3=BCrich, Switzerland - Zoran Milosevic, Deontik, Australia - Shin Nakajima, National Institute of Informatics, Japan - Leo Orbst, The MITRE Corporation, USA - Maja Pesic, Technical University of Eindhoven, The Netherlands - Manfred Reichert, University of Twente, The Netherlands - Stefanie Rinderle, Universit=C3=A4t Ulm, Germany - Florian Rosenberg, Technical University of Vienna, Austria - Shazia Sadiq, The University of Queensland, Australia - Jennifer Sampson, National ICT Australia - Biplav Srivastava, IBM India Research Lab * FURTHER INFORMATION * Detailed information can be found on the workshop webpage: http://www.leduotang.com/sylvain/ddbp2008/ 24RD INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP'08) Call for Workshop Proposals December 9-13, 2008 Udine, Italy http://iclp08.dimi.uniud.it/ * ICLP'08, the 24rd International Conference on Logic Programming, will be held in Udine (Italy), from December 9 to 13, 2008. * Workshops co-located with international conferences are one of the best venue for the presentation and discussion of preliminary work or novel ideas, and new open problems to a wide and interested audience. Co-located workshops also provide an opportunity for presenting specialized topics and opportunities for intensive discussions and project collaboration. The topics of the workshops co-located with ICLP'08 can cover any areas related to logic programming, (e.g., theory, implementation, environments, language issues, alternative paradigms, applications) including cross-disciplinary areas. However, any workshop proposal will be considered. * The format of the workshop will be decided by the workshop organizers, but ample time must be allowed for general discussion. Workshops can vary in length, but the optimal duration will be half a day or a full day. * Workshop Proposal: Those interested in organizing a workshop at ICLP'08 are invited to submit a workshop proposal. Proposals should be in English and about two pages in length. They should contain: - The title of the workshop. - A brief technical description of the topics covered by the workshop. - A discussion of the timeliness and relevance of the workshop. - A list of some related workshops held in the last years - The (preliminary) required number of half-days allotted to the workshop and an estimate of the number of expected attendees. - The names, affiliation and contact details (email, web page, phone, fax) of the workshop organizer(s) together with a designated contact person. - The previous experiences of the workshop organizing committee in workshop/conference organization. * Proposals are expected in ASCII or PDF format. All proposals should be submitted to the Workshop Chair (Tran Cao Son) by email (tson@cs.nmsu.edu) by June 2nd, 2008. * Workshop Organizers' Tasks: - Producing a "Call for Papers" for the workshop and posting it on the net and/or other means. Please provide a web page URL which can be linked into the ICLP'08 home page by July 15th, 2008. - Providing a brief description of the workshop for the conference program. - Reviewing/accepting submitted papers. - Scheduling workshop activities in collaboration with the local organizers and the workshop chair. - Sending workshop program and workshop proceedings in pdf format to the workshop chair for printing (deadline to be defined) - The use of the Computing Research Repository (CoRR) for the workshop proceedings is strongly suggested (see http://www.logicprogramming.org/ [Guidelines for electronic publishing of proceedings]) * Location: All workshops will take place in the city of Udine at the site of the main conference. See the ICLP'08 web site for location details. * Important Dates: June 2, 2008: Proposal submission deadline June 15, 2008: Notification July 15, 2008: Deadline for receipt of CFP and URL for workshop web page November 1, 2008: Deadline for preliminary proceedings December 9-13, 2008: ICLP'08 workshops * Workshop Chair: Tran Cao Son [tson AT cs dot nmsu dot edu] (www.cs.nmsu.edu/~tson) BOOK ANNOUNCEMENT: PRINCIPLES OF MODEL CHECKING by Christel Baier and Joost-Pieter Katoen MIT Press 2008, 993 pages ISBN: 978-0-262-02649-9 * Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. * The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature. * Complementary material such as slides and solutions to selected exercises will be made available to lecturers. * Foreword by Kim G. Larsen; endorsements by Moshe Vardi and Gerard Holzmann * Further information can be found at: http://mitpress.mit.edu/catalog/item/default.asp?ttype=3D2&tid=3D11481 POSTDOCTORAL POSITION IN DATABASE THEORY AT OXFORD UNIVERSITY * The Computing Laboratory has a vacancy for a postdoctoral research assistant in the area of Database Theory. The post is funded by the EPSRC Project "Schema Mappings and Services for Data Integration and Exchange" (PI Georg Gottlob). * The contract will have a duration of approximately two years, and is available from April 2008. Salary will be on the University Grade 7, (=C2=A326,666 to =C2=A332,796 p.a.) * Applicants should have, or expect shortly to obtain, a doctoral degree in computer science, mathematics, or related discipline, and should be skilled in theoretical computer science and mathematics. They should have relevant scientific publications, possess good scientific-writing skills and project management skills. * The post will require occasional travel to conferences and co-operation with partners in the EU and in America. * Application deadline: 15 April 2008. * For more details, see http://www.comlab.ox.ac.uk/news/10-full.html FULLY FUNDED PhD STUDENTSHIPS IN INFORMATION SYSTEMS AT OXFORD * The Information Systems Research Group is offering fully-funded PhD positions in Oxford University's Computing Laboratory in Information Systems. This position is not tied to a project, and any student with a strong background in theoretical computer science and an interest in information management can apply. * Research topics available include - logic and complexity: (logic and automata on trees, tractability of graph and hypergraph algorithms), - database theory (tractability in query processing, foundational and systems issues in XML query processing, data cleaning, and data integration), and - database systems (querying of social networks, information extraction, stream processing). * The studentships are fully funded *at EU fee levels* for three years from October 2008. Each includes a stipend of =C2=A312,600 per year as w= ell as provision for travel to conferences. Students who are *not* from EU countries will need supplementary funding. * Candidates must satisfy the usual requirements http://web.comlab.ox.ac.uk/oucl/prospective/dphil/dphil-criteria.pdf for doing a doctorate at Oxford. For Further Information contact Michael Benedikt (http://www.comlab.ox.ac.uk/people/Michael.Benedikt/home.html) or Georg Gottlob (http://benner.dbai.tuwien.ac.at/staff/gottlob/), who will be happy to discuss this position on an informal basis. * The deadline for applications is April 30, 2008. Interviews for qualified candidates will take place in May of 2008. To apply you need to download the University's application form from http://www.admin.ox.ac.uk/postgraduate/apply/forms/ You will need to submit references, transcript, and a statement of research interests (in the slot marked ``research proposal') with your application. Submit the form to: Mrs Julie Sheppard Secretary for Graduate Studies, Oxford University Computing Laboratory Wolfson Building, Parks Road, Oxford, OX1 3QD, UK for e-mail queries: Julie.Sheppard@comlab.ox.ac.uk From rrosebru@mta.ca Wed Apr 2 20:18:15 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 02 Apr 2008 20:18:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JhC0v-00024Y-8o for categories-list@mta.ca; Wed, 02 Apr 2008 20:05:05 -0300 Subject: categories: The Rankin Lectures 2008 From: Tom Leinster To: categories@mta.ca Content-Type: text/plain Date: Wed, 02 Apr 2008 16:39:36 +0100 Mime-Version: 1.0 Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 5 It's not category theory, but you might anyway be interested in... THE RANKIN LECTURES 2008 The Rankin Lectures 2008 will be given by John Baez (University of California, Riverside). The series title is "My Favorite Numbers" and the individual lecture titles are Mon 15 September, 4pm: "5" Wed 17 September, 4pm: "8" Fri 19 September, 4pm: "24". They will be held at the University of Glasgow, and are supported by the Glasgow Mathematical Journal Trust. Information and abstracts can be found at http://www.maths.gla.ac.uk/~tl/rankin/ If you can come, you'd be very welcome to visit for the week and chat - there should be some like-minded people about. As it's a lecture series rather than a conference, there are no travel funds and we're not organizing accommodation, but you can find practical information on visiting at www.maths.gla.ac.uk . Best wishes, Tom -- Tom Leinster From rrosebru@mta.ca Wed Apr 2 20:18:15 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 02 Apr 2008 20:18:15 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JhC4C-0002QC-4C for categories-list@mta.ca; Wed, 02 Apr 2008 20:08:28 -0300 Date: Wed, 02 Apr 2008 22:19:40 +0300 From: Jawad Abuhlail Subject: categories: AJSE-Gentle Reminder To: categories@mta.ca MIME-version: 1.0 Content-type: text/plain; charset=us-ascii Content-transfer-encoding: 7BIT Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 6 Dear Professors, This is a GENTLE REMINDER about the special theme issue "Interactions of Algebraic & Coalgebraic Structures (Theory and Applications)" of AJSE. Deadline for submissions is June 1, 2008. Your valuable contribution is highly appreciated. For more information, you may download the call for papers: http://faculty.kfupm.edu.sa/math/abuhlail/AJSE/AJSE-CallForPapers-IACS.pdf Wassalam, Jawad ----------------------------------------------------- Dr. Jawad Abuhlail Associate Professor of Algebra Dept. of Mathematics & Statistics Box # 5046, KFUPM 31261 Dhahran (KSA) Fax: +966-3-860-2340 Office: +966-3-860-4737 Home: +966-3-860-5994 Mobile: +966-55-7609357 http://faculty.kfupm.edu.sa/math/abuhlail From rrosebru@mta.ca Sat Apr 5 15:26:36 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 05 Apr 2008 15:26:36 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JiCsH-0003t8-PO for categories-list@mta.ca; Sat, 05 Apr 2008 15:12:21 -0300 Date: Thu, 3 Apr 2008 13:45:15 -0700 From: "Mike Stay" To: categories Subject: categories: symmetric monoidal closed bicategory definition? MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 7 I'm trying to find out what the appropriate definition of a symmetric monoidal closed bicategory is. Day & Street define symmetric monoidal bicategories in "Monoidal bicategories and Hopf algebroids." Has someone considered the closed case? Are there different notions of closed for a bicategory, the adjoints to tensoring with an object versus tensoring with a 1-morphism? I've been told that pseudoadjunctions are the appropriate generalization of adjunctions for the bicategory case. -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com From rrosebru@mta.ca Mon Apr 7 11:18:39 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 07 Apr 2008 11:18:39 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jiryk-0003qs-TW for categories-list@mta.ca; Mon, 07 Apr 2008 11:05:46 -0300 Date: Sun, 6 Apr 2008 21:19:17 -0700 From: "Mike Stay" To: categories Subject: categories: Re: symmetric monoidal closed bicategory definition? MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 8 On Thu, Apr 3, 2008 at 1:45 PM, Mike Stay wrote: > I'm trying to find out what the appropriate definition of a symmetric > monoidal closed bicategory is. Day & Street define symmetric monoidal > bicategories in "Monoidal bicategories and Hopf algebroids." Now that I actually have a copy of the paper, I find it's in definition 5; sorry for the noise. -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com From rrosebru@mta.ca Mon Apr 7 11:18:40 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 07 Apr 2008 11:18:40 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JiryG-0003lU-MV for categories-list@mta.ca; Mon, 07 Apr 2008 11:05:16 -0300 From: Michael Mislove To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v919.2) Subject: categories: MFPS 24 Call for Participation Date: Sun, 6 Apr 2008 21:53:24 -0500 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: RO X-Status: X-Keywords: X-UID: 9 The 24th Mathematical Foundations of Programming Semantics Conference will take place on the campus of the University of Pennsylvania from Thursday, May 22 through midday Sunday, May 25, 2008. The program includes plenary lectures by Samson Abramsky (Oxford), Luca Cardelli (Microsoft Research, Cambridge), Dusko Pavlovic (Kestrel and Oxford), Benjamin Pierce (Penn), Phil Scott (Ottawa) and James Worrell (Oxford). In addition to special sessions on Systems Biology, on Security and on Type Theory, there will be a session honoring Phil Scott on his 60th birthday year. The remainder of the program will consist of the papers accepted from those submitted for presentation at the meeting; the list of accepted papers is now available on the conference web site. In addition to MFPS 24, a Tutorial Day on Category Theory and Computer Science will take place on Wednesday, May 21. This has been organized by Phil Scott, and will have lectures by Marcelo Fiore (Cambridge), Nicola Gambino (Leicester), Pieter Hofstra (Ottawa) and Peter Selinger (Dalhousie). Detailed information about all these activities is available at the conference web site, http://www.math.tulane.edu/~mfps/mfps24.htm Registration information is also available on the web site; the deadline for reservations at the conference hotel is April 20, so we recommend those interested in attending the meeting register within the next week or so. Best regards, MIke Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== From rrosebru@mta.ca Mon Apr 7 16:22:10 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 07 Apr 2008 16:22:10 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JiwpG-0006sM-Dx for categories-list@mta.ca; Mon, 07 Apr 2008 16:16:18 -0300 Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Dedekind cuts Date: Mon, 7 Apr 2008 17:10:39 +0100 To: Categories list Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 10 Many of the accounts of Dedekind cuts that I have seen, including the original one, wave their hands in the most blatant way, especially with regard to multiplication. Nevertheless, several deep and powerful ideas have been incorporated into this theory in the course of 150 years. This posting is a summary of them, and was written in the hope that somebody might tell me who first discovered each of them. However, whilst I am always glad to receive mathematical, historical and philosophical comments from my colleagues, I would respectfully ask, on this occasion in particular, that they first check them against the actual papers that they cite, and against the bibliography of my paper with Andrej Bauer: The Dedekind Reals in Abstract Stone Duality www.PaulTaylor.EU/ASD/dedras This paper originally appeared in the proceedings of Computability and Complexity in Analysis, held in Kyoto in August 2005. It has now been accepted for a journal, and we intend to finalise it very soon. Abstract Stone Duality is a new axiomatisation of recursive general topology without set theory. In it, the Dedekind reals satisfy the Heine--Borel property ("finite open subcover" compactness of [0,1]), whereas this fails in traditional recursive analysis based on set theory. How ASD achieves this is, of course, explained in the paper, but I also gave a summary in my posting to the categories mailing list on 18 August 2007. However, this posting is about different issues, and will be expressed in traditional (set-theoretic) language. Where I have "d in D" here, in ASD it is written "delta d". Please see www.PaulTaylor.EU/ASD/dedras/classical.html for a version of this posting that includes links and mathematical symbols. It was sent to sci.math.research several weeks ago, generating some discussion of the definition of reciprocals of intervals, but not of most of the main points of history about which I wanted to ask. It did, however, lead me to the original papers about the Archimedean principle and the classical result that this follows from Dedekind completeness. I can send references to anyone who is interested in this point, or you can search for the names Stolz, Veronese, Killing, Bettazzi, Vivanti and Holder. The historical expert on this is Philip Ehrlich at the University of Ohio. DEFINITION OF A DEDEKIND CUT Dedekind originally defined a cut (D,U) as a partition of the rationals. This means that there are two representations of each rational number q as a cut, namely ({d | d <= q}, {u | u > q}) and ({d | d < q}, {u | u >= q}). This is messy, even in the classical situation, so our definition omits q in this case. Who first did this? The letters D and U stand for "down" and "up", for which they are conveniently positioned in the alphabet. For the moment, all lower case variables range over the rationals. We want to say, in a mathematically sensitive way, that D and U have no endpoints: d in D <=> Some e. (d < e) & e in D and u in U <=> Some t. (t < u) & t in U. This property is called roundedness, and I learned it in the context of continuous lattices. Where did it come from originally? D and U also need to be bounded and disjoint: Some d. d in D, Some u. u in U and d in D & u in U => d < u, although there are other ways of expressing disjointness. The final condition is the most interesting one. We want to say that D and U account for the whole line, apart from at most one point, or "almost touch". There is an order-theoretic way to say this, d < u => d in D or u in U, and an arithmetical one, eps > 0 => Some d u. d in D & u in U & u-d < eps. These properties are called locatedness. Who formulated them, particularly the first one? Was is Brouwer, perhaps? I shall return to the difference between these two notions of locatedness, but first examine some useful subsystems. ONE-SIDED REALS Although Andrej and I only set out to construct the real line itself, we found that both the construction and the applications forced us to consider other structures first. Consider D on its own, satisfying just the roundedness condition. Classically, D = {d | d < a} where a = sup D in R + {-oo, +oo}. he collection of all such D or a forms a continuous lattice, which naturally carries the Scott topology. As the set D grows, so does the extended real number a. Customarily, we use a temporal metaphor for the reals, and a vertical one for lattices, so I call D an ascending real, although it is called (I think) lower elsewhere. Similarly, U is a descending or upper real. There is a bijection between rounded lower subsets D of the rationals and of the reals, and this respects the other properties, so I shall switch between the two without comment. This bijection is essentially the idempotence of the cut construction in Dedekind's paper. An (extended) real-valued function f is called lower semicontinuous if f^-1 (a,+oo] is open for all a. I have checked the handedness of this definition with two textbooks and two websites, but who first used it? A function is lower semicontinuous iff it is continuous in the generic sense as a function to the ascending reals with the Scott topology. CONSTRUCTIVE LEAST UPPER BOUND Constructively and computationally, it is not always possible to form sup D. The supremum, if it is a real number a, is represented by a Dedekind cut ({d | d < a}, {u | u > a}). But the lower half of this must be the original D. So, I'm saying that an ascending real D need not have a descending partner U for which (D,U) is a cut. If, as is essentially the case in ASD, D and U are recursively enumerable sets of rationals, an RE set D need not have an RE complement U. Let S be any set of real numbers, and suppose that a = sup S exists as a real number. Then, as R is totally ordered, for any x < y, either x Some d' u' e' t'. [d,u]<<[d',u'] & [e,t]<<[e',t'] & [d',u']*[e',t']<<[a',z'] where [d,u] << [d',u'] means d'0 by sub-dividing [d,u] into sufficiently but finitely many parts, applying the function Moore-wise to each part, and forming the union. Where is this theorem (first) proved in the interval literature? This result is the basis of the construction of R and the proof that [d,u] is compact in ASD. BACK-TO-FRONT INTERVALS Bizarrely, it is also possible to UNDERestimate the image by considering back-to-front intervals. This was first done by E.W. Kaucher, but can anyone give me his paper or tell me his first name? It is also used to construct the existential quantifier in our paper. It does not make sense to represent Kaucher intervals as closed subspaces: we should use D and U instead, although they now overlap. DEDEKIND COMPLETENESS AND THE ARCHIMEDEAN AXIOM A total order X is Dedekind complete if every pair of subsets D, U of X that satisfies the axioms for a cut is of the form D = {d | d < a} and U = {u | u > a} for some unique a in X. Dedekind cuts of the rationals form a Dedekind complete field, ie a cut composed of real numbers defines another real number. In other words, Dedekind's construction is idempotent. Q and R are Archimedean: eps>0 => Some n:N. (n-1) eps < x < (n+1) eps. Classically, R is the only Dedekind complete ordered field, because Dedekind completeness implies the Archimedean principle. Proof: the sets D = {d | Some n:N. d < n} and U = {u | All n:N. u > n} are rounded, disjoint and order-located. They are bounded (and so form a cut) iff U is nonempty. By Dedekind completeness, the cut (D,U) corresponds to an element omega of the field. This should be the only element that lies between D and U, but omega-1 does so too. Hence U must be empty. Assuming the Archimedean principle, the two definitions of locatedness are equivalent. Who first proved these results? John Conway's system of surreal numbers tries to extend the idea of Dedekind completeness to infinities and infinitessimals. The whole system is a proper class, as is U in this proof, and so (D,U) is not a legitimate cut: Conway calls it a gap. I conjecture (and John Conway considered this plausible when I put it to him) that there is a version of his number system in which sets are replaced by RE sets, and every RE Dedekind cut represents a number, but there are also infinities and infinitessimals. Andrej and I certainly don't construct such a thing in our paper. However, we have isolated the use of the Archimedean principle, in the hope that someone in future might eliminate it. LOCATEDNESS OF THE ARITHMETIC OPERATIONS The most difficult thing to prove is always locatedness. In computational terms, when we are asked to compute the result of an operation to a certain precision, we have to ask for its arguments to the appropriate precision. For example, if we need x+y within eps, it is enough to know x and y within eps/2. However, for multiplication things are more complicated: we need to know x to within eps/|y|. This is also formulated and proved constructively in our paper. Finally, we also have a way of defining inverse functions (reciprocals, roots, powers and logarithms) that the referee considered "rather elegant". Paul Taylor pt08@PaulTaylor.EU From rrosebru@mta.ca Thu Apr 10 22:24:16 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 10 Apr 2008 22:24:16 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jk7nP-0003rA-DF for categories-list@mta.ca; Thu, 10 Apr 2008 22:11:15 -0300 Date: Thu, 10 Apr 2008 21:04:41 +0200 From: Peter Achten MIME-Version: 1.0 To: undisclosed-recipients:; Subject: categories: First Call for Participation TFP 2008, The Netherlands Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 11 FIRST CALL FOR PARTICIPATION TRENDS IN FUNCTIONAL PROGRAMMING 2008 RADBOUD UNIVERSITY NIJMEGEN, THE NETHERLANDS MAY 26-28, 2008 INVITED SPEAKER: PROF. HENK BARENDREGT http://www.st.cs.ru.nl/AFP_TFP_2008/ [ EARLY REGISTRATION CLOSES AT MONDAY APRIL 14 ] [ THIS IS THE CORRECT DATE ] The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming languages, focusing on providing a broad view of current and future trends in Functional Programming. It aspires to be a lively environment for presenting the latest research results through acceptance by extended abstracts and full papers. A formal post-symposium refereeing process selects the best articles presented at the symposium for publication in a high-profile volume. TFP 2008 is hosted by the Radboud University Nijmegen, The Netherlands, and will be held in the rural setting of Center Parcs =93Het Heijderbos=94= , Heijen (in the vicinity of Nijmegen), The Netherlands. TFP 2008 is co-located with the 6th Int=92l. Summer School on Advanced Functional Programming (AFP=9208), which is held immediately before TFP=92= 08. PROGRAM INFORMATION We have selected papers in the following themes: (*) Types (*) Applications (*) Parallellism (*) Refactoring (*) Reactive Systems (*) Memory Analysis (*) Software Construction & Program Transformation (*) Reasoning The preliminary program can be found on the site: http://www.st.cs.ru.nl/AFP_TFP_2008/documents/preliminary_program_TFP_200= 8.pdf VENUE INFORMATION TFP (and AFP) is held in The Netherlands, at Center Parcs =93Het Heijderbos=94 which is a holiday resort in the woodlands near the city of Nijmegen. We accomodate participants in DeLuxe Cottages, each of which has three separate bed-rooms, shared bathroom, toilet, kitchen, and terrace. Cottages will be shared by three participants. If you wish to reduce costs, you can choose to share a bedroom. The summer school and symposium will take place in the business center of the venue. Breakfast, lunch and diner is included within the limits of the venue. The resort features, amongst others, a sub-tropical swimming pool (free for participants), restaurants, shops, water sports lake, midget golf court, squash court, and outdoor and indoor tennis courts. Nijmegen is considered to be the oldest city of the Netherlands, being approximately 2000 years old. Nijmegen is located at the east border of the Netherlands, near Germany. Nijmegen can be reached easily from several airports such as Schiphol airport, Eindhoven airport, and D=FCsseldorf airport, as well as by train and car. Conveniently close to Center Parcs =93Het Heijderbos=94 you will find airport Weeze in Germany. The venue Center Parcs =93Het Heijderbos=94 can be reached from Nijmegen by train to Boxmeer (25 minutes). From there you will need to order a taxi. The venue can also be reached by car: parking is free for participants of AFP and TFP. SYMPOSIUM FEES TFP 2008 includes accommodation, symposium, breakfast =96 lunch =96 diner, proceedings, and social event costs. The early registration fee is =80 595; the late registration fee is =80 695. For details, we refer to the site (see above). During the social event we will visit Nijmegen and have a symposium diner at the river-side of De Waal. REGISTRATION INFORMATION Early registration is still possible until april 15 2008. Late registration opens at april 15 2008. Registration closes at may 5 2008. We can not guarantee accommodation in case you wish to register later than may 5 2008. Registration can be done on-line at the site: http://www.st.cs.ru.nl/AFP_TFP_2008/#RegistrationInformation IMPORTANT DATES (ALL 2008) Early Registration Deadline: April 14 Late Registration Opens: April 15 Late Registration Deadline: May 5 TFP Symposium: May 26-28 PROGRAMME COMMITTEE Peter Achten (co-chair) Radboud Univ. Nijmegen, NL Andrew Butterfield Trinity College, IE Manuel Chakravarty Univ. of New South Wales, AU John Clements Cal Poly State Univ., USA Matthias Felleisen Northeastern Univ., USA Jurriaan Hage Utrecht Univ., NL Michael Hanus Christian-Albrechts Univ. zu Kiel, DE Ralf Hinze Univ. of Oxford, UK Graham Hutton Univ. of Nottingham, UK Johan Jeuring Utrecht Univ., NL Pieter Koopman (co-chair) Radboud Univ. Nijmegen, NL Shriram Krishnamurthi Brown Univ., USA Hans-Wolfgang Loidl Ludwig-Maximilians Univ.M=FCnchen, DE Rita Loogen Philipps-Univ. Marburg, DE Greg Michaelson Heriot-Watt Univ., UK Marco T. Moraz=E1n (symp. chair) Seton Hall Univ., USA Sven-Bodo Scholz Univ. of Hertfordshire, UK Ulrik Schultz Univ. of Southern Denmark, DK Clara Segura Univ. Complutense de Madrid, ES Olin Shivers Northeastern Univ., USA Phil Trinder Heriot-Watt Univ., UK Varmo Vene Univ. of Tartu, EE Vikt=F3ria Zs=F3k E=F6tv=F6s Lor=E1nd Univ., HU ORGANIZATION Symposium Chair: Marco T. Moraz=E1n, Seton Hall University, USA Programme Chair: Peter Achten, Pieter Koopman, Radboud University Nijmegen, NL Treasurer: Greg Michaelson, Heriot-Watt University, UK From rrosebru@mta.ca Mon Apr 14 14:03:25 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 14 Apr 2008 14:03:25 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JlRsf-000324-Qa for categories-list@mta.ca; Mon, 14 Apr 2008 13:50:09 -0300 From: MPC'08 Organizers To: categories@mta.ca Subject: categories: [MPC'08] First call for participation Date: Mon, 14 Apr 2008 10:14:17 +0200 (CEST) Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 12 FIRST CALL FOR PARTICIPATION 9th International Conference on Mathematics of Program Construction (MPC'08= ) Marseille (Luminy), France, July 15-18th 2008 http://mpc08.lri.fr We hereby invite you to participate to the MPC (Mathematics of Program Construction) conference held from July 15th to July 18th 2008 at the International Center for Mathematical Meetings (CIRM, http://www.cirm.univ-mrs.fr/web.ang). Online registration is opened on conference web site. Dealine registration is June 1th. INVITED SPEAKERS * Ralf Hinze, University of Oxford, UK. * Greg Morrisett, Harvard University, USA * Simon Peyton-Jones, Microsoft Research Cambridge, UK PROGRAMME The preliminary programme is available on the conference web site. VENUE The conference will be held in Marseille, the second largest city in France next to Paris. Its port is the most important in France, and opens the city to the world through the Mediterranean Sea. MPC'08 will be hosted by the International Center for Mathematical Meetings. The center is located inside the Campus of Luminy Faculty. It is close to the "Calanques", an astounding wild coastline composed of creeks stretching from Marseille to Cassis. PROGRAMME COMMITTEE Christine Paulin-Mohring INRIA-Universit=E9 Paris-Sud, France (chair) Philippe Audebaud=09 Ecole Normale Sup=E9rieure Lyon, France (co-chair) Ralph-Johan Back =09 Abo Akademi University, Finland Eerke Boiten =09 University of Kent, UK Venanzio Capretta =09 University of Nijmegen, Netherlands Sharon Curtis =09 Oxford Brookes University, UK Jules Desharnais =09 Universit=E9 Laval, Qu=E9bec, Canada Peter Dybjer =09 Chalmers University of Technology, Sweden Jeremy Gibbons =09 University of Oxford, UK Lindsay Groves =09 Victoria University of Wellington, New Zealand Ian Hayes =09 University of Queensland, Australia Eric Hehner =09 University of Toronto, Canada Johan Jeuring =09 Utrecht University, Netherlands Dexter Kozen =09 Cornell University, USA Christian Lengauer =09 Universit=E4t Passau, Germany Lambert Meertens =09 University of Utrecht, Netherlands Bernhard M=F6ller =09 Universit=E4t Augsburg, Germany Carroll Morgan =09 University of New South Wales, Australia Shin-Cheng Mu =09 Academia Sinica, Taiwan Jose Nuno Oliveira =09 Universidade do Minho, Portugal Tim Sheard =09 Portland State University, USA Tarmo Uustalu =09 Institute of Cybernetics Tallin, Estonia LOCAL ORGANIZERS MPC 2008 is organized with the support of INRIA. The local organizers are Philippe Audebaud, Christine Paulin-Mohring and Marie-Ren=E9e Donnadieu. Enquiries regarding the programme (submission etc.) should be addressed to mpc08(at)lri.fr From rrosebru@mta.ca Tue Apr 15 10:17:29 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 15 Apr 2008 10:17:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jlkuo-0002cv-Pc for categories-list@mta.ca; Tue, 15 Apr 2008 10:09:39 -0300 Date: Tue, 15 Apr 2008 10:21:19 +0200 (CEST) From: Andrea Corradini To: Andrea Corradini Subject: categories: [ICGT'08 Doctoral Symposium] Call for Abstract Submissions MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 13 ================================================================= Call for Abstract Submissions ICGT 2008 Doctoral Symposium http://www.di.unipi.it/~andrea/ICGT08-DS/ An event to be held during ICGT 2008 4th International Conference on Graph Transformation Leicester (United Kingdom), September 9 - 12, 2008 ---------------------------------------------------------------------- The ICGT 2008 Doctoral Symposium will consist of some technical sessions held during the ICGT 2008 Conference, dedicated to presentations by PhD students and by young researchers who completed their doctoral studies within the past two years. ICGT 2008 aims to bring together researchers and practitioners interested in the foundations and applications of graph transformation to a variety of areas. A non-exhaustive list of topics of interest can be found on the conference web pages: Within ICGT 2008, the Doctoral Symposium will provide a unique opportunity for doctoral students and young researchers (having defended their thesis at most two years previously) to interact with established researchers of the graph transformation community and with other students. The Doctoral Symposium will be held on a date to be determined, during the regular activities of the ICGT 2008 conference. Presentations for the Doctoral Symposium will be selected by designated members of the ICGT 2008 Program Committee (see according to originality, significance, and general interest, on the basis of submitted three-pages abstracts. Accepted abstracts, revised according to the comments by the reviewers, will be included in the LNCS proceedings of the Conference. After the conference, selected authors of presentations will be invited to submit a full paper of at most 15 pages for the refereed post-proceedings of the Doctoral Symposium, which is expected to be published as a volume of the Electronic Communications of the EASST (European Association of Software Science and Technology). ---------------------------------------------------------------------- Important Dates May 20, 2008 Submission deadline for abstracts June 2, 2008 Notification of acceptance June 15, 2008 Final abstract due September 10 - 12, 2008 ICGT 2008 Conference in Leicester September 22, 2008 Invitation of full papers (for selected authors only) November 14, 2008 Submission deadline for full papers ---------------------------------------------------------------------- Submissions The abstracts must be up to three pages long including references, and should be formatted preferably using the standard Springer-Verlag LNCS style . Each abstract can be authored by a single young resarcher (a PhD student, or having defended the thesis in the last two years). The abstracts have to be submitted electronically via the EasyChair system, at the URL In the mail accompanying the submission, the author should declare either to be a PhD student, or that he/she defended the thesis not earlier than April 2006. In both cases, please indicate the name of the PhD supervisor. Full papers submitted after the invitation for the post-proceedings can be co-authored by other researchers. ---------------------------------------------------------------------- Grants Discounted fees and grants will be offered for PhD students. Details will published later. ---------------------------------------------------------------------- Organizing committe Andrea Corradini, Pisa (I) Emilio Tuosto, Leicester (UK) ---------------------------------------------------------------------- Contacts For any information about the ICGT 2008 Doctoral Symposium, feel free to contact Andrea Corradini: email: andrea@di.unipi.it, phone: +39 050 2212786. ---------------------------------------------------------------------- From rrosebru@mta.ca Tue Apr 15 10:17:29 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 15 Apr 2008 10:17:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JlkwI-0002pP-CJ for categories-list@mta.ca; Tue, 15 Apr 2008 10:11:10 -0300 Date: Tue, 15 Apr 2008 13:07:06 +0100 From: Philip Wadler MIME-Version: 1.0 To: categories@mta.ca, types Subject: categories: Equational correspondence and equational embedding Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 14 The notion of *equational correspondence* was defined by Sabry and Felleisen in their paper: Amr Sabry and Matthias Felleisen Reasoning about programs in continuation-passing style LISP and Symbolic Computation, 6(3--4):289--360, November 1993. We lay out below the definition, along with a related notion of *equational embedding*. We've seen relatively little about equational correspondence in the literature, and nothing about equational embedding. Given that these seem to be fundamental concepts, we suspect we've been looking in the wrong places. Any pointers to relevant literature would be greatly apprectiated. An *equational theory* T is a set of terms t of T, and a set of equations t =_T t' (where t, t' are terms of T). Let S, T be equational theories. We say that f : S -> T and g : T -> S constitute an *equational correspondence* between S and T if 1. g(f(s)) =_S s, for all terms s in S 2. f(g(t)) =_T t, for all terms t in T 3. s =_S s' implies f(s) =_T f(s'), for all terms s, s' in S 4. t =_T t' implies g(t) =_S g(t'), for all terms t, t' in T Let S, T be equational theories. We say that f : S -> T and g : f(S) -> S (where f(S) is the image of S under f, a subset of T) constitute an *equational embedding* between S and T if 1. g(f(s)) =_S s, for all s in S 2. s =_S s' implies f(s) =_T f(s'), for all s, s' in S It is easy to see that there is an equational embedding of S into T if and only if there is a function from S to T that preserves and reflects equations. Clearly, f and g constitute an equational correspondence between S and T if f and g constitute an equational embedding of S into T and g and f constitute an equational embedding of T into S. We conjecture that whenever there is an equational embedding of S into T and of T into S that there is an equational correspondence between S and T. This is not immediate, because one equational embedding might be given by f and g and the other by h and k, with no obvious relation between the two. As I said, any pointers to relevant literature would be greatly appreciated! Yours, -- Sam Lindley, Philip Wadler, Jeremy Yallop -- \ Philip Wadler, Professor of Theoretical Computer Science /\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From rrosebru@mta.ca Tue Apr 15 10:17:29 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 15 Apr 2008 10:17:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jlkvf-0002jz-8Y for categories-list@mta.ca; Tue, 15 Apr 2008 10:10:31 -0300 Date: Tue, 15 Apr 2008 10:39:59 +0100 From: Alex Simpson To: categories@mta.ca Subject: categories: Research Associate in Semantics of Computation MIME-Version: 1.0 Content-Type: text/plain;charset=ISO-8859-1;format="flowed" Content-Disposition: inline Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 15 Postdoctoral Research Associate in the Semantics of Computation The Laboratory for Foundations of Computer Science at the School of Informatics, University of Edinburgh invites applications for a postdoctoral research associate, tenable for up to three years, on the EPSRC-funded project "Linear Observations and Computational Effects" (EPSRC research grant EP/F042043/1). The project involves the development of category-theoretic models of computation and associated type theories, and the application of these to establishing behavioural properties of programming constructs. The successful applicant will hold a PhD in a relevant area of theoretic computer science or mathematics and will have a good knowledge of category theory and/or type theory and their computer science applications. The post will be taken up as soon as possible. Fixed Term: Up to 3 years Closing date: 30th April 2008 For more information, go to vacancy ref. 3009010 at http://www.jobs.ed.ac.uk/ -- Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://homepages.inf.ed.ac.uk/als Fax: +44 (0)131 667 7209 -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From rrosebru@mta.ca Wed Apr 16 09:36:53 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 16 Apr 2008 09:36:53 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jm6jo-0005F9-0c for categories-list@mta.ca; Wed, 16 Apr 2008 09:27:44 -0300 Date: Tue, 15 Apr 2008 12:53:55 -0300 From: Janus Subject: categories: Re: Equational correspondence and equational embedding Cc: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 16 Dear Prof. Waddler, I don't know if the following proof is correct, please, let me know if I made any mistake: By hypothesis there exists k:S->T and h:k(S)->S such that h(k(S)) =3D_S s for all s in S and s =3D_S s' implies k(s) =3D_T k(s') for all s, s= ' in S On the other hand, there exists f:T->S and g:f(T)->S such that g(f(t)) =3D_T t for all t in T and t=3D_T t' implies f(t) =3D_S f(t') for all t, t' in T Assume that there exists t in T\k(S) =3D> |T| > |S| because k is injective and S =3D dom(k). Hence, there exists t' not equal to t such that f(t) =3D_S f(t') which is absurdum. So, there not exists t in T\k(S), then T =3D k(S). So, k and k^-1 constitutes an equational correspondence. Yours, Alejandro --=20 Alejandro D=EDaz-Caro Homepage: http://www.fceia.unr.edu.ar/~diazcaro Weblog: http://computacioncuantica.exactas.org From rrosebru@mta.ca Wed Apr 16 09:36:53 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 16 Apr 2008 09:36:53 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jm6i6-00053t-KL for categories-list@mta.ca; Wed, 16 Apr 2008 09:25:58 -0300 Date: Tue, 15 Apr 2008 16:16:10 +0100 From: Robin Houston To: categories@mta.ca Subject: categories: Re: Equational correspondence and equational embedding Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 17 To my category-infected mind, it seems that what you really need is a little category theory. :-) I take it that your equations should define an equivalence relation? (It seems strange to call them 'equations' if not.) If that's right, then an "equational theory" is the same thing as an essentially-discrete category, i.e. a category that is equivalent to a discrete one, and an "equational correspondence" is an equivalence of categories. With the definition of "equational embedding" you give, your conjecture is false. For example, let the equational theories S and T each have two terms x and y, with equations x =3D_S x y =3D_S y x =3D_S y x =3D_T x y =3D_T y We can define an equational embedding S -> T by mapping both terms to x, and we can define an equational embedding T -> S by mapping x to x and y to y, but there can be no equational correspondence between S and T (since 1 !=3D 2). It would seem more natural, at least from a categorical point of view, to define an equational embedding to be a full functor, i.e. a function f: S -> T such that s =3D_S s' iff f(s) =3D_T f(s'). With that definition, your conjecture is true by the Schr=C3=B6der-Bernstein theorem. Robin From rrosebru@mta.ca Wed Apr 16 09:36:54 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 16 Apr 2008 09:36:54 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jm6hR-0004zx-C2 for categories-list@mta.ca; Wed, 16 Apr 2008 09:25:17 -0300 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: categories@mta.ca Content-Transfer-Encoding: 7bit From: Matthias Felleisen Subject: categories: Re: Equational correspondence and equational embedding Date: Tue, 15 Apr 2008 10:06:57 -0400 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 18 Phil, Amr responded with the bare facts. Here is my path of discovery, with two additional lit ptrs: John Gately was an MS student at IU working in Indiana. I suggested to him that he work out a cbv theory of combinators in the spirit of Gordon Plotkin's CBN/CBV paper in TCS(1974). I also suggested that he read Barendregt (chapter 7, with an overview in chapter 2) because it summarizes the equational correspondence I was after. John dropped out from IU but rejoined me at Rice and published a paper on his CBV CL ~ lambda_v correspondence paper at some workshop (mathematical foundations of programming languages?). Around the same time, I started Eric Crank on a correspondence between cps(\lambda_v) and lambda with the hope that a reduction rule Bruce Duba and I had played with since 1985: (\x.E[x]) M = E[M] for x not in fv(E) [beta_Omega]. While Eric preferred to switch to equational characterizations of imperative parameter passing, Amr came along and solved this puzzle. As Amr said, we tried to stay as close as possible to the source (Curry) with our write-up for LFP 1992. -- Matthias On Apr 15, 2008, at 8:07 AM, Philip Wadler wrote: > The notion of *equational correspondence* was defined by Sabry and > Felleisen in their paper: > > Amr Sabry and Matthias Felleisen > Reasoning about programs in continuation-passing style > LISP and Symbolic Computation, 6(3--4):289--360, November 1993. > > We lay out below the definition, along with a related notion of > *equational embedding*. We've seen relatively little about equational > correspondence in the literature, and nothing about equational > embedding. Given that these seem to be fundamental concepts, we > suspect we've been looking in the wrong places. Any pointers to > relevant literature would be greatly apprectiated. > > An *equational theory* T is a set of terms t of T, and a set of > equations > t =_T t' (where t, t' are terms of T). > > Let S, T be equational theories. We say that f : S -> T and g : T - > > S > constitute an *equational correspondence* between S and T if > > 1. g(f(s)) =_S s, for all terms s in S > 2. f(g(t)) =_T t, for all terms t in T > 3. s =_S s' implies f(s) =_T f(s'), for all terms s, s' in S > 4. t =_T t' implies g(t) =_S g(t'), for all terms t, t' in T > > Let S, T be equational theories. We say that f : S -> T and > g : f(S) -> S (where f(S) is the image of S under f, a subset of T) > constitute an *equational embedding* between S and T if > > 1. g(f(s)) =_S s, for all s in S > 2. s =_S s' implies f(s) =_T f(s'), for all s, s' in S > > It is easy to see that there is an equational embedding of S into T if > and only if there is a function from S to T that preserves and > reflects equations. > > Clearly, f and g constitute an equational correspondence between S and > T if f and g constitute an equational embedding of S into T and g and > f constitute an equational embedding of T into S. > > We conjecture that whenever there is an equational embedding of S into > T and of T into S that there is an equational correspondence between S > and T. This is not immediate, because one equational embedding might > be given by f and g and the other by h and k, with no obvious relation > between the two. > > As I said, any pointers to relevant literature would be greatly > appreciated! > > Yours, -- Sam Lindley, Philip Wadler, Jeremy Yallop > > -- > \ Philip Wadler, Professor of Theoretical Computer Science > /\ School of Informatics, University of Edinburgh > / \ http://homepages.inf.ed.ac.uk/wadler/ > > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > From rrosebru@mta.ca Thu Apr 17 09:34:29 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 17 Apr 2008 09:34:29 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JmTAS-0000EG-6I for categories-list@mta.ca; Thu, 17 Apr 2008 09:24:44 -0300 From: Michael Mislove To: categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v919.2) Subject: categories: MFPS 24 Second Call for Participation Date: Wed, 16 Apr 2008 14:36:02 -0500 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 19 Dear Colleagues, MFPS 14 will take place from May 22 through midday May 25 on the campus of the University of Pennsylvania, Philadelphia. The program for MFPS 24 and the affiliated Tutorial Day on Category Theory and Computer Science, which will take place on May 21, are now online. They can be found at the URL http://www.math.tulane.edu/~mfps/ mfps24.htm There is a link to the registration form for the conference that includes reserving a room at the conference hotel. PLEASE NOTE that the deadline to reserve a hotel room at the conference rate is THIS SUNDAY, APRIL 20. Best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== From rrosebru@mta.ca Fri Apr 18 16:19:11 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 18 Apr 2008 16:19:11 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JmvuK-0006Oc-Bo for categories-list@mta.ca; Fri, 18 Apr 2008 16:06:00 -0300 Date: Fri, 18 Apr 2008 14:23:14 -0400 (EDT) From: Robert Seely To: Categories List Subject: categories: Pregroups seminar, 5 May 2008, Quebec city MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 20 A single-day session of talks on the topic of pregroups and grammar has been organized by Daniela Bargelli, as part of the 75th Acfas congress in Quebec city, 5th May 2008. The program may be found on the triples homepage under "Upcoming meetings", or directly at For further information, please contact bargelld@math.mcgill.ca -= rags =- -- From rrosebru@mta.ca Sun Apr 20 10:07:44 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 20 Apr 2008 10:07:44 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JnZ2I-0006eP-NP for categories-list@mta.ca; Sun, 20 Apr 2008 09:52:50 -0300 Date: Sat, 19 Apr 2008 23:58:20 +0200 From: Thomas Hildebrandt MIME-Version: 1.0 To: fmxsocandbpm@cs.unibo.it, categories@mta.ca, prog-lang@itu.dk Subject: categories: EXPRESS'08: preliminary call for papers Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 21 Apologies for multiple copies.... ----------------------------------------------------------------- 15th International Workshop on Expressiveness in Concurrency (EXPRESS'08) August 23rd, 2008, Toronto (Canada) Affiliated to CONCUR 2008 SCOPE AND TOPICS: The EXPRESS workshops aim at bringing together researchers interested in the relations between various formal systems, particularly in the field of Concurrency. More specifically, they focus on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, rewrite systems etc.) on the basis of their relative expressive power. SUBMISSION GUIDELINES: Short papers (up to 5 pages, not included in the final proceedings) and Full papers (up to 15 pages) are accepted only in ENTCS-style. Paper submission is performed through the EXPRESS'08 EASYCHAIR server (to be opened on May, 15th). The very best papers will be invited in a special issue of the journal of Mathematical Structures in Computer Science. INVITED SPEAKERs: Michele Bugliesi, Venezia (I), joint with SecCo'08; Gianluigi Zavattaro, Bologna (I). IMPORTANT DATES: Abstract submission: June 1st, 2008 Paper submission: June 8th, 2008. Notification date: July 4th, 2008 Submission of preliminary version for the Proceedings: July 14th, 2008 Submission of final version for ENTCS: September 29th, 2008. WORKSHOP CO-CHAIRS: Daniele Gorla (Dip. di Informatica - Univ. di Roma "La Sapienza", IT) Thomas T. Hildebrandt (IT University of Copenhagen, DK) PROGRAMME COMMITTEE: Julian Bradfield, Edinburgh (UK) Daniele Gorla (co-chair), Rome (I) Thomas Hildebrandt (co-chair), Copenhagen (DK) Gethin Norman, Oxford (UK) Anna Ing=F3lfsd=F3ttir, Reykjavik (IS) Alan Jeffrey, Bell-Labs (USA) Bas Luttik, Eindhoven (NL) Sergio Maffeis, London (UK) Peter Selinger, Dalhousie (CA) Frank Valencia, Paris (F) Daniele Varacca, Paris (F) From rrosebru@mta.ca Mon Apr 21 15:17:21 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 21 Apr 2008 15:17:21 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jo0NB-0000Dt-Gj for categories-list@mta.ca; Mon, 21 Apr 2008 15:04:13 -0300 Date: Mon, 21 Apr 2008 10:44:42 +0100 From: Andrew Butterfield MIME-Version: 1.0 To: categories@mta.ca Subject: categories: UTP'08 (revised call for papers) Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 22 CALL FOR PAPERS Unifying Theories of Programming 2008 Trinity College, Dublin, Ireland September 8th--10th, 2008 https://www.cs.tcd.ie/utp08/ mailto:utp08@easychair.org ** Proceedings to be published in Springer LNCS ** Important Dates (revised) --------------- Full Paper Submission 8th May, 6am BST Author Notification 23rd June Final Paper 21st July Symposium 8th-10th September Following on the success of the first International Symposium on Unifying Theories of Programming (UTP) held at Walworth Castle in 2006, we are pleased to announce the second, to be held in Dublin in September 2008. Based on the pioneering work on unifying theories of programming of Tony Hoare, He Jifeng, and others, the aims of this Symposium series are to continue to reaffirm the significance of the ongoing UTP project, to encourage efforts to advance it by providing a focus for the sharing of results by those already actively contributing, and to raise awareness of the benefits of such unifying theoretical frameworks among the wider computer science and software engineering communities. Of particular interest is how unification may be used to meet the goals and difficulties to be encountered in the Grand Challenges of Computing, with particular reference to the UK's "GC6: Dependable Systems Evolution", its international cousin the "Verified Software Initiative", and their plan to develop a Verified Software Repository. To this end the Symposium welcomes contributions on the above themes as well as others which can be related to them. Such additional themes include, but are not limited to, relational semantics, relational algebra, healthiness conditions, normal forms, linkage of theories, algebraic descriptions, incorporation of probabilistic programming, timed calculi and object-based descriptions, as well as alternative programming paradigms such as functional, logical, data-flow, and beyond. In all cases, the UTP approach should be compared and advantages/disadvantages discussed. The proceedings will be published in Springer LNCS. Papers may be up to 20 pages (single-column) in length and should ideally be prepared using LaTeX in LNCS format and submitted as pdf files no later than 6am British Summer Time on May 8th, 2008. Paper submission and reviewing will be handled by Easychair ( http://www.easychair.org/conferences/?conf=UTP-08 ) This site is now open for submissions. After the symposium, it is anticipated that selected papers will invited for submission to a journal special issue. Invited Speakers ---------------- Jifeng He, East China Normal University, Shanghai, China Ralph-Johan Back, Abo Akademi University, Finland. Program Committee ----------------- Bernhard Aichernig, Graz University of Technology, Austria Andrew Butterfield (Chair), Trinity College Dublin, Ireland Ana Cavalcanti, University of York, UK Yifeng Chen, University of Durham, UK Steve Dunne, University of Teesside, UK Colin Fidge, Queensland University of Technology, Brisbane, Australia Jeremy Gibbons, University of Oxford, UK Lindsay Groves, Victoria University of Wellington, New Zealand Ian Hayes, University of Queensland, Australia Rick Hehner, University of Toronto, Canada Martin Henson, University of Essex, UK Arthur Hughes, Trinity College Dublin, Ireland Zhiming Liu, United Nations University, Macau David Naumann, Stevens Institute of Technology, New Jersey, US Shengchao Qin, University of Durham, UK Augusto Sampaio, Universidade Federal de Pernambuco, Brazil Jim Woodcock, University of York, UK Huibiao Zhu, East China Normal University, Shanghai, China Local Organisation ------------------ Andrew Butterfield, Arthur Hughes Pawel Gancarski From rrosebru@mta.ca Wed Apr 23 08:53:06 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 23 Apr 2008 08:53:06 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JodHH-0001Yg-3D for categories-list@mta.ca; Wed, 23 Apr 2008 08:36:43 -0300 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Content-Transfer-Encoding: quoted-printable From: lamarche Subject: categories: Finite categories and filtered colimits, Date: Mon, 21 Apr 2008 21:04:21 +0200 To: categories@mta.ca Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 23 Fellow category theorists, I'm looking for a ref for the following result: Let C be a finite category. Then TFAE -- C has colimits for all small filtered (well, directed is probably =20 better) diagrams. -- Idempotents split in C. This doesn't seem to be in Makkai-Par=E9 or Adamek-Rosicky, but surely =20= somebody must have observed this. Actually the result is a bit more =20 general since idempotents split in *any* category that has filtered =20 colimits. Thanks in advance, Fran=E7ois Lamarche From rrosebru@mta.ca Wed Apr 23 18:15:02 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 23 Apr 2008 18:15:02 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JomCn-0004Su-BD for categories-list@mta.ca; Wed, 23 Apr 2008 18:08:41 -0300 Mime-Version: 1.0 (Apple Message framework v753) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed To: categories@mta.ca Content-Transfer-Encoding: quoted-printable From: Steve Vickers Subject: categories: Re: Finite categories and filtered colimits, Date: Wed, 23 Apr 2008 14:28:16 +0100 Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 24 Dear Francois, I don't know how relevant this is to your thinking, but I thought I'd =20= mention the result is constructively false. For an example, let C be the poset with two elements b <=3D t. The only =20= idempotents are the identities on b and t, so of course they split. Let p be a truth value, and let I =3D {b} u {t | p}, an ideal (hence =20 directed) in C. If this has a colimit, then it must be either b or t. =20= The colimit is b iff not p (so I =3D {b}), and it follows that if the =20= colimit is t we have not not p. Hence existence of the colimit gives =20 (not p or not not p) for every p, which is not intuitionistically valid. In fact one way to regard the set of truth values (i.e. the subobject =20= classifier) is as the ideal completion of C. Regards, Steve. On 21 Apr 2008, at 20:04, lamarche wrote: > Fellow category theorists, > > I'm looking for a ref for the following result: > > Let C be a finite category. Then TFAE > > -- C has colimits for all small filtered (well, directed is =20 > probably better) diagrams. > > -- Idempotents split in C. > > > This doesn't seem to be in Makkai-Par=E9 or Adamek-Rosicky, but =20 > surely somebody must have observed this. Actually the result is a =20 > bit more general since idempotents split in *any* category that has =20= > filtered colimits. > > > Thanks in advance, > > Fran=E7ois Lamarche > > > > > > From rrosebru@mta.ca Mon Apr 28 18:22:27 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 28 Apr 2008 18:22:27 -0300 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jqaab-0004i9-Q6 for categories-list@mta.ca; Mon, 28 Apr 2008 18:08:45 -0300 Date: Sun, 27 Apr 2008 12:49:28 -0300 (BRT) Subject: categories: WoLLIC 2008 - Call for Participation From: ruy@cin.ufpe.br To: wollic@cin.ufpe.br MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: cat-dist@mta.ca Precedence: bulk Message-Id: Status: O X-Status: X-Keywords: X-UID: 25 [** sincere apologies for duplicates **] Call for Participation 15th Workshop on Logic, Language, Information and Computation (WoLLIC 2008) http://wollic.org/wollic2008/ Heriot-Watt University Edinburgh, Scotland July 1-4, 2008 >>>>>> SPECIAL: There will be a screening of George Csicsery's "JULIA ROBINSON AND HILBERT'S TENTH PROBLEM" http://zalafilms.com/films/juliarobinson.html with kind permission of the film director WoLLIC is an annual international forum on inter-disciplinary resear= ch involving formal logic, computing and programming theory, and natura= l language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The Fifteenth WoLLIC will be held in the campus of Heriot-Watt Univ, Edinburgh, Scotland, from July 1 to July 4, 2008. It is sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the European Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the Sociedade Brasileira de Computacao (SBC), and the Sociedade Brasileira de Logica (SBL). SCIENTIFIC PROGRAMME Research contributions will be presented on all pertinent subjects, with particular emphasis in cross-disciplinary topics: foundations o= f computing and programming; novel computation models and paradigms; broad notions of proof and belief; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection. INVITED SPEAKERS Olivier Danvy (BRICS) Anuj Dawar (Cambridge, UK) Makoto Kanazawa (Nat Inst of Informatics, Japan) Sam Lomonaco (U Maryland Baltimore) Mark Steedman (Edinburgh U) Henry Towsner (CMU) Nikolay Vereshchagin (Moscow) PROGRAMME COMMITTEE Lev Beklemishev (Utrecht) Eli Ben-Sasson (Technion) Xavier Caicedo (U Los Andes, Colombia) Mary Dalrymple (Oxford) Martin Escardo (Birmingham) Wilfrid Hodges (Queen Mary, U London) (Chair) Achim Jung (Birmingham) Louis Kauffman (Maths, U Ill at Chicago) Ulrich Kohlenbach (Darmstadt) Leonid Libkin (Edinburgh U) Giuseppe Longo (Ecole Normal Superieure, Paris) Michael Moortgat (Utrecht) Valeria de Paiva (PARC, USA) Andre Scedrov (Maths, U Penn) Valentin Shehtman (Inst for Information Transmission Problems, Mosco= w) Joe Wells (Heriot-Watt U, Scotland) ORGANISING COMMITTEE Mauricio Ayala-Rincon (U Brasilia, Brazil) Fairouz Kamareddine (Heriot-Watt U, Scotland, co-chair) Anjolina de Oliveira (U Fed Pernambuco, Brazil) Ruy de Queiroz (U Fed Pernambuco, Brazil, co-chair) STEERING COMMITTEE S. Abramsky, J. van Benthem, J. Halpern, W. Hodges, D. Leivant, A. Macintyre, G. Mints, R. de Queiroz WEB PAGE wollic.org/wollic2008/ INVITED TALKS Inter-Deriving Semantic Artifacts for Object-Oriented Programming Olivier Danvy and Jaco Johannsen On the Descriptive Complexity of Linear Algebra Anuj Dawar Talks on Quantum Computing Sam Lomonaco On game semantics of the affine and intuitionistic logics Ilya Mezhirov and Nikolay Vereshchagin CONTRIBUTED TALKS Conjunctive Grammars and Alternating Pushdown Automata Tamar Aizikowitz and Michael Kaminski Expressive Power and Decidability for Memory Logics Carlos Areces, Diego Figueira, Santiago Figueira and Sergio Mera Reasoning with Uncertainty by Nmatrix-Metric Semantics Ofer Arieli and Anna Zamansky A Propositional Dynamic Logic for CCS Programs Mario Benevides and Luis Menasche Schechter Towards Ontology Evolution in Physics Alan Bundy and Michael Chan Interval Additive Generators of Interval T-Norms Gracaliz Dimuro, Benjamin Bedregal, Renata Reiser and Regivan Nunes PDL as a Logic of Belief Revision Jan van Eijck and Yanjing Wang Time Complexity and Convergence Analysis of Domain Theoretic Picard Method Amin Farjudian and Michal Konecny Matching and Alpha-Equivalence for Nominal Terms with Variables and Permutations Christophe Calves and Maribel Fernandez On the formal semantics of IF-like logics Santiago Figueira, Daniel Gorin and Rafael Grimson On a graph calculus for algebras of relations Renata de Freitas, Paulo A.S. Veloso, Sheila R.M. Veloso and Petruci= o Viana One-and-a-halfth order terms: Curry-Howard and incomplete derivation= s Murdoch Gabbay and Dominic Mulligan Labelled calculi for Lukasiewicz logics Didier Galmiche and Yakoub Salhi On Characteristic Constants of Theories Defined by Kolmogorov Comple= xity Shingo Ibuka, Makoto Kikuchi and Hirotaka Kikyo An infinitely-often one-way function based on an average-case assump= tion Edward Hirsch and Dmitry Itsykson Adversary lower bounds for nonadaptive quantum algorithms Pascal Koiran, Juergen Landes Natacha Portier and Penghui Yao On Second-Order Monadic Groupoidal Quantifiers Juha Kontinen and Heribert Vollmer Using alpha-CTL to specify complex planning goals Silvio Lago Pereira and Leliane Nunes de Barros Hyperintensional Questions Carl Pollard Inference Processes for Quantified Predicate Knowledge Jeff Paris and Soroush Rafiee Rad Skolem theory and Generalized Quantifiers Livio Robaldo ---