Newsletter 61
September 29, 1999
[Past issues of the newsletter are available at
http://logik.mathematik.uni-freiburg.de/lics/newsletters/
http://www.cs.bell-labs.com/who/libkin/lics/newsletters/]
NEW LICS URLS:
* Homepage: http://logik.mathematik.uni-freiburg.de/lics/
* US-Mirror: http://www.cs.bell-labs.com/who/libkin/lics/
* Contact: lics-request@logik.mathematik.uni-freiburg.de
1999 KLEENE AWARD
* 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"
INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION (CADE-17)
Pittsburgh, Pennsylvania, June 17-20, 2000
Preliminary Call for Papers
http://www.research.att.com/conf/cade
* 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
INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION (CADE-17)
Pittsburgh, Pennsylvania, June 17-20, 2000
Call for Workshops and Tutorials
June 16. and 21. 2000
http://www.research.att.com/conf/cade/
* 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
advanced.
* 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 (dmac@research.att.com)
Conference Chair: Frank Pfenning (fp+@cs.cmu.edu)
Workshop Chair: Michael Kohlhase (kohlhase@cs.uni-sb.de)
CONFERENCE ON COMPUTER AIDED VERIFICATION (CAV 2000)
Chicago, USA, July 15-19, 2000
http://www.cs.utexas.edu/users/cav2k/
* 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
implemented.
* 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
ACM SIGPLAN WORKSHOP ON PARTIAL
EVALUATION AND SEMANTICS-BASED PROGRAM MANIPULATION (PEPM'00)
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 http://www.cs.brandeis.edu/~pepm00).
* Submission. E-mail a gunzip'ed, uuncoded PostScript file to
pepm00@cs.brandeis.edu 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
Sorensen.
INTERNATIONAL CONFERENCE ON COMPUTATIONAL LOGIC (CL 2000)
Imperial College, London, UK, July 24-28, 2000
http://www.doc.ic.ac.uk/cl2000
* 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
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES
(FOSSACS 2000)
Berlin, Germany, March 27-31, 2000
Call for Papers
http://fossacs.mimuw.edu.pl
* 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
systems.
* 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)
INTERNATIONAL WORKSHOP ON FIRST-ORDER THEOREM PROVING
St Andrews, Scotland, July 3-5, 2000
Call for Papers
http://www.uni-koblenz.de/ftp00/
* 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
mathematics.
* 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
TABLEAUX NON CLASSICAL SYSTEMS COMPARISON (TANCS 2000)
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
http://www.dis.uniroma1.it/~tancs
* 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
TABLEAUX-00.
* 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
series.
* 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
BOOK ANNOUNCEMENT
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
considerably.
BOOK ANNOUNCEMENT
* 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 dtranah@cup.cam.ac.uk). 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
literature.
* 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.
BOOK ANNOUNCEMENT
Semantics with Applications
H.R.Nielson & F.Nielson
2nd edition, 1999, 240 pages
available for download at http://www.daimi.au.dk/~hrn
* 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.
BOOK ANNOUNCEMENT
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
http://crm.umontreal.ca/pub/Ventes/CatalogueEng.html
by mid-August. You can also order the book directly by sending an
email to sales@crm.umontreal.ca.
PhD AND POST-DOC POSITIONS AVAILABLE
Department of Computer Science
Utrecht University
The Netherlands
http://www.cs.uu.nl
* 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
filled.
* To apply (or for further details) please send email to
Erik Meijer (mailto:erik@cs.uu.nl)
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.