Newsletter 76
December 14, 2001

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

* Calls for Papers and Conference Announcements
  Symposium on Functional and Logic Programming
  Clifford Lectures and Workshop on the Mathematical
    Foundations of Programming Semantics
  Symposium on the Theory and Applications of Satisfiability Testing
  Workshop on Complexity in Automated Deduction
  Workshop on Fixed Points in Computer Science
  Workshop on Domain Theory
* Book Announcements
  The pi-Calculus, A Theory of Mobile Porcesses by D.Sangiorgi, D.Walker
  Handbook of Automated Reasoning edited by J.A.Robinson, A.Voronkov
* Journals
  Special Issue on Proof Carrying Code of the Journal of
    Automated Reasoning
* Position Announcement
  Postdoc Positions at Toronto

  (Co-Located with ACM SIGPLAN ASIA-PEPM 2002)
  Call for Papers
  Aizu, Japan, September 15-17, 2002
* Theme. FLOPS is a forum for research on all issues concerning
  functional programming and logic programming. In particular, it
  wants to stimulate the cross-fertilization as well as integration of
  the two paradigms. FLOPS 2002 invites original papers in all areas
  of functional and logic programming, including foundations,
  implementations and applications. Original research papers and
  system descriptions are solicited.
* Submission is Web-based. In order to submit a paper, authors should
  fill in the submission form available at
  where more detailed instructions are given.
* Important Dates
  Paper submission: March 1, 2002
  Notification of acceptance: May 21, 2002
  Final version due: June 25, 2002
* Program committee. Maria Alpuente (Spain), Wei-Ngan Chin
  (Singapore), Pierre Deransart (France), Moreno Falaschi
  (Italy), Michael Hanus (Germany), Zhenjiang Hu (Co-Chair, Japan),
  Jan Maluszynski (Sweden), Aart Middeldorp (Japan), Gopalan Nadathur
  (USA), Susumu Nishimura (Japan), Catuscia Palamidessi (USA), Mario
  Rodriguez-Artalejo (Co-Chair, Spain), Francesca Rossi (Italy), Harald
  Sondergaard (Australia), Kwangkeun Yi (Korea), Kazunori Ueda (Japan)

  First Announcement
  Tulane University
  New Orleans, LA USA, March 20 - 26, 2002
* This year's MFPS workshop - MFPS 18 - will be held in conjunction
  with the 2002 Clifford Lectures, an annual lecture series sponsored
  by the Tulane Mathematics Department.
* The Clifford Lectures are named in honor of A. H. Clifford, noted
  algebraist and longtime member of the Tulane Mathematics
  Department. The 2002 Clifford Lecturer is Sergei N. Artemov, Gaduate
  Center, CUNY. The lectures will include invited talks by other
  participants. The lectures will take place from midday, March 20,
  2002 through midday, March 23, 2002. A complete list of speakers can
  be found at the web site listed above.
* The Eighteenth Workshop on the Mathematical Foundations of
  Programming Semantics (MFPS 18) will take place at Tulane
  immediately following the Clifford Lectures. The invited speakers
  include Rajeev Alur (Penn), Patrick Cousot (ENS), John Hatcliff
  (Kansas State), John Mitchell (Stanford), John Reynolds (CMU) and
  Doug Smith (Kestrel). In addition there will be three special
  sessions. The remainder to fhe program will consist of talks
  contributed by participants. The available slotts will be allocated
  on a first come - first serve basis.
* To submit an abstract for a contributed talk, send email to giving the title and a short abstract.
* More information about both meetings can be found at the MFPS 18
  home page 

  Call for Papers, SAT solvers, SAT benchmarks
  May 6-9, 2001, Cincinnati, Ohio, USA
* Topics: Several aspects of Satisfiability testing will be explored
  including: propositional proof systems, search techniques,
  relationship between BDDs and search, applications such as in formal
  verification, probabilistic analysis of SAT algorithms and SAT
  properties, upper bounds on SAT algorithm performance, specific
  solvers, empirical results, quantified boolean formulas, and related
