ONLINE LICS BIBLIOGRAPHY UPDATED Now includes all papers from the Eighth meeting, June 1993. The bibliography is in BibTeX format and all entries for LICS 8 have abstracts. * Retrieval via mail server. Send message with body "send meyer lics.bib" to archive-server@theory.lcs.mit.edu. Using "send meyer Index" as the body gets an index of other available files; "help" gets server info. * Retrieval via ftp. Ftp to theory.lcs.mit.edu [18.52.0.92], login as "anonymous", password "guest", get file pub/meyer/lics.bib. INTERNATIONAL CONF. ON PROOF THEORY, PROVABILITY LOGIC, AND COMPUTATION University of Berne, Switzerland, March 20--24, 1994. PPC provides a platform for the presentation of recent results in the areas of Proof Theory, Provability Logic, and Computation where these are interrelated. * Topics. Applications of proof theory to theoretical computer science; new developments in provability logic related to computer science; new challenges from computer science for proof theory and provability logic. * Submissions. Send an extended abstract (2 pages) by January 5, 1994 to the address below. * Invited Speakers. L. Beklemishev, D. de Jongh, W. Buchholz, F. Montagna, S. Buss, R.F. Stark, R. Constable, A.S. Troelstra, P. Hajek. * Program Committee. S. Artemov, S. Feferman, G. Boolos, G. Jager, E. Engeler, A. Visser. * Information. PPC '94, Institut fur Informatik und, angewandte Mathematik, Universitat Bern, Langgassstrasse 51, CH--3012 Bern. Fax: +41 31 65 39 65. E-mail: ppc@iam.unibe.ch. CONFERENCE ON COMPUTER-AIDED VERIFICATION Stanford University, Stanford, California, USA. June 21-24, 1994. CAV is dedicated to the advancement of the theory and practice of computer-assisted formal verification. * Topics. Application areas: synchronous and asynchronous circuits, computer arithmetic, protocols, distributed algorithms, real-time systems, hybrid systems. Methods based on: automata, model-checking, automated deduction. Theoretical issues: decidability of verification problems and logics, computational complexity results, verification algorithms. * Submissions. Electronic submission of postscript required. Receipt deadline: January 14, 1994. 10 page maximum. * Program Chair. David L. Dill, CIS 135, Stanford, CA, 94305-4070. cav@cs.stanford.edu. * Program Committee. R. Alur, R. Bryant, R. Brayton, R. Cleaveland, C. Courcoubetis, R. de Simone, A. Emerson, M. Fujita, S. German, O. Grumberg, N. Halbwachs, G. Holzmann, K. Larsen, K. McMillan, L. Paulson, N. Shankar, F. Somenzi, B. Steffen, P. Varaiya, P. Wolper, T. Yoneda. FIRST INTERNATIONAL CONFERENCE ON TEMPORAL LOGIC Gustav Stresemann Institut, Bonn, Germany, July 11-14, 1994. ICTL attempts to create bridges between the various communities working in Temporal Logic. * Topics. Pure temporal logic, specification and verification, temporal aspects in AI, modelling tense and aspect in natural language, temporal databases, temporal theorem proving, tools, planning and change, temporal logic programming. * Submissions. 4 copies, received by December 20, 1993. There are 4 categories of papers: research papers (at most 15 pages), survey papers (30 pages), position papers (5 pages), and system descriptions (3 pages). Papers must specify category and topic. Latex style file available. * Program Chair. Dov M. Gabbay, Imperial College of Science, Technology and Medicine, Dept. of Computing, Huxley Bld., 180 Queen's Gate, London SW7 2AZ, England. Tel: +44 71 225 8447. Fax: +44 71 581 8024. Email: dg@doc.ic.ac.uk * Program Committee. J. Allen, H. Barringer, J. van Benthem, G. Brewka, E. Clarke, N. Francez, D. M. Gabbay, M. Georgeff, H. Kamp, I. Nemeti, H. J. Ohlbach, A. Pnueli, A. Porto, W. de Roever, E. Sandewall, A. Sernadas, Y. Shoham, A. Szalas. * Invited Speakers. James Allen, Johan van Benthem, Hans Kamp, Amir Pnueli. SYMPOSIUM ON LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS '94) St. Petersburg, Russia, July 14--18, 1994. * Topics. Broad range, including: 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. * Submissions. 4 copies of an extended abstract (limit 3000 words), received by Nov 29, 1993. Electronic submissions accepted (contact lfcs@msiadmin.cit.cornell.edu for details). Submissions may be sent to: Dr. E.Ya. Dantsin, Laboratory of Mathematical Logic, Steklov Institute, of Mathematics, 27 Fontanka, St.Petersburg 191011, RUSSIA, logic@sovam.com (phone: + 7 (812) 311-4392, FAX: + 7 (812) 310-5377); or, outside the former USSR: 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). INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP'94) S. Margherita Ligure, Italy, 13-18 June 1994. ICLP'94 is one of the two major annual international conferences reporting recent research results in logic programming. * Topics. Topics include: applications, language design, architecture, natural language, artificial intelligence, parallelism, concurrency, programming methodology, constraints, proof theory, databases, semantics and foundations, environments, static analysis, higher order programming, theorem proving, implementation, types, * Submissions. 6 copies of a paper (limit 15 pages), including a 200 word abstract, by Nov. 15, 1993, to Pascal Van Hentenryck, Brown University, Box 1910, Providence, RI 02912 (USA). Email: pvh@cs.brown.edu. Phone: +1 401 863 76 34. Fax: +1 401 863 76 57. * Program committee. K. Ali, M. Bruynooghe, P. Codognet, Y. Deville, H. Gallaire, C. Hogger, J. Jaffar, G. Levi, J. Maluszinski, K. Marriott, M. Martelli, L. Naish, F. Pfenning, D. Poole, A. Porto, R. Ramakrishnan, M. Rodriguez-Artalejo, G. Smolka, V.S. Subrahmanian, P. Szeredi, E. Tick, K. Ueda, P. Van Hentenryck (chair), P. Van Roy, A. Voronkov, M. Wallace, R. Yang SECOND INTERNATIONAL CONFERENCE ON THEOREM PROVERS IN CIRCUIT DESIGN: THEORY, PRACTICE AND EXPERIENCE Bad Herrenalb (Blackforest), Germany, September 26-29, 1994. TPCD provides a forum for discussing the role of theorem provers in the design of digital systems. * Submissions. Send five copies of a complete paper by March 25, 1994, to the address below. Maximum length: 6000 words. E-mailed postscript accepted. Use of benchmark circuits encouraged (ftp from goethe.ira.uka.de after Dec 3). * Program Committee. D. Borrione, H. Busch, L. Claesen, H. Eveking, S. Finn, M. Gordon, K. Hanna, W. A. Hunt Jr., P. Loewenstein, M. Leeser, T. Melham, T. Nipkow, D. Shepherd, J. Staunstrup, V. Stavridou, P. Subrahmanyam. Program chair: Mike Fourman. * Information. Ramayya Kumar, TPCD Conference Chair, Forschungszentrum Informatik, Department - ACID, Haid-und-Neu Strasse 10-14, 76131 Karlsruhe, Germany. Tel: (+49) 721 9654-419. Fax: (+49) 721 9654-459. kumar@fzi.de. STRUCTURE IN COMPLEXITY THEORY (STRUCTURES 94) CWI & The University of Amsterdam, Amsterdam, The Netherlands, June 28 -- July 1, 1994. The conference seeks original research papers or technical expositions in *all* areas of complexity theory. * Topics. Topics include: structure of complexity classes, properties of complete sets, resource-bounded reducibilities, theory of relativizations, circuit complexity, complexity and logic, interactive proof systems, Kolmogorov complexity, structural aspects of distributed and parallel computing, cryptographic complexity. * Submission. Send 10 copies of an extended abstract to Uwe Schoening, Univ. Ulm, Abteilung Theoretische Informatik, D 89069 Ulm, Germany. (email: schoenin@informatik.uni-ulm.de.) NOTE: papers *must* be at most 10 pages and be received by Dec. 1, 1993 to guarantee consideration. * Program Committee. U. Schoening (chair), A. Condon, R. Gavalda, J Hartmanis, U Hertrampf, N Immerman, N. Nisan, R. Reischuk, L. Torenvliet. * Ftp site. top.cis.syr.edu (128.230.31.4), pub/structures contains Structures related documents, including conference announcements, past issues of the Structures Abstracts, and past conference attendance lists. UNIFICATION THEORY INTRODUCTION AND OVERVIEW Unification Theory, F. Baader and J.H. Siekmann. In "Handbook of Logic in Artificial Intelligence and Logic Programming}, D.M. Gabbay and C.J. Hogger and J.A. Robinson (eds.), Oxford University Press, Oxford, UK (to appear). * FTP version. A Postscript or DVI version of this paper can be obtained via anonymous ftp from "duck.dfki.uni-sb.de", directory pub/papers. (Login as "ftp" and use your e-mail address as password.) The file "abstracts" contains abstracts of other available papers. NEW TEXTBOOK: CATEGORIES FOR TYPES available shortly. Roy L. Crole, Imperial College, University of London. Cambridge Mathematical Textbooks, Cambridge University Press. ISBN 0521 450926 (HB). Explains the basic principles of categorical type theory and illustrates some of the techniques used to derive categorical semantics for specific type theories. For advanced undergraduates and beginning graduates. Includes introduction to category theory. SACKS PRIZE FOR BEST LOGIC DISSERTATION in honor of Gerald Sacks. To be awarded on a regular basis by a committee of distinguished logicians. Contributions in support of the award are requested. Some matching funds have been obtained. Checks should be made payable to the Sacks Prize Fund, and sent to Ms. Carla Kirmani, Administrative assistant, Department of Mathematics, MIT, Cambridge, MA 02139, ATTN: Sacks Prize Fund. 2ND CONFERENCE ON INFORMATION AND KNOWLEDGE MANAGEMENT Washington, DC, Nov. 1-5, 1993. CIKM-93 will provide an international forum for the presentation and discussion of research on the management of information and knowledge. The scope of the conference will cover the integration of database technology, knowledge representation and reasoning, information retrieval, and techniques for locating and accessing relevant data and knowledge in very large, distributed information systems. * Advance program, further information. Send email to CIKM-INFO@CS.UMBC.EDU to get automated reply, or ftp from ftp.cs.umbc.edu:pub/cikm/. * General inquiries. CIKM-93, C.S. Department, U. of Maryland Baltimore County, Baltimore, MD 21228. cikm@cs.umbc.edu. phone: 410-455-3000, fax: 410-455-3969. INTERNATIONAL WORKSHOP ON HIGHER ORDER ALGEBRA, LOGIC & TERM REWRITING (HOA'93) CWI, Amsterdam, The Netherlands, September 23-24, 1993. * Final program. Anonymous ftp: ftp.cwi.nl:pub/gipe/HOA93.txt. CATEGORY THEORY MEETING Category Theory Research Center, Mcgill University, Oct 9-10, 1993. * Information. Tom Fox, Dept of Mathematics and Statistics, McGill University, 805 Sherbrooke West, Montreal, Quebec, Canada, H3A 2K6. fox@triples.math.mcgill.ca. MAMLS @ RUTGERS/DIMACS Sept. 18, 1993 * Location. Room 705 Hill Center, Busch Campus, Rutgers. * Speakers: A. Macintyre, A. Borovik, M. Kojman, J. Lynch, S. Shelah.