Newsletter 71

January 13, 2001
TABLE OF CONTENTS
* Calls for Papers
  Workshop on Logic and Learning
  Symposium on Theoretical Aspects of Computer Software
  Workshop on Implicit Computational Complexity
  Workshop on Logic and Complexity in Computer Science
  Conference on the Mathematical Foundations of Programming Sematics
* Calls for Participation
  Workshop on The Unusual Effectiveness of Logic in Computer Science
  Workshop on Formal Design of Safety Critical Embedded Systems
  Summer School on Formalware Engineering
  Summer School on Logical Methods
* Book Announcements
  Dynamic Logic by David Harel, Dexter Kozen, and Jerzy Tiuryn
  A Short Introduction to Intuitionistic Logic by Grigori Mints


WORKSHOP ON LOGIC AND LEARNING
  (affiliated with LICS 2001)
  Call for Papers
  Boston, June 19 - 20, 2001
  http://www.eecs.tufts.edu/~roni/LicsWksp/
* Logic has been used as the underlying representation language in many
  areas of AI including machine learning.  There are theoretical results
  on learning in propositional logic as well as for logic programs,
  description logic, and fragments of first-order logic. The techniques
  applied are probabilistic and combinatorial, recursion theoretic, proof
  theoretic, and model theoretic. The workshop has a two-fold objective:
  to provide an introduction to the area for those who work in other LICS
  areas and are interested in applying logic to learning, and to provide a
  forum for research in the area of logic learning.
* Submission Deadline: March 15, 2001
* Confirmed invited speakers: Arun Sharma (University of New South
  Wales) and Leslie Valiant (Harvard University). 
* Workshop Organizers: Roni Khardon (Tufts University), Gyorgy Turan 
  (University of Illinois at Chicago).
* Program committee: J. Lloyd (ANU, Australia), E. Martin (UNSW, Australia),
  S. Muggleton (University of York, UK), P. Tadepalli (Oregon State 
  University, USA), A. Yamamoto (Hokkaido University, Japan).


4TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER
SOFTWARE (TACS 2001)
  Call for Papers
  Sendai, Japan, October 29 - 31, 2001
  http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/
* Theme. Theoretical aspects of the design, semantics, analysis, and
  implementation of programming languages and systems; logics of
  programs; calculi and models of concurrency and parallel
  computation; theories of mobile computation and system security;
  categories and types in computer science; formalisms, methods, and
  systems for program specification, verification, synthesis, and
  optimization; constructive, linear, and modal logics in computer
  science.  
* Submission. Max. 6000 words (see the URL above for details).
* Submission Deadline. April 1, 2001.  
* General Chair. Takayasu Ito 
* Program committee. Z. Ariola, C. Fournet, J. Garrigue, M. Hagiya,
  R. Harper, M. Hasegawa, N. Heintze, M. Hofmann, Z. Hu, N. Kobayashi
  (co-chair), M. Odersky, C. Palamidessi, B. Pierce (co-chair),
  F. Pottier, A. Scedrov, N. Shankar, I. Stark, M. Tatsuta


