[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: firstname.lastname@example.org. Alternatively, submissions can be sent to: Dan Suciu, AT&T Labs-Research, 180 Park Avenue, Rm. B294, Florham Park, NJ 07932-0971, USA, email@example.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 firstname.lastname@example.org, 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 email@example.com, 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 firstname.lastname@example.org 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 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: 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. * For additional information about the position, consult the dean of 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: email@example.com, 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, firstname.lastname@example.org. * 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 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.