Newsletter 14, March 15, 1994


INTERNATIONAL CONFERENCE ON TYPED LAMBDA CALCULI AND APPLICATIONS (TLCA)
  April 10-12, 1995, Edinburgh, Scotland.
* Topics.  Proof theory of type systems, logic and type systems, typed
  lambda calculi as models of (higher order) computation, semantics of type
  systems, proof verification via type systems, type systems of programming
  languages, typed term rewriting systems.
* Program committee.  H. Barendregt, M. Dezani (Chair), J-Y. Girard,
  R. Hindley, F. Honsell, J. W. Klop, G. Longo, A. Meyer, G. Plotkin,
  P. Scott, J. Smith, J. Tiuryn.
* Submissions.  Electronic submission (PostScript only) is preferred; hard
  copy (6 copies required) will also be accepted.  Send to the address
  below.  Papers should not exceed 15 standard pages and should be
  accompanied by a one-page abstract.  The deadline for submissions is
  September 8, 1994.  It is intended to publish the accepted papers as a
  volume of the Springer Verlag Lecture Notes in Computer Science series.
* Conference secretariat.  TLCA Secretariat, Professor M. Dezani,
  Universita di Torino, Dipartimento di Informatica, Corso Svizzera, 185,
  10149 Torino, ITALY.  Tel: 39-11-7429232.  Fax: 39-11-751603.  Email:
  dezani@di.unito.it.

CALL FOR PARTICIPATION: LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS'94)
  St. Petersburg, Russia July 11--14, 1994.
* Topics.  Complexity of formal systems, constructive mathematics in
  computer science, denotational semantics of programs, descriptive
  complexity, dynamic logic, concurrent and distributed computational
  models, foundations of logic programming, generalized computability,
  lambda and combinatory calculi, logical foundations of database theory,
  logics for knowledge, modal and temporal logics, program verification,
  teaching computer science and logic, type theory in programming.
* Program committee.  A. Nerode (chair), S. Abiteboul, S.I. Adian,
  S.N. Artemov, H. Barendregt, A. Blass, G. Jager, V. Marek,
  Yu.V. Matijasevich, V.A. Nepomnyaschy, V.P. Orevkov, A.A. Razborov,
  J. Remmel, A. Scedrov, M.A. Taitslin, M. Vardi.
* Further information.  1.  LFCS'94 Secretariat, Laboratory of Mathematical
  Logic, Steklov Institute of Mathematics, 27 Fontanka, St.Petersburg
  191011, RUSSIA, lfcs@sovam.com (phone: + 7 (812) 311-4392, FAX: + 7
  (812) 310-5377).  2.  LFCS'94, Mathematical Sciences Institute, Cornell
  University, 407 College Ave., Ithaca, NY 14850, USA,
  lfcs@msiadmin.cit.cornell.edu (phone: + 1 (607) 255-7752, FAX: + 1 (607)
  255-8005).

THE VIII-TH BANFF HIGHER ORDER WORKSHOP
LOGICS FOR CONCURRENCY: STRUCTURE VS AUTOMATA
  The Banff Centre, Banff, Alberta, Canada, Aug. 27 - Sept. 3, 1994.
This year's BANFF Higher Order Workshop is based on the theme of Logics for
Concurrency.  It is mainly intended for graduate students and researchers
already interested in concurrency theory and/or temporal logics who want a
kick start into selected central themes.
* Lecture Series.  Samson Abramsky, Interaction Categories.  E Allen
  Emerson, Automated Temporal Reasoning about Reactive Systems.  Yoram
  Hirshfeld and Faron Moller, Algorithms for Normed Processes.  Colin
  Stirling, Modal and Temporal Logics for Processes.  Moshe Y Vardi, An
  Automata-Theoretic Approach to Program Specification and Verification.
* Cost.  $1200 (CAN).  Includes food, accommodation and taxes.
* Further information.  Graham Birtwistle, Department of Computer Science,
  University of Calgary, Calgary T2N 1N4, CANADA.  tel: +1 (403) 220 6055.
  fax: +1 (403) 284 4707.  net: graham@cpsc.ucalgary.ca.

ICLP'94 POST-CONFERENCE WORKSHOP ON
PROOF-THEORETICAL EXTENSIONS OF LOGIC PROGRAMMING
  S. Margherita Ligure, Italy, 17 June 1994. 
* Topics.  Proof-theoretic foundations: cut elimination;
  negation-as-failure; equational theories; program completion; reasoning
  by induction; partial inductive definitions; linear logic; constructive,
  modal and temporal logics; many-valued logics; higher-order logics;
  type-theoretic approaches.  Languages: Elf; GCLA; Isabelle; lambda
  Prolog; LO!; Lolli; ACL.  Applications: program synthesis,
  transformations and equivalence; program termination; unification theory
  and constraints; theorem proving; programming language implementations;
  modularity; knowledge representation.
* Organizing Committee.  Lars-Henrik Eriksson, Roy Dyckhoff, Alberto
  Momigliano, Mario Ornaghi.
* Submissions.  Electronic submissions in LaTeX, DVI or Postcript format of
  extended abstracts (up to 5 pages) are strongly encouraged, preferably
  following the Springer style.  Deadline is March 31.  Post-conference
  in-depth review of submitted papers for publication will be considered.
* Contact person.  Alberto Momigliano, Department of Philosophy, Carnegie
  Mellon University, Pittsburgh, PA 15213-3890, U.S.A.  Telephone: +1 412
  268-8047.  FAX: +1 412 268-1440.  Email: mobile@lcl.cmu.edu.