3rd INTERNATIONAL WORKSHOP ON IMPLICIT COMPUTATIONAL COMPLEXITY (ICC'01)
  (affiliated with PADO and MFPS)
  May 20, 2001
  Aarhus, Denmark
  http://www.dcs.ed.ac.uk/home/mxh/ICC01.html
* Topics. The synergy between Logic, Computational Complexity and
  Programming Language Theory has gained importance and vigour in
  recent years, cutting across areas such as Proof Theory, Computation
  Theory, Applicative Programming, and Philosophical Logic. Several
  machine-independent approaches to computational complexity have been
  developed, which characterize complexity classes by conceptual
  measures borrowed primarily from mathematical logic. Collectively
  these approaches might be dubbed IMPLICIT COMPUTATIONAL COMPLEXITY.
  Practically, implicit computational complexity provides a framework
  for a streamlined incorporation of computational complexity into
  areas such as formal methods in software development, programming
  language theory. In addition to research reports on theoretical
  advances in implicit computational complexity, practical
  contributions bridging the gap between Computational Complexity and
  Programming Language Theory are therefore of particular interest.
* Program Committee. Samson Abramsky (University of Oxford, UK)
  Martin Hofmann (University of Edinburgh, UK) (Chair) Bruce Kapron
  (University of Victoria, Canada) Harry Mairson (Brandeis University)
  Jean-Yves Marion (Loria, Nancy, France) So/ren Riis (Queen Mary and
  Westfield College, London) Helmut Schwichtenberg (University of
  Munich, Germany)
* Important Dates.
  16 March 2001 Submission deadline 
  10 April 2001 Notification of authors of accepted papers 
  20 May 2001  Workshop


INTERNATIONAL WORKSHOP ON LOGIC AND COMPLEXITY INCOMPUTER SCIENCE (LCCS'2001)
  Call for Papers
  Creteil, FRANCE, September 3-5 2001
  http://www.univ-paris12.fr/~lacl/LCCS2001
* Aim: The workshop is held to honour Anatol Slissenko and his
  outstanding contributions towards advancing computer science on
  occasion of his 60th anniversary. The aim of the workshop is to
  provide a forum for the exchange of results in the area of logic and
  complexity applied to computer science. The preferable topics to be
  presented are those connected with scientific interests of
  A.O. Slissenko.
* Topics: Papers are solicited in all research areas related to logic
  and complexity applied to computer science, including but not
  limited to : logic and computability, proofs search in the
  propositional and predicate calculi, complexity of combinatorial and
  geometrical problems, model checking, software specification,
  verification.
* Paper submission: Authors are invited to send three copies of an
  abstract not exceeding ten pages to: Danièle Beauquier, LACL
  University Paris 12, 61 Av. du Général de Gaulle, 94 010 CRETEIL,
  France. 
  Electronic submissions in the form of postscript files are
  encouraged and can be sent to beauquier@univ-paris12.fr Submissions
  are to be received before May 2, 2001.  
* Program committee : D. Beauquier ( Créteil, co-chair), M. de
  Rougemont (Paris), E. Grandjean (Caen), Y. Gurevich (Microsoft),
  Y. Matijassevich (St Petersb., co-chair), D. Niwinski (Warsaw),
  A. Rabinovich (Tel Aviv), W. Thomas (Aachen), K. Wagner (Würzburg).


17th CONFERENCE ON THE MATHEMATICAL FOUNDATIONS OF PROGRAMMING
SEMANTICS (MFPS 17)
  Call for Papers
  Aarhus, Denmark
  May 24-27
  http://www.math.tulane.edu/mfps17.html
* Submissions in areas traditionally represented at MFPS, as well as
  in related areas, are encouraged. Details about the meeting and
  about submission process can be found on the MFPS 17 home page.
* The deadline for submissions also has been extended, til January 15,
  2001.


NSF/CISE WORKSHOP ON THE UNUSUAL EFFECTIVENESS OF LOGIC IN COMPUTER SCIENCE
  Call for Participation
  Room 110, National Science Foundation, Arlington, VA
  January 22, 2001
  http://www.cs.rice.edu/~vardi/logic/
* Background: During the past twenty five years there has been
  extensive, continuous, and growing interaction between logic and
  computer science.  In many respects, logic provides computer science
  with both a unifying foundational framework and a tool for modeling.
  In fact, logic has been called ``the calculus of computer science''.
  This workshop will provide an overview of the surprising
  effectiveness of logic in computer science by presenting some of the
  areas in which logic played a crucial role in computer science.
* Speakers. 
  Moshe Y. Vardi: Logic as The Calculus of Computer Science
  Ken McMillan: The Role of Logic in Computer Systems Verification
  Victor Vianu: Logic as a Query Language--from Frege to XML
  Neil Immerman: Descriptive Complexity
  Peter Lee: Types, Proofs, and Safe Mobile Code--Programming
             Languages in an Interconnected World
  Jon Millen: Applications of Logic in Computer Security
  (followed be a general discussion)
* Organizer: Moshe Y. Vardi
* The meeting is open to the general public.
  For more details see http://www.cs.rice.edu/~vardi/logic/ or
  contact vardi@cs.rice.edu.


WORKSHOP ON FORMAL DESIGN OF SAFETY CRITICAL EMBEDDED SYSTEMS
  Call for Participation 
  March 21 - 23, 2001
  Munich, Germany
  http://ais.gmd.de/~ap/femsys
* Scope. The Workshop on "Formal Design of Safety Critical Embedded
  Systems" aims at disseminating new technologies for embedded
  systems. It is targeted to R&D engineers who are involved in the
  design of embedded systems, and in particular, Safety Critical
  Embedded Systems.  It concentrates on the various formal
  technologies that have been developed recently, or are under
  development.
* Format. The workshop combines academic tutorials and industrial
  user's lectures with a tool exhibition. Tutorials and user's lecture
  will address the following themes: OO design of reactive systems,
  UML, Notations & Formalisms, Distributed platforms & middle ware, in
  relation to safety critical & embedded systems, Deployment on
  distributed architectures, Static analysis & related topics,
  Testing, Model checking & related topics.
  Major tool vendors will exhibit their tools. Additionally industrial
  tools will be presented as well as a couple of mature academic
  tools.
* Program Committee.  Albert Benveniste co-chair (Inria, Rennes,
  France) Axel Poigné co-chair (GMD, Sankt-Augustin, Germany) Manfred
  Broy (Tech. Univ. München, Germany) Werner Damm (OFFIS, Oldenburg,
  Germany) Nicolas Halbwachs (Verimag, Grenoble, France) Bengt Jonsson
  (Uppsala University, Sweden) Amir Pnueli (Weizman Institute,Israel)


SUMMER SCHOOL ON FORMALWARE ENGINEERING - FORMAL METHODS FOR
ENGINEERING SOFTWARE
  Udine/Italy, 
  September 24-28, 2001
  http://www.cism.it/c2001/c07/index.htm
* Courses on ASM, B, VDM, PVS, Model Checking, LF (of five lectures
  each) by Abrial, Boerger, Buettner, Gorm Larsen, Gurevich, Honsell,
  Shankar


EEF SUMMER SCHOOL ON LOGICAL METHODS
  BRICS, University of Aarhus, Denmark 
  June 25-July 6, 2001
  http://www.brics.dk/LogicsSchool01/
  E-mail: LogicsSchool01@brics.dk.
* Courses.
  M. Bezem (Bergen): Type Theory, 
  R. Crole (Leicester): Categorical Logic, 
  U. Kohlenbach (Aarhus): Computational Content of Proofs, 
  O. Kupferman (Jerusalem): Model Checking, 
  J. Makowsky (Haifa): Model theoretic methods in combinatorics 
                       and complexity, 
  A. Scedrov (Philadelphia): Logic in Computer Security, 
  C. Schuermann (Yale): Logical Frameworks, 
  J. Tucker (Swansea): Computable functions on many sorted algebras, 
  A. Voronkov (Manchester): Proof Theory and Automated Deduction, 
  I. Walukiewicz (Warsaw): Automata and Logic. 
* Registration. An electronic registration form will soon be available
  on the schools website mentioned above.
* Grants. A limited number of grants are available for students,
  covering registration, accommodation and living expenses during the
  school, leaving only travel expenses to be paid. Applications for
  grants is made as part of the electronic registration.
* Organizing Committee. Janne Christensen, Ulrich Kohlenbach, Mogens
  Nielsen, Glynn Winskel.
* The school is co-sponsored by the European Educational Forum (EEF)
  and BRICS (Basic Research in Computer Science) funded by the Danish
  National Research Foundation.


BOOK ANNOUNCEMENT
  Dynamic Logic
  by David Harel, Dexter Kozen, and Jerzy Tiuryn
  MIT Press, ISBN 0-262-08289-6
  http://mitpress.mit.edu/promotions/books/HAR1DHF00
* Among the many approaches to formal reasoning about programs,
  Dynamic Logic enjoys the singular advantage of being strongly
  related to classical logic. Its variants constitute natural
  generalizations and extensions of classical formalisms. For example,
  Propositional Dynamic Logic (PDL) can be described as a blend of
  three complementary classical ingredients: propositional calculus,
  modal logic, and the algebra of regular events. In First-Order
  Dynamic Logic (DL), the propositional calculus is replaced by
  classical first-order predicate calculus. Dynamic Logic is a system
  of remarkable unity that is theoretically rich as well as of
  practical value.  It can be used for formalizing correctness
  specifications and proving rigorously that those specifications are
  met by a particular program.  Other uses include determining the
  equivalence of programs, comparing the expressive power of various
  programming constructs, and synthesizing programs from
  specifications.
* This book provides the first comprehensive introduction to Dynamic
  Logic.  It is divided into three parts. The first part reviews the
  appropriate fundamental concepts of logic and computability theory
  and can stand alone as an introduction to these topics. The second
  part discusses PDL and its variants, and the third part discusses DL
  and its variants. Examples are provided throughout, and exercises
  and a short historical section are included at the end of each
  chapter.


BOOK ANNOUNCEMENT
  A Short Introduction to Intuitionistic Logic
  by Grigori Mints
  Kluwer Academic/Plenum Publishers, 2000
* Intuitionistic logic is presented here as part of familiar classical
  logic which allows mechanical extraction of programs from proofs. To
  make the material more accessible, basic techniques are presented
  first for propositional logic; Part II contains extensions to
  predicate logic. This material provides an introduction and a safe
  background for reading research literature in logic and computer
  science as well as advanced monographs. Readers are assumed to be
  familiar with basic notions of first order logic. One device for
  making this book short was inventing new proofs of several
  theorems. The presentation is based on natural deduction. 
* The topics include programming interpretation of intuitionistic
  logic by simply typed lambda-calculus (Curry-Howard isomorphism),
  negative translation of classical into intuitionistic logic,
  normalization of natural deductions, applications to category
  theory, Kripke models, algebraic and topological semantics,
  proof-search methods, interpolation theorem. 
* The text developed from material for several courses taught at
  Stanford University in 1992-1999.





Back to the LICS web page.

Martin Grohe