* Invited Speakers: Edmund Clarke (Carnegie Mellon University, USA),
  Joăo Marques-Silva (Inst. Superior Técnico, Universidade Técnica de
  Lisboa), Uwe Schöning (Universität Ulm, Germany)
* In conjunction with the symposium: SAT Solver Competition (BDD
  packages welcome): see the symposium home page for details.
  Special Mini-Workshop on QBF: see the symposium home page for details.
* For submission details, see the symposium home page.
* Important Dates:
  Submission of extended abstracts: February 6, 2002.
  Submission of SAT solvers: March 6, 2002.
  Submission of SAT benchmarks: March 6, 2002.
  Decisions on extended abstracts returned: March 6, 2002.
  SAT Solver Bugfixes: March 27, 2002.
  SAT Solver Competition: Starting April 6, 2002, until the conference.
  Requests to participate without submission: April 10, 2002.
  Conference: May 6 - 9, 2002.
  Submission of final journal articles: May 30, 2002.
* Program Committee: Dimitris Achlioptas (Microsoft Research, USA),
  Endre Boros (Rutcor, Rutgers University, USA), Nadia Creignou
  (Université del la Méditerranée, Marseille, France), Joe Culberson
  (University of Alberta, Edmonton, Canada), Olivier Dubois
  (Université Paris 6, France), Thomas Eiter (Technische Universität
  Wien, Austria) John Franco (University of Cincinnati, USA) Ian Gent
  (St. Andrews University, Scotland, UK) Andreas Goerdt (Chemnitz,
  Germany) Edward A. Hirsch (Steklov Institute of Mathematics at
  St. Petersburg, Russia) Russell Impagliazzo (UC San Diego, USA)
  Henry Kautz (University of Washington, USA) Lefteris Kirousis
  (University of Patras, Greece) Hans Kleine Büning (Universität
  Paderborn, Germany) Oliver Kullmann (Swansea, Wales, UK) Daniel Le
  Berre (Université d'Artois, France) Chu-Min Li (LaRIA, Université de
  Picardie Jules Verne, France) Hans van Maaren (University of Delft,
  The Netherlands) Paul W. Purdom (Indiana University, USA) Bart
  Selman (Cornell University, USA) Ewald Speckenmeyer (Universität
  Köln, Germany) Allen Van Gelder (UC Santa Cruz, USA) Miroslav
  N. Velev (Carnegie Mellon University, USA) Toby Walsh (University of
  York, UK) Lintao Zhang (Princeton University, USA)

  Call for Papers
  July 30 - August 1, 2002 in Copenhagen, Denmark,
  as part of the Federated Logic Conference FLoC'02
* The conference invites papers concerning all aspects - theoretical
  foundations, implementation techniques, systems development and
  applications -  of the mechanization of reasoning with tableaux
  and related methods.
* All submissions must be done electronically via
  Detailed information on submission categories can be found
* Important dates
  Submission deadline: February 2, 2002
  Notification of acceptance: March 29, 2002
  Camera-ready copy due: May 10, 2002
* Program committee:
  Peter Baumgartner (U Koblenz-Landau), Bernhard Beckert (U Karlsruhe),
  Marcello D'Agostino (U Ferrara, Italy),  Roy Dyckhof (U St Andrews),
  Uwe Egly (TU Vienna, co-chair), Christian Fermueller (TU Vienn, co-chair)
  Melvin Fitting (City U of NY), Didier Galmiche (LORIA Nancy),
  Rajeev Gore (ANU), Jean Goubault-Larrecq (ENS Cachan), Reiner Haehnle
  (Chamlers U), Ian Horrocks (U Manchester), Christoph Kreitz (Cornell),
  Reinhold Letz (TU of Munich), Fabio Massacci (U Siena),
  Neil Murray (SU of NY-Albany), Nicola Olivetti (U Torino).

  (affiliated with CADE-18)
  July 25-26 2002 in Copenhagen, Denmark
