Newsletter 89
December  5, 2003

* Past issues of the newsletter are available at
* Instructions for submitting an announcement to the newsletter
  can be found at

  LICS 2004 - Call for Papers
  ICALP 2004 - Call for Papers
  WRS'04 - Call for Papers
  CAV'04 - Call for Papers
  WITS'04 - Call for Papers
  ACSD'04 - Call for Papers
  WS-FM 2004 - Call for Papers
  CMCS'04 - Call for papers
  SEFM 2004 - Call for Papers
  MPC2004 - Call for Papers
  EWSCS'04 - Call for Participation
  Computability Theory - S. Barry Cooper
  Verification of Reactive Systems -  Klaus Schneider
  Logic for Concurrency and Synchronisation - Ruy J.G.B. de Queiroz (editor)
  Logic and Complexity - Richard Lassaigne and Michel de Rougemont
  Postdoc and PhD positions at CWI, Amsterdam

  (co-located with ICALP 2004)
  Turku, Finland, July 14-17, 2004
  Call for Papers
* The LICS Symposium is an annual international forum on theoretical and
  practical topics in computer science that relate to logic in a broad
  sense.  We invite submissions on that theme.  Suggested, but not
  exclusive, topics of interest for submissions include: automata
  theory, automated deduction, categorical models and logics,
  concurrency and distributed computation, constraint programming,
  constructive mathematics, database theory, domain theory, finite model
  theory, proof theory, formal aspects of program analysis, formal
  methods, hybrid systems, lambda and combinatory calculi, linear logic,
  logical aspects of computational complexity, logics in artificial
  intelligence, logical representation of knowledge, logics of programs,
  logic programming, modal and temporal logics, model checking,
  programming language semantics, reasoning about security, rewriting,
  specifications, type systems and type theory, and verification.
* Authors are required to submit electronically a paper title and a
  short abstract of about 100 words before submitting the extended
  abstract of the paper.
    Titles & Short Abstracts Due : January 26, 2004
    Extended Abstracts Due       : February 2, 2004
    Author Notification          : March 27, 2004
    Camera-ready Papers Due      : April 25, 2004
  All deadlines are firm; late submissions will not be considered.
  Detailed information about electronic paper submission will be posted
  at the LICS website.
* LICS 2004 will have a session of short (5--10 minutes) presentations.
  This session is intended for descriptions of work in progress, student
  projects, and relevant research being published elsewhere; other brief
  communications may be acceptable. Submissions for these presentations,
  in the form of short abstracts (1 or 2 pages long), should be entered
  at the LICS 2004 submission site between March 27th and April 4th,
  2004.  Authors will be notified of acceptance or rejection by April
  17th, 2004.
* An award in honor of the late S.C. Kleene will be given for the best
  student paper, as judged by the program committee.  For a submission
  to be eligible, the research presented in the paper must have been
  carried out while all authors were full-time students.  The program
  committee may decline to make the award or may split it among several
* As in previous years, there will be a number of workshops affiliated
  with LICS 2004; information will be posted at the LICS website.
* Program committee: Rajeev Alur, Andrew Appel, Albert Atserias,
  Franz Baader, Samuel Buss, Roberto Di Cosmo, Gilles Dowek,
  Harald Ganzinger (chair), Martin Hofmann, Achim Jung, Kim Larsen,
  Leonid Libkin, Rocco de Nicola, Damian Niwinski, Prakash Panangaden,
  Albert Rubio, Vitaly Shmatikov, Moshe Vardi, Helmut Veith,
  Andrei Voronkov
* Invited speakers:
  LICS: S. Abramsky (O. Oxford), D. Sangiorgi (U. di Bologna),
    I. Walukiewicz (U. Bordeaux),
  Joint ICALP/LICS: R. Harper (Carnegie Mellon), A. Razborov
    (Princeton & Moscow), M. Yannakakis (Stanford).

  (co-located with LICS 2004)
  Turku, Finland, July 12-16, 2004
  Call for Papers
* Papers presenting original research on all aspects of theoretical
  computer science are sought. Typical but not exclusive topics of
  interest are as follows:
    TRACK A: Algorithmic aspects of parallel and distributed
    computing; algorithms and data structures; algorithms and models
    for large networks; algorithms for computationally hard problems;
    automata theory and formal languages; bioinformatics;
    computational complexity; combinatorics and structures in Computer
    Science; cryptography; machine learning; molecular computing,
    neural and evolutionary algorithms; proof complexity; quantum
    TRACK B: Algebraic and categorical models; applications of
    automata in logic; concurrency, mobility and distributed systems;
    databases, semi-structured data and finite model theory; logics
    and their applications; principles of programming languages;
    program logics, formal methods and model checking; security
    analysis and verification; semantics of programming languages;
    specification, refinement and verification; type systems and typed
