[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/] TABLE OF CONTENTS * Calls for Papers: Workshop on Implicit Computational Complexity Workshop on Logical Frameworks and Meta-Languages Workshop on Fixed Points in Computer Science Workshop on Formal Methods and Computer Security PDPTA Special Sessions on Formal Validation * Call for participation: International School on Applied Semantics * Book Announcements: Kuper, Libkin, Paredaens (eds), Constraint Databases Fokkink, Introduction to Process Algebra Huth, Ryan, Logic in Computer Science: Modelling and reasoning about systems Clarke, Grumberg, Peled, Model Checking * Special Issues: Journal of Functional Programming Journal of Applied Non-Classical Logics WORKSHOP ON IMPLICIT COMPUTATIONAL COMPLEXITY (ICC'00) (affiliated with LICS 2000) Call for Papers Santa Barbara, June 29 - 30, 2000 http://www.loria.fr/~marionjy/ICC00.html * Theme. Implicit computational complexity, i.e., machine independent characterizations of computational complexity classes, has gained importance and vigor in recent years. Practically, implicit computational complexity provides framework for a streamlined incorporation of computational complexity into areas such as formal methods in software development programming language theory. * All submissions must be done electronically. Please email your submission to Jean-Yves.Marion@loria.fr * Submission Deadline : March 31, 2000 * Program committee. Samuel Buss (University of California, USA), Loic Colson (Univ. de Metz, France), Martin Hofmann (University of Edinburgh, GB), Neil Jones (University of Copenhagen, Danemark), Claude Kirchner (Loria, Nancy, France), Daniel Leivant (University of Indiana, USA), Jean-Yves Marion (Loria, Nancy, France) (Chair), Helmut Schwichtenberg (University of Muenchen, Germany) WORKSHOP ON LOGICAL FRAMEWORKS AND META-LANGUAGES (LFM'2000) (affiliated with LICS 2000) June 25, 2000 http://www-sop.inria.fr/certilab/LFM00/ * Outline: The aim of the workshop is is to bring together designers, implementers, and practitioners to discuss the development of logical frameworks and their use in meta-reasoning and programming. * Major topics: The design of logical frameworks, meta-theoretical studies, comparative studies, implementation, techniques of representation of formal systems, proofs of properties of formal systems, program development and proofs of program correctness, etc. * Submission: The submission deadline is April 25, 2000. The web page details the format and submission requirements. Authors will be notified of acceptance by May 15, 2000. The final version of accepted papers will be due by June 9, 2000. * Program Committee: David Basin (Freiburg), Thierry Coquand (Goteborg), Joelle Despeyroux (INRIA, Chair), Amy Felty (Bell Labs), Robert Harper (CMU), Martin Hofmann (Edinburgh), Benjamin Pierce (Penn), Benjamin Werner (INRIA). WORKSHOP ON FIXED POINTS IN COMPUTER SCIENCE (FICS 00) Call for Papers July 22 and 23, 2000, Paris, France http://www.liafa.jussieu.fr/~ig/FICS.html * Fixed points play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks. The aim of the workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the fixed point operation in the different fields and formalisms. The First workshop on Fixed Points in Computer Science was held in Brno (1998). * Invited speakers: S. Bloom (Hoboken), B. Courcelle (Bordeaux), H. Marandjian (Yerevan), J. Rutten (Amsterdam), I. Walukiewicz (Warsaw). * PC chair: Irene Guessarian, LIAFA, University Paris 7, Paris 6, Case 7014, 2, place Jussieu, 75251 Paris Cedex 05, France e-mail: ig@liafa.jussieu.fr. * Proceedings: preliminary proceedings containing the abstracts of the talks will be available at the meeting. Publication of final proceedings as a special issue of Theoretical Informatics and Applications depends on the number and quality of the papers. * Paper submission: Authors are invited to send 3 copies of an abstract not exceeding 3 pages to the PC chair. Electronic submissions in the form of uuencoded postscript file are encouraged and can be sent to ig@liafa.jussieu.fr. Submissions are to be received before April 3, 2000. Authors will be notified of acceptance by June 1, 2000. * The workshop will be organised just before the Logic 2000 conference. WORKSHOP ON FORMAL METHODS AND COMPUTER SECURITY (CAV Workshop) Call for Papers Chicago, July 20, 2000 http://www.cs.cmu.edu/~veith/fmcs/ * Computer security protocols are notoriously difficult to get right. Surprisingly simple problems with some well known protocols have been found years after the original protocol was published and extensively analyzed. Our workshop goal is to bring together the formal methods and security communities. Security is a current hot topic in the formal methods community, and we hope that this workshop can help focus these energies. * Topics of interest include descriptive techniques (specification languages, models, logics) and analysis techniques (model checking, theorem proving, and their combination), as applied to protocols for authentication, fair exchange, electronic commerce, and electronic auctions. However, this list is not exclusive. We particularly want to hear about new approaches, new problems, new security properties, and new protocol bugs. Reports on work in progress are welcome. * The program of the workshop will include a keynote address by Doug Tygar, a number of technical sessions (with talks of about 15-20 minutes duration), and a panel discussion. * Paper submission: An extended abstract (about 5-10 pages) explaining recent research results or work in progress should be mailed electronically to fmcs-2000@cs.cmu.edu. * Submission deadline: April 14, 2000. Notification: May 16, 2000. Final papers: June 16, 2000. Workshop: July 20, 2000. * Program Committee: Edmund Clarke (Carnegie Mellon University), Nevin Heintze (Bell Laboratories), Catherine Meadows (Naval Research Laboratory), Jonathan Millen (SRI International), John Mitchell (Stanford University), Scott Stoller (Indiana University) SPECIAL SESSIONS OF FORMAL VALIDATION AT PDPTA 2000 Call for Papers International Conference on Parallel and Distributed Techniques and Applications (PDPTA'2000) Las Vegas, June 26-29 2000 * Two special sessions on Formal Verification technology are being organized at the International Conference on Parallel and Distributed Techniques and Applications (PDPTA'2000) to be held in Las Vegas during June 26-29, 2000. These two sessions are entitled 1. Formal Verification and Formal Methodologies in the Industrial Validation flow 2. Technological Challenges in the Formal Verification of Parallel and Distributed System Designs * Papers are invited for both the sessions. Authors may contribute previously unpublished papers describing research results, case studies and tool descriptions with benchmark results etc. * Deadline for submission March 1, 2000 Acceptance Notification April 1, 2000 Camera Ready Version Due May 15, 2000 Presentation: June 26-29, 2000 * Organizers: Dr. G. M. Reed, Oxford (gmr@comlab.ox.ac.uk) Dr. S. K. Shukla, Santa Clara (sandeep.k.shukla@intel.com) INTERNATIONAL SUMMER SCHOOL ON APPLIED SEMANTICS, APPSEM'2000 Call For Participation Caminha, Portugal 9-15 September 2000 http://www-sop.inria.fr/oasis/Caminha00/index.html * Theme. The summer school is addressed to postgraduate students, researchers and industrials who want to learn about recent developments in programming language research, both in semantic theory and in implementation. * Programme. The programme will consist of introductory and advanced courses on the following themes: description of existing programming language features; design of new programming language features; implementation and analysis of programming languages; transformation and generation of programs; verification of programs. (more details in http://www-sop.inria.fr/oasis/Caminha00/abstract.html) * Lecturers. Andrew Pitts, John Hughes, Eugenio Moggi, Nick Benton, Pierre-Louis Curien, Thierry Coquand, Gilles Barthe, Olivier Danvy, Peter Dybjer, Cedric Fournet, Georges Gonthier, Xavier Leroy, Didier Remy, Martin Odersky, Abbas Edalat, Achim Jung. * Registration. Early registration (before April 21st). Single room 120 000 PTE. Double room: 100 000 PTE. Late registration. Single room: 140 000 PTE. Double room: 120 000 PTE. There is no deadline for late registration but accommodation is not guaranteed if you applied after the 1st July 2000. See http://www-sop.inria.fr/oasis/Caminha00/registration.html for further information. * Grants. Limited funds will be available for grants. The deadline for application for a grant is April 1st. You will receive notification of acceptance/rejection by April 8th. (see http://www-sop.inria.fr/oasis/Caminha00/grant.html) * Scientific committee. Gilles Barthe, Peter Dybjer, John Hughes, Eugenio Moggi, Simon Peyton-Jones, Jose Manuel Valenca, Glynn Winskel. BOOK ANNOUNCEMENT Constraint Databases Gabriel Kuper, Leonid Libkin, and Jan Paredaens, editors Springer Verlag, 2000, ISBN 3-540-66151-4 http://www.cs.bell-labs.com/~libkin/cdb-book * This book is the first comprehensive survey of the field of constraint databases. Constraint databases are a fairly new and active area of database research. The key idea is that constraints, such as linear or polynomial equations, are used to represent large, or even infinite, sets in a compact way. The ability to deal with infinite sets makes constraint databases particularly promising as a technology for integrating spatial and temporal data with standard relational databases. Constraint databases bring techniques from a variety of fields, such as logic and model theory, algebraic and computational geometry, as well as symbolic computation, to the design and analysis of data models and query languages. * The book is a collaborative effort involving many authors who have contributed chapters on their fields of expertise. Despite this, the book is designed to be read as a whole, as opposed to a collection of individual surveys. In particular, the terminology and the style of presentation have been standardized, and there are multiple cross-references between the chapters. * Ordering information. See the URL above. BOOK ANNOUNCEMENT Introduction to Process Algebra Wan Fokkink Texts in Theoretical Computer Science. An EATCS Series Springer-Verlag, January 2000 ISBN 3-540-66579-X, DM 59,- * Automated and semi-automated manipulation of so-called labelled transition systems has become an important means in discovering flaws in software and hardware systems. Process algebra has been developed to express such labelled transition systems algebraically, which enhances the ways of manipulation by means of equational logic and term rewriting. The theory of process algebra has developed rapidly over the last twenty years, and verification tools have been built on the basis of process algebra, often in cooperation with techniques related to model checking. Applications of process algebra exist in diverse fields such as safety-critical systems, network protocols and biology. In the educational vein, process algebra has been recognised to teach skills to deal with complex concurrent systems, by representing and reasoning about such systems in a mathematically clear and precise manner. This textbook gives a thorough introduction into the basics of process algebra and its applications. * Order information at http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-66579-X * Course material is available for use with the book at http://www.cwi.nl/~wan BOOK ANNOUNCEMENT Michael R A Huth, and Mark D Ryan Logic in Computer Science: Modelling and reasoning about systems * Cambridge University Press, 2000 387 pp., Hardback: ISBN 0521652006, UK pounds 52.50 / US $80.00. Paperback: ISBN 0521656028, UK pounds 19.95 / US $34.95. * http://www.cs.bham.ac.uk/research/lics/ http://www.cis.ksu.edu/~huth/lics/ (mirror) * From the foreword by Ed Clarke: "The book is a wonderful example of what a modern text on logic for computer science should be like." * The book is intended as an undergraduate text book in logic applications in computer science. If you are interested in having an inspection copy, please ask Mark Ryan (mdr@cs.bham.ac.uk), letting me know some details of the course you might use it on. * Recent years have seen the development of powerful tools for verifying hardware and software systems, and increasing interest in that technology from major companies such as Intel, Siemens, BT, AT&T, and IBM. Students need a basic formal training which allows them to gain sufficient proficiency in using logic-based verification methods. This book addresses these needs by providing a sound basis in logic, and an introduction to the logical frameworks used in modelling, specifying and verifying computer systems. It provides a simple and clear presentation, covering propositional and predicate logic, and some specialised logics used for reasoning about the correctness of computer systems. The authors introduce a carefully chosen core of essential terminology: further technicalities are introduced only where they are required by the applications. Numerous examples are given, as well as a full exposition of a fast-growing technique for modelling and verifying computer systems, known as symbolic model checking. Numerous examples are given, and web support is available from http://www.cs.bham.ac.uk/research/lics. * Chapter Contents 1. Propositional logic; 2. Predicate logic; 3. Verification by model checking; 4. Program verification; 5. Modal logics and agents; 6. Binary decision diagrams; Bibliography; Index. BOOK ANNOUNCEMENT Model Checking Edmund M. Clarke, Orna Grumberg and Doron A. Peled MIT press, December 1999, ISBN 0262032708 http://mitpress.mit.edu/book-home.tcl?isbn=0262032708 * Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1999 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers. * The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years. * This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers. SPECIAL ISSUE OF THE JOURNAL OF FUNCTIONAL PROGRAMMING Logical Frameworks and Meta-languages Call for Papers http://www-sop.inria.fr/certilab/LFM00/cfp-jfp.html * Topics. The design of logical frameworks, meta-theoretical studies, comparative studies, implementation, techniques of representation of formal systems, proofs of properties of formal systems, program development and proofs of program correctness, etc. * Submission. The deadline for submissions is October 23, 2000. The web page details the format and submission requirements. * Guest editors. Joelle Despeyroux (Joelle.Despeyroux@inria.fr) and Robert Harper (Robert.Harper@cs.cmu.edu). SPECIAL ISSUE OF THE JOURNAL OF APPLIED NON-CLASSICAL LOGICS http://www.editions-hermes.fr * Vol. 9, No 2-3 of the Journal of Applied Non-Classical Logics (JANCL) contains a Special Issue dedicated to the Memory of George Gargov (guest editor: Dimiter Vakarelov). The issue contains a collection of papers by leading logicians. * Content: G. Gargov - Knowledge, uncertainty and ignorance in logic: bilattices and beyond, S. N. Artemov - Realization of intuitionistic logic by proof polynomials, P. Balbiani, E. Orlowska - A hierarchy of modal logics with relative accessibility relations, M. Fitting - Barcan both ways, V. Goranko, D. Vakarelov - Hyperboolean algebras and hyperboolean modal logic, V. Shehtman - ``Everywhere'' and ``here'', D. Skvortsov - Remark on a finite axiomatization of finite intermediate propositional logics, V. Sotirov - Arithmetizations of syllogistic a la Leibniz, J. van Benthem - The range of modal logic * The JANCL is an international tribune, which aims at promoting the development of non-classical logics in Computer Science, with contributions ranging from mathematical foundations of such logics to their applications in Computer Science. The JANCL is published by Hermes