* Aim of the workshop: The Workshop on Complexity in Automated
  Deduction will bring together researchers who work on or have a
  serious interest in problems that are in the interface between
  automated deduction and computational complexity.  The aim of the
  workshop is to enhance the interaction between automated deduction
  and computational complexity through invited and contributed talks
  that will present comprehensive overviews, report on state-of-the
  art advances, and expand the horizons of this area of research.
* Invited speakers: Marco Cadoli (Universitŕ di Roma La Sapienza,
  Roma, Italy), Hubert Comon (LSV, ENS Cachan, France), Erich Grädel
  (RWTH Aachen, Germany), Martin Grohe (University of Edinburgh, UK),
  Phokion G. Kolaitis (University of California, Santa Cruz, USA),
  Paliath Narendran (SUNY Albany, USA), Reinhard Pichler (Siemens AG
  Austria and TU Wien, Vienna, Austria), Pavel Pudlák (Mathematical
  Institute, Academy of Sciences, Prague, Czech Republic), Andrei
  Voronkov (University of Manchester, UK)
* Contributed talks: In addition to the invited presentations, there
  will be contributed talks. If you are interested in giving such a
  contributed talk, please send an abstract, preferably as a
  PostScript attachment, to no later than
  Friday, May 17, 2002.
* Organizers: Georg Gottlob (TU Wien, Vienna, Austria), Miki Hermann
  (LORIA, Nancy, France), Michael Rusinowitch (LORIA, Nancy, France)
