Newsletter 79
June 14, 2002

* Past issues of the newsletter are available at
* Instructions for submitting an announcement to the newsletter
  can be found at

  Workshop on Term Graph Rewriting
  Workshop on Domains
  Workshop on Logical Frameworks and Meta-Languages
  Workshop on Hybrid Logics
  Isabelle/HOL: A Proof Assistant for Higher-Order Logic
    by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel
  Special Issue of the Jornal of Automated Reasoning

  (A satellite event of The First International Conference on Graph
  Transformation, ICGT 2002)
  Second Call for Papers
  Barcelona, Spain, October 7, 2002
* Topics of interest. All aspects of term graphs and sharing of common
  subexpressions in rewriting, programming, automated reasoning and symbolic
  computation. This includes (but is not limited to): Theory of first-order
  and higher-order term graph rewriting; graph rewriting in lambda calculus
  (sharing graphs, optimality); applications in functional, logic and
  functional-logic programming; applications in automated reasoning and
  symbolic computation; implementation issues; system descriptions
* Submissions. Authors are invited to submit an extended abstract of 5 to
  10 pages by e-mail to the program chair ( Submissions
  should be in PostScript format. It is strongly recommended to use LaTeX
  and ENTCS style files (
* Publication. Accepted contributions will appear in an issue of Elsevier's
  Electronic Notes in Theoretical Computer Science.
* Important dates.
  Submission deadline:  June 15, 2002
  Notification:         July 15, 2002
  Final version due:    September 6, 2002
* Program committee. Zena M. Ariola (University of Oregon, Eugene),
  Richard Banach (University of Manchester), Rachid Echahed (IMAG, Grenoble),
  Richard Kennaway (University of East Anglia, Norwich), Jan Willem Klop
  (Free University of Amsterdam), Rinus Plasmeijer (University of Nijmegen),
  Detlef Plump (University of York, chair)

  Call for Abstracts
  Birmingham, UK, 16-19 September 2002
* The Workshop on Domains is aimed at computer scientists and
  mathematicians alike who share an interest in the mathematical
  foundations of computation. The workshop will focus on domains,
  their applications and related topics.
* Invited Speakers: Ulrich Berger (University of Wales Swansea),
  Thierry Coquand (Goeteborg University), Jimmie Lawson (Louisiana
  State University), John Longley (University of Edinburgh), Dag
  Normann (University of Oslo), Prakash Panangaden (McGill
  University), Uday Reddy (University of Birmingham), Thomas Streicher
  (Darmstadt University)
* As such, domain theory is highly interdisciplinary. Topics of
  interaction with domain theory for this workshop include, but are
  not limited to: program semantics, program logics, probabilistic
  computation, exact computation over the real numbers, lambda
  calculus, games, models of sequential computation, constructive
  mathematics, recursion theory, realizability, real analysis,
  topology, locale theory, metric spaces, category theory, topos
  theory, type theory
* Submission of Abstracts: One-page abstracts should be submitted to Shortly after an abstract is submitted
  (usually one or two weeks), the authors will be notified by the
  programme committee. The criterion for acceptance is relevance to
  the meeting. In particular, talks on subjects presented at other
  conferences and workshops are acceptable. Abstracts will be dealt
  with on a first-come/first-served basis.
* Programme Committee: Martin Escardo (University of Birmingham),
  Achim Jung (University of Birmingham), Klaus Keimel (Darmstadt
  University), Alex Simpson (University of Edinburgh)

  (Affiliated with FLoC'02)
  Call for Participation
  Copenhagen, Denmark, July 26, 2002
* Logical frameworks and meta-languages form a common substrate for
  representing, implementing, and reasoning about a wide variety of
  deductive systems of interest in logic and computer science.  Their
  design and implementation has been the focus of considerable
  research over the last two decades, using competing and sometimes
  incompatible basic principles.  This workshop will bring together
  designers, implementors, and practitioners to discuss all aspects of
  logical frameworks.
* Informal proceedings will be published as a volume in the Electronic
  Notes in Theoretical Computer Science (ENTCS) and will be available
  at the workshop.
* The workshop is open for any interested party.  If you are planning
  to attend you are welcome to participate in the informal system
  demonstration session.  Please send mail to the workshop chair
  (Frank Pfenning ) if you are interested in showing
  your implementation.
* The program can be found at

  (Affiliated with FLoC'02)
  Call for Participation
  Copenhagen, Denmark, July 25, 2002
* Hybrid logic is a branch of modal logic in which it is possible to
  directly refer to worlds/times/states or whatever the elements of
  the (Kripke) model are meant to represent. Although they date back
  to the late 1960s, and have been sporadically investigated ever
  since, it is only in the 1990s that work on them really got into its
* It is easy to justify interest in hybrid logic on applied grounds,
  with the usefulness of the additional expressive power. For example,
  when reasoning about time one often wants to build up a series of
  assertions about what happens at a particular instant, and standard
  modal formalisms do not allow this. What is less obvious is that the
  route hybrid logic takes to overcome this problem (the basic
  mechanism being to add nominals --- atomic symbols true at a unique
  point --- together with extra modalities to exploit them) often
  actually improves the behavior of the underlying modal
  formalism. For example, it becomes far simpler to formulate modal
  tableau and resolution in hybrid logic, and completeness and
  interpolation results can be proved of a generality that is simply
  not available in modal logic. That is, hybridization --- adding
  nominals and related apparatus --- seems a fairly reliable way of
  curing many known weaknesses in modal logic.
* HyLo@LICS is likely to be relevant to a wide range of people,
  including those interested in description logic, feature logic,
  applied modal logics, temporal logic, and labelled
  deduction. Moreover, if you have an interest in the work of the late
  Arthur Prior, note that this workshop is devoted to exploring ideas
  he first introduced 30 years ago --- it will be an ideal opportunity
  to see how his ideas have been developed in the intervening period.
* In this workshop we hope to bring together researchers from all the
  different fields just mentioned (and hopefully some others) in an
  attempt to explore what they all have (and do not have) in
  common. If you're unsure whether the workshop is of relevance to
  your work , please check out the Hybrid Logics homepage. And do not
  hesitate to contact the workshop organisers for more
  information. We'd be delighted to tell you more. Contact details are
  given below.
* The program includes invited talks by Melvin Fitting and Moshe
  Vardi. The full program is available at the workshop webpages:

  Isabelle/HOL: A Proof Assistant for Higher-Order Logic
  by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel
  Springer LNCS 2283, ISBN 3-540-43376-7
* This book is a self-contained introduction to interactive proof in
  higher-order logic (HOL), using the proof assistant Isabelle2002. It is a
  tutorial for potential users rather than a monograph for researchers.
* The book has three parts.
  1. Elementary Techniques shows how to model functional programs in
  higher-order logic. Early examples involve lists and the natural
  numbers. Most proofs are two steps long, consisting of induction on a
  chosen variable followed by the auto tactic. But even this elementary part
  covers such advanced topics as nested and mutual recursion.
  2. Logic and Sets presents a collection of lower-level tactics that you can
  use to apply rules selectively. It also describes Isabelle/HOL's treatment
  of sets, functions and relations and explains how to define sets
  inductively. One of the examples concerns the theory of model checking, and
  another is drawn from a classic textbook on formal languages.
  3. Advanced Material describes a variety of other topics. Among these are
  the real numbers, records and overloading. Advanced techniques are
  described involving induction and recursion. A whole chapter is devoted
  to an extended example: the verification of a security protocol.
* The book is available online.

  Bytecode Verification
  Call for Papers
* Topic: Bytecode verification for the Java Virtual Machine and related
  approaches to program analysis of low level code for the enforcement of
  safety properties. Particularly welcome are contributions emphasizing the
  correctness of the analysis and the application of automated or interactive
  verification techniques.
* Submission:  Manuscripts should be unpublished works and not
  submitted elsewhere.  Revised and enhanced versions of papers
  published in conference proceedings that have not appeared in
  archival journals are eligible for submission.  All submissions will
  be reviewed according to the usual standards of scholarship and
  originality.  *The deadline for submissions is October 13, 2002.*
* Guest editor: Tobias Nipkow,

Back to the LICS web page.