Newsletter 79
June 14, 2002
*******************************************************************
* Past issues of the newsletter are available at
http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/
* Instructions for submitting an announcement to the newsletter
can be found at
http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/inst.html
*******************************************************************
TABLE OF CONTENTS
* CONFERENCES AND WORKSHOPS
Workshop on Term Graph Rewriting
Workshop on Domains
Workshop on Logical Frameworks and Meta-Languages
Workshop on Hybrid Logics
* BOOK ANNOUNCEMENT
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel
* JOURNALS
Special Issue of the Jornal of Automated Reasoning
INTERNATIONAL WORKSHOP ON TERM GRAPH REWRITING (TERMGRAPH 2002)
(A satellite event of The First International Conference on Graph
Transformation, ICGT 2002)
Second Call for Papers
Barcelona, Spain, October 7, 2002
http://www.cs.york.ac.uk/~det/Termgraph_2002/cfp.html
* 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 (det@cs.york.ac.uk). Submissions
should be in PostScript format. It is strongly recommended to use LaTeX
and ENTCS style files (http://math.tulane.edu/~entcs/).
* 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)
DOMAINS VI
Call for Abstracts
Birmingham, UK, 16-19 September 2002
http://www.cs.bham.ac.uk/~wd6/index.html
* 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
domainsvi@cs.bham.ac.uk. 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)
WORKSHOP ON LOGICAL FRAMEWORKS AND META-LANGUAGES (LFM'02)
(Affiliated with FLoC'02)
Call for Participation
Copenhagen, Denmark, July 26, 2002
http://www.cs.cmu.edu/~lfm02/
* 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 http://www-2.cs.cmu.edu/~lfm02/program.html.
WORKSHOP ON HYBRID LOGICS (HyLo@LICS)
(Affiliated with FLoC'02)
Call for Participation
Copenhagen, Denmark, July 25, 2002
http://hylo20002.hylo.net
* 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
stride.
* 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:
http://hylo20002.hylo.net
BOOK ANNOUNCEMENT
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
http://www.in.tum.de/~nipkow/LNCS2283/
* 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.
SPECIAL ISSUE OF THE JOURNAL OF AUTOMATED REASONING
Bytecode Verification
Call for Papers
http://www.in.tum.de/~nipkow/jar-bcv/
* 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, nipkow@in.tum.de.
Back to the LICS web page.