FOM: LICS (Logic in Computer Science) Newsletter 79

[Stephen G Simpson]

 From: Martin Grohe <grmail at dcs.ed.ac.uk>
 To: LICS List <grmail at dcs.ed.ac.uk>
 Subject: LICS Newsletter 79
 Date: Fri, 14 Jun 2002 19:30:09 +0100

 *******************************************************************  
 * 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 at 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 at 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 <fp at cs.cmu.edu>) 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 at 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 at 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 at in.tum.de.