[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.