* Submissions of max 12 pages to be submitted via the conference web
  site.  Accepted papers will be published in Springer LNCS.
* Submission deadline: February 8, 2004.  Notification: March 31, 2004
* Program committees:
    TRACK A: A. Atserias, Barcelona (ES), G. Brodal, Aarhus (DK),
    J. Cassaigne, Marseille (FR), J. D?az, Barcelona (ES), chair,
    R. Fleischer, Hong Kong (HK), H. Gabow, Boulder (US), L. Goldberg,
    Warwick (UK), J. Hromkovic, Aachen (DE), G. Italiano, Roma (IT),
    T. Jiang, Riverside (US), C. Kaklamanis, Patras (GR), J. Kari,
    Turku (FI), C. Moore, Santa Fe (US), P. Pudlak, Prague (CZ),
    P. Raghavan, Verity, Stanford (US), M. Santha, Paris (FR),
    B. Voecking, Dortmund (DE), G. Woeginger, Twente (NL), M. Yung,
    Columbia U. (US).
    TRACK B: R.-J. Back, Turku (FI), P.-L. Curien, Paris (FR),
    A. Gordon, Microsoft, Cambridge (UK), S. Hayashi, Kobe (JP),
    T. Henzinger, Berkeley (US), M. Hofmann, Munich (DE), B. Jacobs,
    Nijmegen (NL), E. Moggi, Genova (IT), J. Parrow, Uppsala (SE),
    C. Palamidessi, University Park, Penn. (US), B. Pierce,
    Philadelphia (US), A. Rabinovich, Tel Aviv (IL), D. Sannella,
    Edinburgh (UK), chair, W. Thomas, Aachen (DE), I. Walukiewicz,
    Bordeaux (FR).
* Invited speakers:
    ICALP: P. Flajolet (INRIA), M. Henzinger (Google), M. Hofmann
    (Munich), W. Rytter (Warsaw & NJIT).
    Joint ICALP/LICS: R. Harper (Carnegie Mellon), A. Razborov
    (Princeton & Moscow), M. Yannakakis (Stanford).

  June 2 2003, Aachen, Germany
  Call for Papers
* Papers are solicited on all aspects of reduction strategies in
  rewriting and programming.
* Deadline: March 17 2004
* For more information see Web page.

  July 13-17 2004, Omni Parker House Hotel, Boston, USA
  Call for Papers
* CAV'04 conference is the 16th in a series  dedicated to the
  advancement of the theory and practice of computer-assisted formal
  analysis methods  for software  and hardware systems.
  The  conference covers the  spectrum from theoretical
  results to  concrete applications,  with an emphasis  on practical
  verification  tools and  the  algorithms and  techniques that  are
  needed for their implementation.
* Deadline (strict): January 23, 2004
* For more information see Web page

  April 3-4 2004, Barcelona, Spain
  Co-located with ETAPS'04
  Call for Papers
* WITS is the offical 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. The members of WG hold their annual workshop as
  an open event to which all researchers working on the theory of
  computer security are invited. This is the fourth workshop of the
  series, and is organised in cooperation with ACM SIGPLAN and GI
  working group FoMSESS.
* Extended abstracts of work (accepted after selection and) presented at
  the Workshop are collected and distributed to the participants. There
  will be no formally published proceedings; however, selected papers
  will be invited for submission to a special issue of the Journal of
  Computer Security.
* Deadline: 15 December 2003
* For more information see Web page

  June 16-18 2004, Hamilton, Canada
  Call for Papers
* The International Conference on Application of Concurrency to System
  Design (ACSD) serves as a forum for disseminating theoretical results
  and advanced methods and tools for the design of complex concurrent
  systems. While there are a few success stories in the field, there is
  still a strong need to bring theory and practice closer together. The
  conference aims at cross-fertilizing both types of research.
* Deadline for submissions: 19 December, 2003
* For more information see Web page

1st International Workshop on Web Services and Formal Methods (WS-FM 2004)
  February 23 2004, Pisa, Italy
  Call for Papers
* The aim of the workshop is to bring together researchers working
  on Web Services and Formal Methods in order to activate a fruitful
  collaboration in this direction of research. This, potentially, could
  also have a great impact on the current standardization phase of Web
  Service technologies.
* Deadline: December 15, 2003
* For more information see Web page

  March 27-29, 2004, barcelona, Spain
  Co-located with ETAPS'04
  Call for Papers
