Newsletter 64
February 17, 2000
[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