Newsletter 61

September 29, 1999

[Past issues of the newsletter are available at]

* Homepage: 
* US-Mirror:
* Contact:

* The Kleene award for the  LICS'99 best student paper has been 
  given to Matthias Ruhl (MIT) for his paper
       "Counting and Addition Cannot Express 
        Deterministic Transitive Closure"

  Pittsburgh, Pennsylvania, June 17-20, 2000
  Preliminary Call for Papers
* Topics. For the last 25 years CADE has been the major forum for the
  presentation of research in automated deduction.  Original research
  papers in all aspects of automated theorem proving, automated
  reasoning, computer aided verification, formal methods and static
  analysis are solicited for CADE-17.
* Program committee: David McAllester (chair), Hubert Comon, David
  Dill, Ulrich Furbach, Harald Ganzinger, Mike Gordon, Didier
  Galmiche, Tom Henzinger, Deepak Kapur, Ursula Martin, Ken McMillan,
  Paliath Narendran, David Plaisted, Robert Nieuwenhuis, Tobias
  Nipkow, Hans de Nivelle, Larry Paulson, Amir Pnueli, Mark Stickel,
  Moshe Y. Vardi, Andrei Voronkov.
* Conference Chair: Frank Pfenning
* Submissions. Papers must be original and not submitted for publication
  elsewhere. Research papers can be up to 15 proceedings pages, and
  system descriptions can be up to 5 pages.  System description
  submissions must include a URL for a web page from which the system
  can either be run or obtained by reviewers.  The proceedings of
  CADE-17 will be published by Springer-Verlag in the LNAI series.
  Electronic submission of postscript generated from LaTeX2e and the
  Springer llncs class files is strongly encouraged (details and
  alternatives at the web site above).
* Submissions deadline: January 15, 2000
  Notification of acceptance: March 1
  Camera-ready copy: March 21

  Pittsburgh, Pennsylvania, June 17-20, 2000
  Call for Workshops and Tutorials 
  June 16. and 21. 2000
* CADE is the major forum for the presentation of new research in all
  aspects of automated deduction. Proposals for workshops and for
  tutorials are solicited.  Tutorials will run June 16. and workshops
  also on June 21.  Workshops will ordinarily run a whole day, and
  tutorials for half a day.
* Workshop Topics. Recent CADE workshops have included term
  schematizations and their applications, reasoning, automation of
  proofs by induction, empirical studies in logic algorithms,
  mechanization of partial functions, proof search in type-theoretic
  languages, automated model building, evaluation of automated
  theorem-proving systems, strategies in automated deduction,
  automated theorem proving in software engineering and in
  mathematics, integration of symbolic computation and deduction.
  Workshops may have the same topic as those of previous workshops,
  and this practice is encouraged.
* Tutorial Topics. Recent CADE tutorials have included equality
  reasoning in semantic tableaux, proof systems for nonmonotonic
  logics, rewrite techniques in theorem proving, proof planning,
  parallelization of deduction strategies, resolution decision
  methods, constructive type theory, the use of semantics in
  Herbrand-based proof procedures, logical frameworks, theorem proving
  by the inverse method, deduction methods based on boolean rings,
  higher-order equational logic, and term indexing in automated
  reasoning.  Tutorials may be introductory, intermediate, or
* Proposals. Anyone wishing to organize a workshop or tutorial in
  conjunction with CADE-17 should send (e-mail preferred) a proposal
  no longer than two pages to the workshop chair by November 30, 1999.
  The proposal should describe the topic of the proposed workshop or
  tutorial and explain why the topic is relevant to CADE. Proposals
  will be evaluated, and decisions will be communicated by December
  15. 1999.  Further information about the arrangements for workshops
  and tutorials can be obtained from the CADE-17 Web site.
* Proposal deadline:            November 30, 1999
  Notification of acceptance:   December 15, 1999
  Workshop paper deadline:      April    1,  2000
  Workshop paper notification:  May      1,  2000