* During the last few years, it is becoming increasingly clear that a
  great variety of state-based dynamical systems, like transition systems,
  automata, process calculi and class-based systems can be captured
  uniformly as coalgebras. Coalgebra is developing into a field of its
  own interest presenting a deep mathematical foundation, a growing field
  of applications and interactions with various other fields such as
  reactive and interactive system theory, object oriented and concurrent
  programming, formal system specification, modal logic, dynamical systems,
  control systems, category theory, algebra, analysis, etc. The aim of the
  workshop is to bring together researchers with a common interest in the
  theory of coalgebras and its applications.
* Deadline for submission: January 1, 2004
* For more information see Web page

  Beijing, China 26-30 September 2004
  Call for Papers
* The aim of the conference is to bring together practitioners
  and researchers from academia, industry and government to
  advance the state of the art in formal methods, to scale up
  their application in software industry and to encourage their
  integration with practical engineering methods.
* Important dates:
  Submission deadline for abstract:  29 March 2004
  Submission deadline for papers:    05 April 2004
  Notification of acceptance:        18 June 2004
  Camera-ready version due:          12 July 2004
  Tutorials and workshops:           26-27 September 2004
  SEFM 2004 in Beijing, China:       28-30 September 2004
* For more information see Web page

  (in conjunction with AMAST 2004)
  Stirling, Scotland, UK, 12--14 July, 2004
  Call for Papers
* Theme. The development of mathematical principles and
  techniques that are demonstrably useful in the process of
  constructing computer programs, whether implemented in
  hardware or software; techniques that combine precision
  with conciseness, enabling programs to be constructed by
  formal calculation.  We welcome contributions to
  programming methodology, to programming paradigms and to
  language design;  theoretical contributions are welcome
  provided their relevance to program construction is
  evident, and discussion of applications is welcome
  provided the mathematical basis is evident.
* Submission of full papers in Postscript or PDF by email to
* Submission Deadline: 31st January, 2004
* Program committee. Roland Backhouse, Stephen Bloom, Eerke
  Boiten, Jules Desharnais, Thorsten Ehm, Jeremy Gibbons,
  Ian Hayes, Eric Hehner, Johan Jeuring, Dexter Kozen
  (chair), Rustan Leino, Hans Leiss, Christian Lengauer,
  Lambert Meertens, Bernhard Moeller, David Naumann, Alberto
  Pardo, Georg Struth, Jerzy Tiuryn, Mark Utting.

  Call for Participation
  Palmse, Estonia, 29 Feb - 5 March 2004
* EWSCS is a series of regional-scope international winter schools
  held annually in Estonia. The main objective of EWSCS is to expose
  Estonian, Baltic, and Nordic graduate students in computer science
  (but also interested students from elsewhere) to frontline research
  topics usually not covered within the regular curricula. The subject
  of the schools is general computer science, with a bias towards
  theory, this comprising both algorithms, complexity and models of
  computation, and semantics, logic and programming theory. The
  working language of the schools is English.
* The schools' scientific programme consists of short courses by
  renowned specialists and a student session. The course list for
  EWSCS'04 is the following:
  - Sergei Artemov (City University of New York, USA):
    [Explicit Provability and Constructive Semantics]
  - Rusins Freivalds (University of Latvia, Riga, Latvia):
    Unreasonable Effectiveness of Classical Mathematics
    in Computer Science
  - Achim Jung (University of Birmingham, UK):
    Stone Duality and Program Logics
  - Moni Naor (Weizmann Institute, Rehovot, Israel):
    Cryptography and Privacy-Preserving Operations
  - Madhu Sudan (MIT / Radcliffe Institute, Cambridge, MA, USA):
    Algorithmic Introduction to Coding Theory
* The purpose of the student session is to give students an opportunity
  to present their own ongoing work (typically, thesis work) and get
  feedback. Registrants to EWSCS'04 are invited to propose short talks
  (20 min) or posters. The selection will be based on abstracts of
  150-400 words.
* Deadline for registration and submission of abstracts of student
  talks/posters: 16 Jan 2004. Notification of acceptance: 30 Jan 2004.

  Computability Theory
  S. Barry Cooper
  Chapman Hall/CRC Mathematics Series, Volume 26, 2003, ISBN: 1584882379
* Written by a leading researcher, Computability Theory provides a
  concise, comprehensive, and authoritative introduction to contemporary
  computability theory, techniques, and results. The basic concepts and
  techniques of computability theory are placed in their historical,
  philosophical and logical context. This presentation is characterized by
  an unusual breadth of coverage and the inclusion of advanced topics not
  to be found elsewhere in the literature at this level.
* The book includes both the standard material for a first course in
  computability and more advanced looks at degree structures, forcing,
  priority methods, and determinacy. The final chapter explores a variety
  of computability applications to mathematics and science.
