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 email@example.com 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 firstname.lastname@example.org. 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.