Newsletter 79June 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 ReasoningINTERNATIONAL 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 VICall 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.netBOOK ANNOUNCEMENTIsabelle/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 REASONINGBytecode 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.