* Program Chair: David McAllester  (
  Conference Chair: Frank Pfenning (
  Workshop Chair: Michael Kohlhase (

  Chicago, USA, July 15-19, 2000
* The CAV 2000 conference is the twelfth 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.  The proceedings of the conference will be published
  in the Springer-Verlag Lecture Notes in Computer Science series.
* Topics. Modeling and specification formalisms, Algorithms and tools,
  Verification techniques, Applications and case studies, Testing
  based on Verification technology, Verification in practice.
* Submissions. There are two categories of submissions: (A) Regular
  papers: A submission of a regular paper should include an extended
  abstract not exceeding ten (10) pages. The submission should contain
  original research, and sufficient detail to assess the merits and
  relevance of the contribution. For papers reporting experimental
  results, authors are strongly encouraged to make their data
  available with their submission.  Simultaneous submission to other
  conferences with proceedings or submission of material that has
  already been published elsewhere is not allowed.  (B) Tool
  presentations: Tool submission should be an abstract not exceeding
  four (4) pages.  The same page limit (4) applies to the conference
  proceedings.  The submission should describe the tool and its novel
  features.  Tool papers must describe tools that were already
  implemented. A demonstration is expected to accompany a tool
  presentation. Papers describing tools that have already been
  presented in this conference before will be accepted only if
  significant and clear enhancements to the tool are reported and were
* Submission deadline (firm):                   15 January 2000
  Notification of acceptance:                   15 March 2000
  Proceedings version of accepted papers due:   14 April 2000
* Program Committee. Parosh Abdulla, Rajeev Alur, Henrik Reif
  Andersen, Ed Brinksma, Randy Bryant, Werner Damm, David Dill,
  E. Allen Emerson (co-chair), Steven German, Rob Gerth, Patrice
  Godefroid, Ganesh Gopalakrishnan, Mike Gordon, Nicolas Halbwachs,
  Warren Hunt, Bengt Jonsson, Kim Larsen, Ken McMillan, John Mitchell,
  Doron Peled, Carl Pixley, Amir Pnueli, Bill Roscoe, Joseph Sifakis,
  A. Prasad Sistla (co-chair), Fabio Somenzi, Pierre Wolper

  Call for Papers
  Boston, Massachusetts
  January 22-23, 2000 (back to back with POPL'00)
* Theme.  The PEPM'00 workshop will bring together researchers working in
  the areas of semantics-based program manipulation and partial evaluation.
  The workshop focuses on techniques and supporting theory for the analysis
  and manipulation of programs.
* Technical topics include, but are not limited to program manipulation
  techniques, program analysis techniques, programs as data objects, and
  applications (more detail in
* Submission.  E-mail a gunzip'ed, uuncoded PostScript file to to arrive no later than Monday, October 4, 1999.
  Authors are also requested to submit the title, the list of authors, the
  name of the corresponding author, and a brief ASCII abstract (fewer than
  200 words) by Friday, October 1, 1999.
* Program committee. Zino Benaissa, Andrzej Filinski, John Hatcliff,
  Luke Hornof, Laura Lafave, Julia Lawall (chair), Sheng Liang, Gilles
  Muller, Norman Ramsey, Jon Riecke, Olin Shivers, Morten Heine

  Imperial College, London, UK, July 24-28, 2000            
* CL2000 is the first conference in a major new series of annual
  international conferences bringing together the various communities
  of researchers who have a common interest in Computational Logic.
* CL2000 is collocating with the following conferences: 
  DOOD2000: 6th Int'l Conference on Rules and Objects in Databases 
  ILP2000: 10th Int'l Workshop on Inductive Logic Programming 
  LOPSTR2000: 10th Int'l Workshop on Logic-based Program Synthesis 
              and Transformation 
* CL2000 will include seven streams covering various subfields of
  computational logic, each with its own separate Program Committee:
   - Database Systems (DOOD2000)      
   - Program Development (LOPSTR2000)            
   - Knowledge Representation and Non-monotonic Reasoning       
   - Automated Deduction: Putting Theory into Practice   
   - Constraints        
   - Logic Programming: Theory and Extensions       
   - Logic Programming: Implementations and Applications 
  The last three streams effectively constitute the former ICLP
  conference series that will be now integrated into CL2000. 
  ILP2000 will be collocating as a separate conference.
* Papers on all aspects of the theory, implementation, and application
  of Computational Logic are invited, where Computational Logic is to
  be understood broadly as the use of logic in Computer Science.
* Provisional deadlines.          
  Papers must be submitted by 1 February, 2000        
  Authors will be notified of acceptance/rejection by 1 May, 2000         
  Camera-ready versions must be received by 1 June, 2000  

(FOSSACS 2000)
  Berlin, Germany, March 27-31, 2000
  Call for Papers                      
* FOSSACS seeks papers which offer progress in foundational research
  with a clear significance for software science. A central issue is
  theories and methods which support the specification,
  transformation, verification, and analysis of programs and software
* Topics. Computational and syntactic foundations of software science:
  computation processes over discrete and continuous data, techniques
  for their manipulation, and their algorithmic, algebraic, and
  logical properties; Transition systems, models of concurrency and
  reactive systems, and corresponding calculi, algebras, and logics;
  Type theory, domain theory, and their connections to semantics of
  programming languages and software specification.
* Best paper awards. There will be two awards for the best paper
  among all the papers presented at any of the five main ETAPS
  conferences: EATCS award and EAPLS award.
* Invited speaker. Abbas Edalat (Imperial College, London)
* Submitted papers must be in English and must not have appeared in,
  or have been submitted to, other symposia or journals.  Papers
  should be no more than 15 pages in the Springer-Verlag LNCS style *
* Submission deadline: Monday 18th October 1999
  Notification of authors: Monday 13th December 1999
  Final versions due: Thursday 13th January  2000
* Program committee. Andre Arnold, Mariangiola Dezani, Harald
  Ganzinger, Georg Gottlob, Fritz Henglein, Jean-Pierre Jouannaud,
  Dexter Kozen, Marta Kwiatkowska, Giuseppe Longo, Andrew Pitts,
  Wolfgang Thomas, Glynn Winskel, Moshe Y. Vardi, Jerzy Tiuryn (chair)

  St Andrews, Scotland, July 3-5, 2000
  Call for Papers
* FTP'2000 is the third in a series of workshops intended to focus
  effort on First-Order Theorem Proving as a core theme of Automated
  Deduction, and to provide a forum for presentation of very recent
  work and discussion of research in progress.
  The workshop will be held in conjunction with TABLEAUX 2000.
* Topics. The workshop welcomes original contributions on theorem
  proving in first-order classical, many-valued, and modal logics,
  including nonexclusively: resolution, equational reasoning,
  term-rewriting, model construction, constraint reasoning,
  unification, propositional logic, specialized decision procedures;
  strategies and complexity of theorem proving procedures;
  implementation techniques and applications of first-order theorem
  provers to problems in verification, artificial intelligence, and
* Submission.  Authors are invited to submit papers in the following
  categories: Extended abstracts of 5-8 pages describing original
  results not published elsewhere, Position papers of 1-2 pages
  describing the author's research interests in the field, work in
  progress, and future directions of research, Practical contributions
  of 1-5 pages consisting of new problem sets, system descriptions, or
  solution processes to problem sets according to the guidelines
  above.  System demonstrations will be possible.
  Accepted submissions will be collected in a volume to be distributed
  at the workshop. Additionally, the submissions will be made
  available on the web after the workshop.
* Program Committee: Peter Baumgartner (co-chair), Maria Paola
  Bonacina, Krysia Broda, Francois Bry, Ricardo Caferra, Michael
  Fisher, Fabio Massacci, Bill McCune, David Plaisted, Michael
  Rusinowitch, Gernot Salzer, Tomas Uribe, Christoph Weidenbach,
  Hantao Zhang (co-chair)
* Submission deadline: April 2, 2000
  Acceptance notification: May 12, 2000
  Camera-ready copy due: June 4, 2000
   April  2, 2000   Paper submissions 
   May   12, 2000   Acceptance notification 
   June   4, 2000   Camera-ready copy due 

  at the 7th International Conference on Automated Reasoning with 
  Analytic Tableaux and Related Methods (TABLEAUX)
  St Andrews, Scotland, July 4-7, 2000
  Call for Experimental Papers
* The TABLEAUX conferences are a major forum for the presentation of
  new research in all aspects of automated deduction. In order to
  stimulate Automated Theorem Proving and Satisfiability Testing
  development in non classical logics, and to expose ATP systems to
  interested researchers, the TANC Systems Comparison will be held at
* Topics. The aim of TANCS is to compare the performance of fully
  automatic, non classical ATP systems (based on tableaux, resolution,
  rewriting, ...) in an experimental setting and promote the
  experimental study on theorem proving and satisfiability testing in
  non classical logics.
  For TANCS-2000 the focus is on extended modal and description logics
  and in particular benchmarks derived from combinatorial problems
  will be available for:
  - modal logic K without global axioms (description logic ALC)
  - modal logic K with global axioms (ALC with cyclic TBox)
  - basic temporal logic Kt (ALC with inverse roles)
  - basic temporal logic Kt with global axioms 
    (ALC with inverse and TBoxes)
  This year new benchmarks will be available for Converse
  Propositional Dynamic Logic.
* Who can take part? Everybody who has written a prover for one of the
  logics under consideration. There is no restriction to provers that
  use a particular calculus.
  In particular we welcome novel approaches based on tableaux,
  resolution, rewriting, automata, and SAT-based decision procedure.
* Submissions. Submissions are invited as original, unpublished
  experimental papers describing a theorem prover and its performance
  on the benchmarks of the TANCS 2000 Comparison.
  Beside the paper, entrants are requested to submit the executable
  (or source code) of their prover and a summary of the experimental
  data upon which their paper is based.
  The experimental papers, together with information on the comparison
  design and results, will appear in the proceedings of the
  TABLEAUX-2000 conference published by Springer Verlag in the LNAI
* The comparison of the submitted systems will be mainly based on two
  aspects: (1) Effectiveness, measured by the type and number of
  problems solved, the average runtime for successful solutions the
  scaling of the prover as problems get bigger. (2) Usability,
  measured by the availability of the prover via web or other sources
  the portability of the code to various platforms the ease of
  installation and use
* Deadlines for submission:        January, 19, 2000
  Evaluation of Results:           February 10, 2000
  Deadline for final text:         March 10, 2000
* Comparison Chair:  Fabio Massacci
  Program Chair:     Roy Dyckhoff

  Finite Model Theory (Second Edition)
  H.-D. Ebbinghaus and J. Flum
  360 pp. paperback 
  Springer-Verlag 1999
  Perspectives in Mathematical Logic
  ISBN 3-540-65758-4
* Finite model theory has roots in classical model theory, but owes
  its systematic development to research from complexity theory and
  database theory. The book presents the main results of descriptive
  complexity theory, that is, the connections between axiomatizability
  of classes of finite structures and their complexity with respect to
  time and space bounds. The logics that are important in this context
  include fixed-point logics, transitive closure logics, and also
  certain infinitary languages; their model theory is studied in full
  detail. Other topics include DATALOG languages, quantifiers and
  oracles, 0-1 laws, and optimization and approximation problems.
* For the present second edition the original text has thoroughly been
  revised and extended; in particular, a new chapter has been added
  which is devoted to a central open problem of finite model theory,
  namely the question whether there is a natural logic capturing PTIME
  also on unordered structures. The bibliography and the bibliographic
  references at the end of each chapter have been enlarged

* Term Rewriting and All That
  Franz Baader and Tobias Nipkow
  Cambridge University Press, 1999
  314 pp, paperback, £ 16.95 
  ISBN: 0 521 77920 0
* This textbook offers a unified and self-contained introduction to
  the field of term rewriting. It covers all the basic material
  (abstract reduction systems, termination, confluence, completion,
  and combination problems), but also some important and closely
  connected subjects: universal algebra, unification theory, Gröbner
  bases and Buchberger's algorithm. The main algorithms are presented
  both informally and as programs in the functional language Standard
  ML (an appendix contains a quick and easy introduction to
  ML). Certain crucial algorithms like unification and congruence
  closure are covered in more depth and Pascal programs are
  developed. The book contains many examples and over 170 exercises
  (solutions available from This text is also
  an ideal reference book for professional researchers: results that
  have been spread over many conference and journal articles are
  collected together in a unified notation, proofs of almost all
  theorems are provided, and each chapter closes with a guide to the
* A welcome and important addition to the library of any researcher
  interested in theoretical computer science. It provides a thorough
  grounding in the subject in a clear style, and gives plenty of
  indications of further directions, including an extensive
  bibliography'. The Computer Journal
* Contents: 1. Motivating examples; 2. Abstract reduction systems; 3.
  Universal algebra; 4. Equational problems; 5. Termination;
  6. Confluence; 7. Completion; 8. Gröbner bases and Buchberger's
  algorithm; 9. Combination problems; 10. Equational unification;
  11. Extensions; Appendix 1. Ordered sets; Appendix 2. A bluffer's
  guide to ML; Bibliography; Index.

  Semantics with Applications
  H.R.Nielson & F.Nielson
  2nd edition, 1999, 240 pages
  available for download at
* This book is intended for advanced undergraduates or graduates and
  covers the main approaches to semantics: Operational Semantics,
  Denotational Semantics, Axiomatic Semantics. It also consider
  applications to language implementation and program analysis.
  It is a revised version of a book formerly published with Wiley;
  additional material is available at the web site.

  Category Theory for Computing Science (Third edition)
  Michael Barr and Charles Wells
* This new edition contains all the material from the first and
  second editions, including the four chapters excised from the
  second edition and the solutions to all the exercises, as well as
  added material on factorization systems, monoidal categories, and
  other topics.  All errors known to the authors have been
  corrected. The price is only Can$45, approximately US$31, postpaid
  anywhere on earth.  
* It should be available for ordering from
  by mid-August.  You can also order the book directly by sending an
  email to

  Department of Computer Science
  Utrecht University
  The Netherlands
* The Software Technology research group at Utrecht University has
  several doctoral and post-doctoral positions available. The
  positions are funded by the department, Microsoft Research, and the
  Dutch Science Foundation (NWO).  The main research interests of the
  group are tool support for the development of computer assisted
  teaching material, components and scripting, program generation and
  transformation, tree displaying and manipulation, generic
  programming, and provably correct systems.
* We seek candidates in any of the following topics:
  - Software architecture:
    component-based software, (D)COM, Corba, JINI,
    distributed systems.
  - Security:
    formalisation and verification of security properties,
    transaction processing.
  - Language design:
    advanced type systems, generic programming, intermediate languages.
  - Language implementation:
    interoperability, platform independent run-time systems,
    program transformation.
  - Scripting:
    domain specific languages, e-commerce.
* Applications will be evaluated from now on until the positions are
* To apply (or for further details) please send email to
    Erik Meijer (
  Your email application should include a CV (ascii or postscript) and
  pointers to any on-line articles that you wish us to
  consider. Please can you also include names and email addresses of
  potential referees.