* Important dates:
  Submission of abstracts for contributed talks:    May 17, 2002
  Notification of acceptance:                       June 6, 2002
  Deadline for final versions of accepted papers:   June 20, 2002
  Workshop:                                         July 25 and 26, 2002

  (affiliated with LICS'02)
  Preliminary Call for Papers
  July 20-21, 2002, Copenhagen, Denmark
* Theme: Construction and reasoning about properties of fixed points,
  categorical, metric and ordered fixed point models, continuous
  algebras, relation algebras, fixed points in process algebras and
  process calculi, regular algebras of finitary and infinitary
  languages, formal power series, tree automata and tree languages,
  infinite trees, the mu-calculus and other programming logics, fixed
  points in relation to dataflow and circuits, fixed points and the
  lambda calculus, fixed points in logic programming and data bases.
* Paper submission: Authors are invited to send three copies of an
  abstract not exceeding three pages to the PC cochair Anna
  Ingolfsdottir.  Electronic submissions in the form of uuencoded
  postscript files are encouraged and can be sent to
* Submissions are to be received before April 15, 2002.
* Invited speakers: L. Aceto (Aalborg), D. Kozen (Cornell), A. Labella
  (Rome), G. Winskel (Cambridge, provisional).
* Program Committee: J. Adamek (Braunschweig), R. Backhouse
  (Nottingham), S. Bloom (Hoboken NJ), J. Bradfield (Edinburgh), R. De
  Nicola (Florence), Z. Esik (cochair, Szeged), I. Guessarian (Paris),
  A. Ingolfsdottir (cochair, Aalborg), W. Kuich (Vienna), A. Labella
  (Rome), M. Mislove (Tulane), D. Niwinski (Warsaw).
* Proceedings: Preliminary proceedings containing the abstracts of the
  talks will be available at the meeting. Final proceedings will be
  published after the meeting as a special issue of the journal
  Theoretical Informatics and Application

  Call for Abstracts
  Birmingham, 16-19 September 2002.
* AUDIENCE. The Workshop on Domains is aimed at computer scientists
  and mathematicians alike who share an interest in the mathematical
  foundations of computation. It will focus on domains, their
  applications and related topics.  Previous meetings were held in
  Darmstadt (94,99), Braunschweig (96), Munich (97) and Siegen
  (98). The emphasis is on the exchange of ideas between participants
  similar in style to Dagstuhl seminars.
* INVITED SPEAKERS. Ulrich Berger (Wales Swansea), Thierry Coquand
  (Goeteborg), Jimmie Lawson (Louisiana State), John Longley
  (Edinburgh), Dag Normann [to be confirmed] (Oslo), Prakash
  Panangaden (McGill), Uday Reddy (Birmingham), Thomas Streicher
* SCOPE. Domain theory has had applications to programming language
  semantics and logics (lambda-calculus, PCF, LCF), recursion theory
  (Kleene-Kreisel countable functionals), general topology (injective
  spaces, function spaces, locally compact spaces, Stone duality),
  topological algebra (compact Hausdorff semilattices) and analysis
  (measure, integration, dynamical systems). Moreover, these
  applications are related - for example, Stone duality gives rise to
  a logic of observable properties of computational processes.
  Talks in any area of interaction with domain theory are welcome.
* SUBMISSIONS. Abstracts will be dealt with on a first-come/
  first-served basis. Please email one-page abstracts to . Authors will hear from the programme
  committee within one or two weeks of submission.
* DEADLINE : 30 April 2002
* PROGRAMME COMMITTEE. Martin Escardo (Birmingham), Achim Jung
  (Birmingham), Klaus Keimel (Darmstadt), Alex Simpson (Edinburgh).

  The pi-Calculus, A Theory of Mobile Porcesses
  by Davide Sangiorgi and David Walker
  Cambridge University Press 2001 ISBN 0-521-78177-9
* A detailed text on the pi-calculus, a mathematical model highly
  suited to describing mobile systems, the components of which
  communicate and change their structure.
* The book is written at the graduate level, assuming no prior
  acquaintance with the subject, and is intended for computer
  scientists interested in mobile systems.
* See above url for ordering information

  Handbook of Automated Reasoning
  edited by J. Alan Robinson and Andrei Voronkov
  MIT Press, 2001, ISBN two-volume set 0-262-18223-8
  Vol. 1, 0-262-18221-1, Vol. 2, 0-262-18222-X
  Available in the USA and dependencies, the Philippines, and Canada only
* Automated reasoning has matured into one of the most advanced areas
  of computer science. It is used in many areas of the field,
  including software and hardware verification, logic and functional
  programming, formal methods, knowledge representation, deductive
  databases, and artificial intelligence. This handbook presents an
  overview of the fundamental ideas, techniques, and methods in
  automated reasoning and its applications. The material covers both
  theory and implementation. In addition to traditional topics, the
  book covers material that bridges the gap between automated
  reasoning and related areas. Examples include model checking,
  nonmonotonic reasoning, numerical constraints, description logics,
  and implementation of declarative programming languages.
* The book consists of eight parts. After an overview of the early
  history of automated deduction, the areas covered are reasoning
  methods in first-order logic; equality and other built-in theories;
  methods of automated reasoning using induction; higher-order logic,
  which is used in a number of automatic and interactive
  proof-development systems; automated reasoning in nonclassical
  logics; decidable classes and model building; and
  implementation-related questions.
* Ordering information. See the URL above.

  Proof-Carrying Code
  Call for Papers
* Topics.  Proof-carrying code and related approaches which use formal
  reasoning to enhance safety and reliability of software.  Original
  results and study of tools and methods for proof generation, proof
  checking, and their integration with code generation/compilation.
* Submission.  Manuscripts should be unpublished works and not
  submitted elsewhere.  Revised and enhanced versions of papers
  published in conference proceedings that have not appeared in
  archival journals are eligible for submission.  All submissions will
  be reviewed according to the usual standards of scholarship and
  originality.  The deadline for submissions is February 22, 2002.
* Guest editor.  Amy Felty (

  Department of Computer Science
  University of Toronto
* The theory group is offering a number of postdoctoral fellowships in
  the areas of computational complexity, combinatorics, graph theory,
  and distributed systems.  The fellowships are for one year,
  beginning September, 2002, with a possible extension to two years.
  Candidates should send applications to Steve Cook
  ( including a CV, a list of publications, a
  statement of research interests, and a list of referees.
* Applications are expected by 15 January, 2002.

Back to the LICS web page.