LICS Newsletter 46

Newsletter 46

September 3, 1997

[Past issues of the newsletter are available at 

  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.

  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.

  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: Alternatively, submissions can be sent to:
  Dan Suciu, AT&T Labs-Research, 180 Park Avenue, Rm. B294, Florham
  Park, NJ 07932-0971, USA, 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
* Further information. E-mail, or see the URL

  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. 

  Call for Participation
* See the above URL for more details. 

  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, before 6 October

  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
* Submission. Electronic submission is encouraged. Send postscript
  file to before October 31, 1997. 
  Additional information can be found at the URL above. 

  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
  undergraduate teaching, and supervise graduate students.
* 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:, or retrieve the announcement from Applications
  must be received on September 10, 1997, at the latest. 
* For additional information about the position, consult the dean of
  mathematics and computer science, Prof. Ewert Bengtsson, tel no
  +46-18-4714367, e-mail 

  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:, 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.

  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, 
* Reminder: Deadline for RTA papers is 28 September, 1997.

  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
  quite powerful already. Now, we want to add features for handling
  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
  links to the Model Checking home page. The VHDL model checker is
  called CV.