LICS Newsletter 39

Newsletter 39

October 26, 1996

Because of the AT&T breakup, LICS has new URL's:

* FTP site.
* WWW homepage.
* Contact.

* This special issue of the Journal of Automated Reasoning is devoted
  to papers describing the implementation of a significant proof or
  theory within a theorem prover.  A submission should consist of two
  parts: (1) a paper outlining the theory, proofs, formalization
  techniques, etc. in informal mathematical language (limited to 30
  pages), and (2) the code of the implementation.  In addition to the
  hardcopy publication in the Journal of Automated Reasoning, papers
  and implementations will be made available electronically for
  browsing and retrieval.
* Submissions should satisfy the usual standards of scholarship and
  originality, although novelty of the proof or theory itself is
  explicitly not required.  Importance and difficulty of the encoded
  theory will play an important role in the evaluation.
  Journal-quality submissions which do not fit into the special issue
  may be considered for a future track of the Journal of Automated
  Reasoning devoted entirely to the publication of formal proofs.
* Submission deadline is January 15, 1997.  Please direct inquiries to
  the guest editor of this special issue: Frank Pfenning, Department
  of Computer Science, Carnegie Mellon University, Pittsburgh, PA
  15213-3891, USA,,

  Delphi, Greece, January 8-10, 1997
  Call for Participation 
* ICDT'97 highlights: Invited talks by S. Abiteboul (Querying
  Semi-Structured Data) and J. Ullman (Information Integration Using
  Logical Views); Invited tutorial on data mining by H. Mannila;
  Presentations of 29 technical papers selected out of 119 submissions
* Deadline for early registration and hotel reservation is November
  12, 1996.    
* Further information: URL above, or email 

  A Theory of Objects
  by Martin Abadi and Luca Cardelli.
  Springer, ISBN 0-387-94775-2.
* This book develops a theory of objects as a foundation for
  object-oriented languages and programming. Our theory provides
  explanations for object-oriented notions in terms of a few basic
  primitives, and can be useful for the design and understanding of
  programming languages.

  ML for the Working Programmer (Second Edition)
  by L. C. Paulson
* The new edition of this successful and established textbook retains
  its two original intentions of explaining how to program in the ML
  language, and teaching the fundamentals of functional programming.
  The major change is the early and prominent coverage of modules,
  which are extensively used throughout. In addition, the first
  chapter has been totally rewritten to make the book more accessible
  to students who have no experience of programming languages. The
  main features of new Standard Library for the revised version of ML
  are described, and many new examples are given, e.g.  polynomial
  arithmetic and new ways of treating priority queues. Finally
  references have been completely updated.  The combination of careful
  explanation and practical advice will ensure that this textbook
  continues to be the preferred text for many courses on ML.
* Contents: 1. Standard ML; 2. Names, functions and types; 3. Lists;
  4. Trees and concrete data; 5. Functions and infinite data;
  6. Reasoning about functional programs; 7. Modules; 8. Imperative
  programming in ML; 9.  Writing interpreters for the lambda-calculus;
  10. A tactical theorem prover; Bibliography.
* Ordering details. To buy this or any Cambridge book on your
  credit card, fax (UK) ++44 (0)1223 325588 or ring ++44 (0)1223
* URL's. or

  The B-Book
  Assigning Programs to Meanings
  by J.-R. Abrial
* The B Method is a means of specifying, designing and coding software
  systems. It deals with the central aspects of the software
  lifecycle, namely technical specification, design by successive
  refinement, layered architecture and executable code
  generation. Each of these items is regarded as an activity that
  involves writing mathematical proofs, the totality of whose
  correctness validates the software system in question.  The B-book
  is an comprehensive account of the B Method, containing the
  mathematical basis on which it is founded, the definition of the
  notation used, and a large number of examples showing how to use the
  method in practice.  The B Method, in some sense the successor of
  the Z specification language, has already been successfully used in
  the development of real, safety-critical, software systems. It is
  here described for the first time in book form, which consequently
  makes this essential for all working on formal methods, in
  particular those involved in systems construction.
* Contents: Tribute; Foreword; Introduction; PART I. MATHEMATICS; 1.
  Mathematical reasoning; 2. Set notation; 3. Mathematical objects;
  PART II.  ABSTRACT MACHINES. 4. Introduction to abstract machines;
  5. Formal definition of abstract machines; 6. Theory of abstract
  machines; 7.  Constructing large abstract machines; 8. Examples of
  abstract machines; PART III. PROGRAMMING. 9. Sequencing and loop;
  10. Programming examples; PART IV. REFINEMENT. 11. Refinement;
  12. Constructing large software systems; 13. Examples of refinement;
  Appendix A; Summary of the most current notations; Appendix B;
  Syntax; Appendix C; Definitions; Appendix D; Visibility rules;
  Appendix E; Rules and axioms; Appendix F; Proof obligations; Index.
* Ordering details. To buy this or any Cambridge book on your
  credit card, fax (UK) ++44 (0)1223 325588 or ring ++44 (0)1223
* URL's. or

  Basic Proof Theory
  by A. S. Troelstra and H. Schwichtenberg
