Newsletter 64

February 17, 2000

[Past issues of the newsletter are available at]

* 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  

  (affiliated with LICS 2000)
  Call for Papers
  Santa Barbara, June 29 - 30, 2000
* 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
* 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)

  (affiliated with LICS 2000)
  June 25, 2000
* 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).

  Call for Papers
  July 22 and 23, 2000, Paris, France
* 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
* 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 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. 

  (CAV Workshop)  
  Call for Papers 
  Chicago, July 20, 2000
* 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
* 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)

  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 (
              Dr. S. K. Shukla, Santa Clara (

  Call For Participation
  Caminha, Portugal
  9-15 September 2000
* 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
* 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 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. 
* Scientific committee.    Gilles Barthe, Peter Dybjer, John Hughes, 
  Eugenio Moggi, Simon Peyton-Jones, Jose Manuel Valenca, Glynn Winskel. 

  Constraint Databases 
  Gabriel Kuper, Leonid Libkin, and Jan Paredaens, editors
  Springer Verlag, 2000, ISBN 3-540-66151-4
* 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.

  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
* Order information at
* Course material is available for use with the book at

  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. 
*  (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 (,
  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
* 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.

  Model Checking
  Edmund M. Clarke, Orna Grumberg and Doron A. Peled
  MIT press, December 1999, 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

  Logical Frameworks and Meta-languages
  Call for Papers
* 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 ( and
  Robert Harper (

* 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