September 3, 1997

```[Past issues of the newsletter are available at
http://www.bell-labs.com/topic/conferences/lics/

BOOK ANNOUNCEMENT
Logic and Structure, Third Edition, Updated and corrected version
Dirk van Dalen.
Springer Verlag Berlin ISBN 3-540-57839-0
* An introduction to the basic facts and techniques.  Treats logic on
the basis of Gentzen's Natural Deduction, Propositional Logic and
Predicate Logic are treated consequently, from each the completeness
theorem is proved separately.  Examples of specific theories are
included.  The next chapter discusses the basics of model theory:
compactness, diagram, Skolem-Loewenheim, elementary
equivalence/extensions, complete theories, quantifier elimination.
A special section is devoted to Skolem functions.  Chapter 4 gives a
brief treatment of second-order logic.  In Chapter 5 the main
non-classical logic is introduced and the notion "constructive" is
discussed. First-order intuitionistic logic is given a thorough
treatment on the basis of natural deduction and Kripke semantics
(including a completeness proof); fundamental properties, such as
existential definability, are shown.  The final chapter covers
(weak) normalization with some applications.  The sections are
supplemented with many exercises.

BOOK ANNOUNCEMENT
Basic Simple Type Theory,
J. Roger Hindley
Cambridge University Press, 1997. ISBN 0-521-46518-4, 186pp.
* This book is aimed at graduate students who already have some
knowledge of lambda calculus. It introduces some of the most
important basic techniques of type theory through a treatment of the
most primitive system, the simple type theory of the pure lambda
calculus. The approach used is through type-assignment, in the style
of Curry and of the language ML. The formulas-as- types
correspondence with implicational logic is emphasized.
* Contents: 1: The type-free lambda-calculus. 2: Assigning types to
terms. 3: The principal-type algorithm. 4: Type-assignment with
equality. 5: A version using typed terms. 6: The correspondence with
implication. 7: The converse principal-type algorithm.  8: Counting
a type's inhabitants. 9. Technical details.

ACM SIGACT-SIGMOD-SIGART SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS (PODS'98)
Call for papers
June 1-3, 1998, Seattle, Washington
* The symposium will focus on new developments in the fundamental
aspects of databases. It will be held jointly with the ACM SIGMOD
International Conference on Management of Data.
* Topics. Access methods and physical design, active databases,
complexity and performance evaluation, concurrency control,
constraint databases, data integration and interoperability, data
mining, data models, database programming languages, database
updates, databases on Internet and Intranet, deductive databases and
knowledge bases, distributed databases, heterogeneous databases,
integrity and security, logic in databases, multimedia databases,
object-oriented databases, OLAP, query languages, real-time
databases, semi-structured data, spatial and temporal databases,
transaction management, views and warehousing.
* Submission. Send 12 copies of extended abstract (not to exceed 10
pages) to the program chair, Jan Paredaens, University of Antwerp
(UIA), Universiteitsplein 1, B-2610 Antwerp, Belgium, e-mail:
pods98@uia.ua.ac.be. Alternatively, submissions can be sent to:
Dan Suciu, AT&T Labs-Research, 180 Park Avenue, Rm. B294, Florham
Park, NJ 07932-0971, USA, suciu@research.att.com. No electronic
submissions will be taken. The firm deadline is November 17, 1997.
* Program committee. Christos Faloutsos, Georg Gottlob, Laks
Lakshmanan, Leonid Libkin, Heikki Mannila, Rajeev Motwani, Jan
Paredaens (chair), Ken Ross, Dan Suciu, Moshe Vardi, Gerhard
Weikum.
* Further information. E-mail pods98@uia.ua.ac.be, or see the URL
above.

IFIP WORKING CONFERENCE ON PROGRAMMING CONCEPTS AND METHODS (PROCOMET '98)
Call for papers
Shelter Island, New York, 8-12 June 1998
* Topics. Compositional approaches to specification and verification,
Specification, verification, and development of concurrent systems,
in particular of reactive, real-time, and hybrid systems,
Abstraction and refinement methods in specification and verification
Semantics of specification and programming concepts, Logical and
algebraic foundations of specification and verification,
Formalization of high-level requirement analysis and design methods
such as synchronous languages, Design of verification support tools,
Practical software-engineering issues in using programming concepts
and methods.
* Program chairs.  D. Gries  and  W.-P. de Roever.
* Program Committee.  Eike Best, Manfred Broy, Ernie Cohen, Philippe
Darondeau, Rocco De Nicola, David Gries, Ian Hayes, Furio Honsell,
Jim Horning, Jay Misra, Carroll Morgan, Ernst-Ruediger Olderog,
Benjamin Pierce, Amir Pnueli, Anders Ravn, Willem-Paul de Roever,
Fred B. Schneider, Michel Sintzoff, Bernhard Steffen, Andrzej
Tarlecki, Frits Vaandrager, Pamela Zave.
* Submissions.  Authors should send 5 copies of a complete paper (at
most 20 pages) by October 15, 1997 to: Prof. Dr. D. Gries, Computer
Science, Upson Hall, Cornell University, Ithaca, NY 14853, USA, or
to Prof. Dr. W.-P. de Roever, Institut fuer Informatik,
Christian-Albrechts-Universitaet, Preusser Strasse 1-9, D-24105
Kiel, Germany. Electronic submissions are also encouraged. For
details, see web site.

INTERNATIONAL LOGIC PROGRAMMING SYMPOSIUM 97 (ILPS'97)
Call for Participation
* See the above URL for more details.

FIRST
INTERNATIONAL CONFERENCE ON TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS'98)
Call for papers
March 31 - April 2, 1998,  Lisbon, Portugal
* Topics.  Compositional verification and construction techniques;
refinement-based methodologies; heterogeneous analysis;
theorem-proving and model checking; analytical techniques for
real-time, hybrid, probabilistic, and safety-critical systems; tool
environments and tool architectures; applications and case studies
* Invited speaker. Randy Bryant (CMU).
* Program committee.  Ed Brinksma, Rance Cleaveland, Fausto
Giunchiglia, Susanne Graf, Tom Henzinger, Daniel Jackson, Kurt
Jensen, Kim Larsen, Tiziana Margaria, Jens Palsberg, Doron Peled,
Scott Smolka, Bernhard Steffen, Frits Vaandrager.
* Submission. Prospective authors are invited to submit an extended
abstract for: A) Regular papers, or B) Tool presentations.
Electronic submission via e-mail is strongly encouraged. Please send
an encapsulated postscript file which can be printed by any
postscript device to tacas98@fmi.uni-passau.de, before 6 October
1997.

INTERNATIONAL WORKSHOP ON VISUALIZATION ISSUES FOR FORMAL METHODS
Call for papers
March 30, 1998, Lisbon, Portugal
* Topics.  Application of visualization and representation concepts to
support domainspecific instantiations of formal methods, System
architectures for enhanced graphical support, Graphical or visual
methods and tools supporting automatic analysis, synthesis and
verification methods, Effects of visual information on productivity
and performance in formal methods, Case studies based on
visually-oriented tools, or comparison studies between visually and
sententially oriented tools and their applications.
* Program Committee.  Lou Feijs, Kathi Fisler, Tiziana Margaria,
Louise Moser, Doron Peled, Joachim Posegga, Peter Reintjes, Dave
Robertson.
* Submission. Electronic submission is encouraged. Send postscript
file to posegga@tzd.telekom.de before October 31, 1997.
Additional information can be found at the URL above.

CHAIR (FULL PROFESSOR) IN COMPUTING SCIENCE
Uppsala University
* Uppsala University invites applications for a tenured chair (full
professor) in computing science at the Faculty of Science and
Technology.  Applicants must demonstrate scientific excellence and
pedagogical proficiency. The successful candidate is expected to
pursue an active research program, perform graduate and
* Prospective candidates must contact the office of the faculty in
order to receive the full announcement with instructions on how to
apply. Please use fax no +46-18-4711999, e-mail:
Christina.Lindberg@uadm.uu.se, or retrieve the announcement from
http://www.csd.uu.se/datalogi/positions97/chair.shtml. Applications
must be received on September 10, 1997, at the latest.
mathematics and computer science, Prof. Ewert Bengtsson, tel no
+46-18-4714367, e-mail Ewert.Bengtsson@cb.uu.se.

INTERNATIONAL WORKSHOP ON ADVANCED COMMUNICATION SYSTEMS (ACoS'98)
Call for papers
April 3 - 4, 1998, Lisbon, Portugal
* Topics.  Application of Intelligent Network concepts for providing
new and advanced services in tele- and heterogeneous communication
networks; Service interaction issues (e.g. dynamic vs. static
analysis; methods and tools for service interaction analysis,
detection and resolution); Methods and tools for the integrated
specification and implementation of new services; Methods and tools
for the operation and control of installed services; Standardization
efforts; Security and availability issues in the service provision
and management; Case studies and fielded experience concerning u.a.
telelearning, tele- medicine, on-line publishing, electronic
commerce, electronic banking.
* Submission. Send an extended abstract (10-15 pages) or proposal for
tool demonstrations, by 31 October 1997, to the Program Chair:
Prof. Bernhard Steffen, Universit"at Dortmund, GB IV, Baroper
Str. 301, D-44221 Dortmund, Germany, E-mail:
acos98@fmi.uni-passau.de, Tel.  : +49 231 755.5801.
* Program Committee.  Sahin Albayrak, Friedrich-Karl Bruhns, Maurizio
Decina, Reinhard Gotzhein, Nancy Griffeth, Jens Gutsche, Bengt
Jonsson, Tiziana Margaria, Walter Ozinger, Manfred Reitenspiess,
Marco Roccetti, Roland R"uckert (Co-Chair), Bernhard Steffen
(Co-Chair), Pamela Zave.

REWRITING TECHNIQUES AND APPLICATIONS (RTA'98)
Call for workshops
* RTA'98 (Rewriting Techniques and Applications, the major
international forum for term rewriting and related areas) will be
held at the University of Tsukuba, Japan, from Monday 30th March to
Wednesday 1st April 1998. Tuesday afternoon (31st) has been reserved
for workshops.  Researchers and practitioners are invited to submit
proposals for workshops on topics relating to term rewriting,
broadly understood.  Anyone wishing to organize a workshop should
send (email preferred) a proposal no longer than two pages to the
program chair by November 15, 1997.  The proposal should describe
the topic of the proposed workshop and its relevance to
RTA. Proposals will be evaluated by the program committee and
decisions will be made by December 1st, 1997. Further information
about the arrangements for workshops can be obtained from the
program chair, Tobias Nipkow, Institut fur Informatik, TU Munchen,
80290 Munchen, Germany, rta98@informatik.tu-muenchen.de.
* Reminder: Deadline for RTA papers is 28 September, 1997.

POST-DOC TO WORK ON VHDL MODEL CHECKER AT CMU
Message from Edmund M. Clarke
* I have support for a post-doc to work on a model checker for VHDL.
We have already spent two years developing the system and it is
abstraction, compositional reasoning, etc. The project would likely
lead to interesting research publications.  The primary requirements
are a knowledge of model checking and compilers. The ability to work
with large software systems is also important. Knowledge of hardware
description languages would be useful, but is not absolutely
required.  The post-doc would last for a year and could start as
early as Oct. 1, 1997. It would pay \$40,000 for the year.
* Please let me know immediately if you are interested in this
position (or know of anyone who is). Send a copy of your CV and two
letters of recommendation (email would be fine) to me at CMU.  If
you would like to see what has been done on the model checker
already, go to my web page at CMU (see the URL above) and follow the