* Further information.  By anonymous ftp from launce.lcl.cmu.edu in
  directory /pub/whop94.
 
INTERNATIONAL CONFERENCE ON COMPILER CONSTRUCTION (CC'94), 7-9 April 1994
EUROPEAN SYMPOSIUM ON PROGRAMMING (ESOP'94), 11-13 April 1994
COLLOQUIUM ON TREES IN ALGEBRA AND PROGRAMMING (CAAP'94), 11-13 April 1994
  Edinburgh, Scotland
* Invited Speakers.  L. Cardelli, H. Comon, J. Engelfriet, R. Milner, 
  K. Nygaard.
* Programme, registration information.  By anonymous ftp in
  /pub/dts/CAAP-ESOP-CC on ftp.dcs.ed.ac.uk.
* Information.  CAAP/ESOP/CC'94, LFCS, Dept. of Computer Science, Univ. of
  Edinburgh, Edinburgh EH9 3JZ, Scotland; e-mail tlc@lfcs.ed.ac.uk.

1ST INT'L CONF ON CONSTRAINTS IN COMPUTATIONAL LOGICS (CCL)
  September 7-9, 1994, Munich, Germany.
* Topics.  CCL covers theoretical and practical issues in the direction
  of combining and extending programming paradigms preferably (but not
  exclusively) by using constraints. Suggested, but not exclusive, topics
  of interest include: symbolic constraints, set constraints, numerical
  constraints, constraints for knowledge representation and processing, use
  of constraints for type checking and program analysis, multi-paradigm
  programming, abstract properties of combined calculi, combinations of
  computational logics, constraints in rewriting, deduction, and symbolic
  computations, working systems.
* Invited lecturers.  Max Dauchet, Dexter Kozen, Helmut Simonis, Gert
  Smolka, Wayne Snyder.
* Submissions.  5 hard copies of a full paper, 16 additional copies of
  the cover page and second page should be received by March 25, 1994 by
  the program chair. Late submissions will not be considered.
* Program chair.  Jean-Pierre Jouannaud, LRI, Bat. 490, CNRS et
  Universite de Paris-Sud, 91405 Orsay Cedex, FRANCE.  E-mail: ccl@lri.fr.
  Phone: (33) 1-69416905.  Fax: (33) 1-69416586.
* Program committee.  A. Aiba, A. Colmerauer, M. Dincbas, H. Ganzinger,
  S. Haridi, V. Hentenryck, J. Jaffar, J.-P. Jouannaud, C. Kirchner,
  D. Miller, U. Montanari, F. Orejas, L. Pacholski, F. Pfenning,
  M. Rodriguez, K. Schulz, M.Wallace.
* Further Information.  Helene.Kirchner@loria.fr.

WORKSHOP ON PROOF THEORY, COMPLEXITY, METAMATHEMATICS
  April 5--8, 1994, University of Technology, Vienna, Austria.
* The aim of this workshop is to bring together researchers working on
  the interrelations between proof theory of logical and mathematical
  systems on the one hand and computation and complexity on the other.
* Invited Speakers.  Arnon Avron, Matthias Baaz, Alessandro Berarducci,
  Alessandra Carbone, Vincent Danos, Elmar Eder, Lavinia Egidi, Giovanni
  Faglia, Georg Gottlob, Jean-Baptiste Joinet, Jan Krajicek, Alexander
  Leitsch, Vladimir Orevkov, Soren Riis, Michel Parigot, Pavel Pudlak,
  Piotr Wojtylak.
* Information.  Kurt Goedel Society, Technische Universitaet Wien,
  Institut fuer Computersprachen E185.2, Resselgasse 3/1, A-1040 Wien,
  Austria.  Phone: (+43 1) 588 01 ext 4088. Fax: (+43 1) 504 1589. Email:
  kgs@logic.tuwien.ac.at.

COURSE: INTRODUCTION TO THEOREM PROVING, USING "ISABELLE"
  11-13 July 1994, University of Cambridge.
* The aim of this course is to introduce participants to the Isabelle
  system, developed at Cambridge University, and used since 1986 in
  research establishments.  Isabelle has built-in support for several
  logics, including first-order logic (FOL), higher-order logic (HOL),
  Zermelo-Fraenkel set theory (ZF) and extensional Constructive Type Theory
  (CTT).  New logics can also be introduced by specifying their abstract
  syntax, notation, and inference rules.  This feature makes Isabelle
  uniquely flexible, applicable to many domains.
* Course fee.  650 pounds sterling, 350 pounds sterling for academic
  participants.
* Information.  Larry.Paulson@cl.cam.ac.uk

NEW BOOK:  MATHEMATICS OF MODALITY, ROBERT GOLDBLATT
* Abstract.  This volume collects together a number of the author's papers
  on modal logic, beginning with his doctoral thesis about the duality
  between algebraic and set-theoretic models, and including two completely
  new articles, one on infinitary rules of inference, and the other about
  recent results on the relationship between modal logic and first-order
  logic. Another paper on the "Henkin method" in completeness proofs has
  been substantially extended to give new applications. Other articles are
  concerned with quantum logic, provability logic, the temporal logic of
  relativistic spacetime, modalities in topos theory, and the logic of
  programs.
* Publisher.  CSLI Publications, Stanford University.  Distributed by
  University of Chicago Press.  CSLI Lecture Notes No. 43, 273pp, 1993.
* Price. US $22.95 (paper), ISBN 1-881526-23-2; $45.95 (cloth)  
  ISBN  1-881526-24-0.
* Further information.  CSLI: pubs@csli.stanford.edu; or or University 
  of Chicago Press: dblobaum@press.uchicago.edu.