* Computability Theory is an invaluable text, reference, and guide to the
  direction of current research in the field. Nowhere else will you find
  the techniques and results of this beautiful and basic subject brought
  alive in such an approachable and lively way.
* Ordering information. See publisher's URL above.

  Verification of Reactive Systems
  Klaus Schneider
  Springer Verlag, 2003, ISBN 3-540-00296-0
* This book considers the most popular logics for specification and
  verification of reactive systems. In particular, the relationships and
  verification procedures of the propositional mu-calculus, omega-automata,
  temporal logics, and (monadic) predicate logics are covered in full detail.
  The book has a special emphasis on algorithms that are listed as detailed
  pseudo-code programs. This makes the book particularly useful for those
  who want to implement modern verification procedures. Most results are
  given with detailed proofs, so that the presentation is self-contained.
  This book is targeted to advanced students, lecturers, and researchers in
  the area.
* Course materials (slides and exercises) based on the book will be made
  available before/during the next summer term. A preliminary German version
  can be found under the above URL.
* A public domain verification tool (Equinox) will be made available during
  the next year.

  Logic for Concurrency and Synchronisation
  Ruy J.G.B. de Queiroz (editor)
  Volume 18 of the series "Trends in Logic"
  Kluwer Academic Publishers, Dordrecht
  Hardbound, ISBN 1-4020-1270-5, xxi+284pp
  July 2003
* From the Foreword (by Johan van Benthem):
  The individual chapters of this book show the state of the art in current
  investigations of process calculi such as linear logic, pi-calculus,
  and mu-calculus - with mainly two major paradigms at work, namely,
  linear logic and modal logic. These techniques are applied to the title
  themes of concurrency and synchronisation, but there are also many
  repercussions for topics such as the geometry of proofs, categorial
  semantics, and logics of graphs. Viewed together, the chapters also offer
  exciting glimpses of future integration, as the reader moves back and forth
  through the book. Obvious links include modal logics for proof graphs,
  labeled deduction merging modal and linear logic, Chu spaces linking proof
  theory and model theory, and bisimulation-style equivalences as a tool for
  analyzing proof processes.
  The combination of approaches and the pointers for further integration in
  this book also suggests a grander vision for the field. In classical
  computation theory, Church's Thesis provided a unification and driving
  force. Likewise, modern process theory would benefit immensely from a
  synthesis bringing together paradigms like modal logic, process algebra,
  and linear logic - with their currently still separate worlds of
  bisimulations, proofs, and normalisation. If this Grand Synthesis is ever
  going to happen, books like this are needed!

  Logic and Complexity
  Richard Lassaigne and Michel de Rougemont
  Springer-Verlag, 2003, ISBN 1-85233-565-3
* Logic and Complexity looks at basic logic as it is used in Computer
  Science, and provides students with a logical approach to Complexity theory.
  With plenty of exercises, this book presents classical notions of
  mathematical logic, such as decidability, completeness and incompleteness,
  as well as new ideas brought by complexity theory such as NP-completeness,
  randomness and approximations, providing a better understanding for
  efficient algorithmic solutions to problems. Divided into three parts, it
  covers: - Model Theory and Recursive Functions - introducing the basic model
  theory of propositional, 1st order, inductive definitions and 2nd order
  logic. Recursive functions, Turing computability and decidability are also
  examined. - Descriptive Complexity - looking at the relationship between
  definitions of problems, queries, properties of programs and their
  computational complexity. - Approximation - explaining how some optimization
  problems and counting problems can be approximated according to their
  logical form. Logic is important in Computer Science, particularly for
  verification problems and database query languages such as SQL.
*Ordering Information:

* The Coordination and Component Based Software group in SEN3 at CWI
  has two open positions for:
    (1) a postdoc for a period of four years, and
    (2) a PhD student (OIO) for four years.
  Both positions are within the project number 600.065.120.03N02
  Compositional Construction of Component Connectors (C-Quattro), recently
  funded by the NWO (the Dutch government's funding agency for academic
  scientific research), with F. Arbab (CWI) and J. Rutten (CWI and VUA) as
  Principal Investigators.  The project C-Quattro is in fact
  a collaboration of SEN3 at CWI with the Section
  Theoretical Computer Science at the Free University of Amsterdam (VUA).
  The postdoc will be employed by CWI; the PhD student will be employed
  by the VUA but will spend part of his or her time at CWI.
* For more information on these vacancies, contact either of the PIs:
    F. Arbab, telephone +31-20-5924056, e-mail
    J. Rutten, telephone +31-20-592-4116, email

Back to the LICS web page.