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