Because of the AT&T breakup, LICS has new URL's: * FTP site. ftp://ftp.research.bell-labs.com/dist/lics/ * WWW homepage. http://www.bell-labs.com/topic/conferences/lics/ * Contact. lics-request@research.bell-labs.com. JOURNAL OF AUTOMATED REASONING SPECIAL ISSUE ON FORMAL PROOF * 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, fp@cs.cmu.edu, http://www.cs.cmu.edu/~fp/ 6TH INTERNATIONAL CONFERENCE ON DATABASE THEORY (ICDT '97) 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 teo@softlab.ece.ntua.gr. BOOK ANNOUNCEMENT 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. BOOK ANNOUNCEMENT 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 325970. * URL's. http://www.cup.cam.ac.uk/ or http://www.cup.org/. BOOK ANNOUNCEMENT 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 325970. * URL's. http://www.cup.cam.ac.uk/ or http://www.cup.org/. BOOK ANNOUNCEMENT 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 intelligence. * 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; 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 325970. * URL's. http://www.cup.cam.ac.uk/ or http://www.cup.org/. SOFTWARE RELEASE ANNOUNCEMENT 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. WORKSHOP ON FORMAL DESIGN OF SAFETY CRITICAL EMBEDDED SYSTEMS (FEmSys '97) 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, France, Albert.Benveniste@inria.fr. POSITION IN LOGIC AT CARNEGIE MELLON UNIVERSITY * 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. MASTER OF LOGIC PROGRAM * 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 illc@wins.uva.nl (Ingrid van Loon). FIRST EUROCONFERENCE ON ALGEBRAIC DEVELOPMENT TECHNIQUES and 12th WORKSHOP ON ABSTRACT DATA TYPES 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.