* This is an introduction to the basic ideas of structural proof
  theory, i.e.  the theory of formal proofs as combinatorial
  structures, with cut elimination and normalisation as central
  tools. There is a thorough discussion and comparison of various
  types of formalisation of first-order logic: in particular Hilbert
  systems, Gentzen systems and Natural Deduction. Examples are given
  of several areas of application. In each case the aim is to
  illustrate the methods in relatively simple situations and then
  apply them elsewhere in much more complex settings. There are
  numerous exercises throughout the text. In general, the only
  prerequisite is a standard course in first-order logic, so the book
  will be ideal for graduate students and beginning researchers in
  mathematical logic, theoretical computer science and artificial
* Contents: 1. Introduction; 2. N-systems and H-systems; 3. Gentzen
  systems; 4. Cut elimination with applications; 5. Refinements;
  6. Normalisation for natural deduction; 7. Resolution;
  8. Categorical logic; 9. Some non-standard logics; 10. Proof theory
  of first-order arithmetic; 11.  Second-order logic; Bibliography;
* Ordering details. To buy this or any Cambridge book on your
  credit card, fax (UK) ++44 (0)1223 325588 or ring ++44 (0)1223
* URL's. or

  The Concurrency Workbench of North Carolina (CWB-NC).
* The CWB-NC supports the automated verification of concurrent
  finite-state systems. Users interested in obtaining version 1.0 the
  system (free!) should consult the above URL. 

  16-18 April 1997,  Munich, Germany  
* Scope of the workshop.  Safety Critical Embedded Systems are
  becoming a major challenge for computer engineering.  The increasing
  demand for embedding more functions as computer software calls for
  new design technologies.  Several R&D projects have been devoted to
  these objectives in the last years, and new formal approaches are
  now proposed and operationally used, which range from specification,
  rapid prototyping and validation, down to code generation and
  testing.  The two european projects Eureka-SYNCHRON and
  Esprit-SACRES have decided to help for the dissemination of these
  technologies through the organization of the Workshop on Formal
  Design of Safety Critical Embedded Systems.
* Intended Participants.  This workshop is mainly targeted to R\&D
  engineers involved in the design of such systems.  It concentrates
  on the various formal technologies that have been developed
  recently, or are under development.
* Tutorials. J. Sifakis : Formal methods: overview; M. Broy :
  Requirements Engineering; F. Mejia : The B Method; D. Harel :
  Statecharts; G. Berry : Synchronous Languages; W. Damm : Model
  Checking.  C. Jard : Testing.
* Program Committee: A. Benveniste, co-chair, A. Poigne, co-chair,
  M. Broy, W. Damm, N. Halbwachs, J. Sifakis.
* Call for Exhibitors.  An exhibition will be organized, mainly for
  commercial tools, but also open to selected robust academic tools.
  Exhibition will be held throughout the second day of the workshop.
  In addition to demonstrating his tool, each exhibitor will have a
  slot to present it. Send a 3-5 pages abstract describing the tool.
  The abstract should be sent, or preferably mailed in Latex or
  postscript format, by November 30, 1996, to Albert Benveniste (tel
  +33 99 84 72 35), IRISA, Campus de Beaulieu, F 35042 Rennes cedex,

* The CMU Philosophy Department announces a tenure-track position at
  the Asst./ untenured Assoc. Prof. rank beginning Autumn, 1997. The
  area of specialization is logic and computability theory; candidates
  should have an excellent computer science background.  Applications
  should be sent to: Logic Search Committee; Department of Philosophy;
  CMU; Pittsburgh, PA 15213.  Applications will be accepted until
  January 15, those received and complete by December 16, 1996 will be
  assured of the most careful consideration. CMU is an Equal
  Opportunity Employer, and the department strongly encourages women
  and minority candidates to apply.  Candidates should include with
  their application a statement of research interests, a sample of
  written work, curriculum vitae, and evidence of teaching
  performance. Candidates should ask at least three referees to send
  confidential letters directly to the Department.

* The Institute for Logic, Language and Computation (ILLC) of The
  University of Amsterdam offers foreign students the possibility to
  become "Master of Logic" The Master of Logic program is a one-year
  curriculum with specializations in the areas of Mathematical Logic,
  Logic and Computer Science, and Logic, Philosophy and
  Linguistics. It is a full year program, consisting of course work
  and a Master's thesis. The required background is at least a
  Bachelor's, or equivalent degree in computer science, mathematics,
  philosophy or linguistics. In addition to the Master's program, ILLC
  also offers an international Certificate and a PhD program in Logic.
* Further information: URL above, or send an e-mail to (Ingrid van Loon). 

  June 3, 1997 -- June 7, 1997
  Call for Participation
  Grand Hotel Helios in Tarquinia Lido
* Topics: algebraic and other approaches to formal specification;
  structuring principles in system specifications; specification
  languages and methods; term rewriting and proof systems; systems
  (concepts, tools, etc.) for specification development .
* Invited speakers: C.Jones and U.Montanari. 
* Deadline for registration is March 1, 1997.