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.