[Past issues of the newsletter are available at http://www.bell-labs.com/topic/conferences/lics/] BOOK ANNOUNCEMENT Descriptive Complexity by Neil Immerman Springer Verlag, 1999, ISBN 0-387-98600-6 http://www.springer.de * Computational complexity was originally defined in terms of the natural entities of time and space, and the term complexity was used to denote the time or space used in the computation. Rather than checking whether an input satisfies a property S, a more natural question might be: what is the complexity of expressing the property S? These two issues --- checking and expressing --- are closely related. It is startling how closely tied they are when the latter refers to expressing the property in first-order logic of finite and ordered structures. Begun in 1974 by Fagin, descriptive complexity has characterized all major notions of complexity in terms of the richness of logical languages needed to describe problems. Descriptive complexity is part of finite model theory, and it ties together logic and computer science. It has major applications to the theory of databases and computer-aided verification. * This self-contained textbook introduces the methods and results of descriptive complexity together with its applications. With many examples and exercises, it may be used for a graduate or advanced undergraduate course. * Ordering information. See the URL above or call Springer. MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS XV) Tulane University, New Orleans, April 28 - May 1, 1999 Call for participation http://www.math.tulane.edu/mfps15.html * See the above URL for further information. WORKSHOP ON FINITE MODEL THEORY AND ITS APPLICATIONS Trento, Italy, July 1, 1999 (part of FLoC'99) Call for contributions http://www.cs.bell-labs.com/~libkin/fmt-floc/ * The interactions between finite model theory and computer science have expanded both in depth and in scope in recent years. Well-established connections, such as those between finite model theory and complexity theory and with relational databases, remain extremely fruitful. In addition, there are newer connections, such as those between finite model theory and verification, between finite model theory and linguistics, and between finite model theory and new database models (e.g. spatial and temporal databases). The goal of this one-day informal workshop is both to allow established researchers in the field of finite model theory to share contributions, and to introduce these new developments to a wide audience. * Invited speakers. Martin Grohe, Kerkko Luosto, Martin Otto. * Contributed talks. If you would like to give a contributed talk at the workshop, please send email to the organizers. * Organizers. Michael Benedikt (firstname.lastname@example.org), Leonid Libkin (email@example.com), Jouko Vaananen (firstname.lastname@example.org). INTERNATIONAL WORKSHOP ON IMPLICIT COMPUTATIONAL COMPLEXITY (ICC'99) Trento (Italy), June 30 and July 1, 1999 (Affiliated with LICS'99, within FLoC'99) http://icc99.cs.indiana.edu * Topics. Characterization, analysis, comparison, development, and implementation of computational complexity issues within descriptive complexity (finite model theory), proof theory (e.g. bounded arithmetic, other weak theories, weak higher order logics, linear logic), and applicative formalisms (e.g. function algebras, ramified recurrence, control mechanisms in lambda calculi). * Submission deadline. Tuesday, March 2, 1999. See the URL above for submission guidelines. * Program committee. Stephen Bellantoni, Samuel Buss, Robert Constable, Stephen Cook, Anuj Dawar (co-chair), Erich Graedel, Yuri Gurevich, Lauri Hella, Neil Jones, Clemens Lautemann, Daniel Leivant (co-chair), Helmut Schwichtenberg, Jurek Tyszkiewicz. 1999 WORKSHOP ON FORMAL METHODS AND SECURITY PROTOCOLS Trento, Italy, July 5, 1999 (part of FLoC'99) Call for papers http://www.cs.bell-labs.com/who/nch/fmsp99/ * Topics. Descriptive techniques (specification languages, models, logics) and analysis techniques (model checking, theorem proving, and their combination), as applied to protocols for authentication, fair exchange, electronic commerce, electronic auctions, etc. * Keynote speaker. Catherine Meadows. * Submission. An extended abstract (about 5-10 pages) explaining recent research results or work in progress should be mailed electronically to both organizers, email@example.com and Edmund.Clarke@cs.cmu.edu, to be received by March 26, 1999. Submissions should be formatted as a PostScript file in USLetter size. * Organizers. Nevin Heintze and Ed Clarke. KURT GOEDEL COLLOQUIUM Joint Conference of The 5th Barcelona Logic Meeting and The 6th Kurt Goedel Colloquium Barcelona, Spain, June 16-19, 1999 http://www.crm.es/info/cobalome.htm * The Joint Conference of the 5th Barcelona Logic Meeting and the 6th Kurt Goedel Colloquium, the biannual conference of the Kurt-Goedel-Society, is devoted to all areas of Mathematical Logic. * Invited speakers. Vicent Danos, Lou van den Dries, Mathew Foreman, Itsvan Juhasz, Byunghan Kim, Leonid Libkin, Angus Macintyre, Hiroakira Ono, Don Pigozzi, Jean Pierre Ressayre. * Submission of contributed papers. Those wishing to present short communications are invited to submit two copies of a one-page abstract before April 1st, 1999, to the following address: Centre de Recerca Matem`atica (CRM), Apartat 50, 08193 Bellaterra (Barcelona), Spain. Alternatively, a LaTeX file can be sent to one of the following e-mail addresses: firstname.lastname@example.org, email@example.com. All abstracts of invited and contributed papers will be published in Collegium Logicum - Annals of the Kurt-Goedel-Society, Vol 4. * Scientific Committee. Matthias Baaz, Enrique Casanovas, Rafael Farr'e, Ramon Jansana, Alexander Leitsch, Helmut Veith, Ventura Verd'u. * Further information. See the URL above. SECOND PANHELLENIC LOGIC SYMPOSIUM Delphi, Greece, July 13-17, 1999 Announcement and Call for Contributed Papers http://logic.math.ntua.gr/symposium * The scientific program of the symposium will consist of hour-long invited talks, tutorials, a panel discussion, and presentations of accepted papers. * Invited speakers. Z. Chatzidakis, A. Kakas, A. Kechris, L. Kirousis, G. Metakides, Y. Moschovakis, C. Papadimitriou, J. Sifakis. * Tutorials. Model Theory and Algebra by A. Macintyre, U. of Edinburgh, UK; Descriptive Set Theory and Large Cardinals by D.A. Martin, UCLA, USA; Logic and Computer-Aided Verification by M.Y. Vardi, Rice U., USA. * Call for contributed papers (see the web address for detailed information). Original papers that fall within the scope of the symposium are solicited. Authors are invited to submit an extended abstract not exceeding five pages to one of the two addresses below by March 31, 1999. Papers may be written in either English or Greek; they may be sent either as hard copy via postal mail or as a postscript file via email. All submitted papers will be reviewed by the scientific committee of the symposium, who will make final decisions on acceptance or rejection. Each accepted paper will be allocated a thirty-minute period for presentation and questions. * Addresses for submission of papers (submit to one of the two). Phokion G. Kolaitis George Koletsos Computer Science Department Department of Mathematics University of California, Santa Cruz National Technical University Santa Cruz, CA 95064 GR-15780 Zografou USA Athens, GREECE email: firstname.lastname@example.org email: email@example.com phone: +1-831-459-4768 phone: +30-1-772-1773 INTERNATIONAL SUMMER SCHOOL ON CONSTRAINTS IN COMPUTATIONAL LOGICS Gif-sur-Yvette, France, 5-9 September, 1999 More info at http://www.lri.fr/~ccl99 LOGIC FOR PROGRAMMING AND AUTOMATED REASONING (LPAR'99) Tbilisi, Republic of Georgia, September 6-10, 1999 Call for papers http://www.csd.uu.se/~voronkov/lpar99.html * Topics. Automated reasoning, logic in databases, logic and complexity, logic and concurrency, programming and logic, model checking, formal methods, programming languages and complexity, knowledge representation and reasoning, reasoning about actions, rewriting, logic programming, constraints, specification and verification using logics, modal logic and computing, temporal logic, description logics, constructive logic, higher-order logic, linear logic, new applications of logic, finite model theory. * Confirmed invited speaker. Yuri Gurevich (for the full list, check the conference web page later). * Submission. Submissions should be longer than 15 pages using the Springer llncs class files. Submit a uuencoded, compressed postscript file to firstname.lastname@example.org before April 20, 1999. The proceedings of LPAR'99 will be published by Springer-Verlag in the LNAI series. * Program co-chairs. Harald Ganzinger, David McAllester, Andrei Voronkov. * Programme Committee. Arnon Avron, Leo Bachmair, Franz Baader, Howard Barringer, Manfred Broy, Maurice Bruynooghe, Alan Bundy, Harald Ganzinger, Georg Gottlob, Ryuzo Hasegawa, Neil Jones, Jean-Pierre Jouannaud, Maurizio Lenzerini, Giorgio Levi, Leonid Libkin, Patrick Lincoln, Ursula Martin, Robert Nieuwenhuis, Catuscia Palamidessi, Frank Pfenning, Uday Reddy, Helmut Schwichtenberg, Moshe Vardi, Michael Zakharyashev. * Further information. See the URL above. FUNDAMENTALS OF COMPUTATION THEORY August 30 - September 3, 1999, Iasi, Romania Call For Papers http://www.info.uaic.ro/fct99 * Topics. Abstract data types, algorithms and data structures, automata and formal languages, categorical and topological approaches, circuits, computational biology, computational and structural complexity, computational geometry, computer systems theory, concurrency theory, constructive mathematics, cryptography, domain theory, distributed algorithms and computation, fault-tolerant computing, logic in computer science, learning theory, probabilistic computation, process algebras and calculi, rewriting, semantics, specification, transformation and verification, symbolic computation, type theory and type systems, universal algebra. * Invited Speakers. Matthew Hennessy, Marek Karpinski, Ugo Montanari, Arto Salomaa, Boris Trakhtenbrot. * Submission. Papers should not exceed 12 single-spaced pages (including the title page and bibliography) using (at least) 11-point font. Authors are encouraged to submit their extended abstracts electronically to email@example.com, before March 26, 1999. See the URL for the submission procedure. * Program Committee. S. Bozapalidis, C. Calude, V. Cazanescu, G. Ciobanu (co-chair), M. Dezani, J. Diaz, R. Freivals, Z. Fulop, J. Gruska, J. Karhumaki, J. Mitchell, F. Moller, R. De Nicola, M. Nielsen, G. Paun (co-chair) A. Rabinovich, M. Sato, M. Sudan, Wei-Ngan Chin, S. Yu. TUTORIAL AND WORKSHOP ON LOGIC AND COGNITIVE SCIENCE Linking Finite Model Theory,Descriptive Complexity, and the Study of Cognition Workshop: April 16-18, 1999 Tutorial: April 12-15, 1999 Philadelphia, PA Call for participation http://www.cis.upenn.edu/~ircs/workshops/lcs.html * See the above URL for further details. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE (MFCS '99) (see Newsletter 57) Dates and site change http://www.tcs.uni.wroc.pl/mfcs99/ * MFCS'99 will be held in Szklarska Poreba, Poland, September 6-10, 1999. The deadline for paper submission is March 11, 1999. DATABASE PROGRAMMING LANGUAGES (DBPL'99) Kinloch Rannoch, Scotland, September 1 - 3, 1999 Call for papers http://www.dcs.gla.ac.uk/dbpl99/ * Topics. Papers are sought on any topic related to the intersection between databases and programming languages, and in particular to the interaction between theory and practice in this area. Major topics in previous workshops include spatial databases, type systems, query languages, views, expressive power, aggregate queries, cooperative work, and transactions. * Submission. Submissios should take the form of extended abstracts, and should not exceed ten pages (given legible font and spacing.) Papers should be submitted electronically, in PDF or PostScript, to the following address: firstname.lastname@example.org. The deadline is April 1, 1999. * Program co-chairs. Richard Connor and Alberto Mendelzon. * Program committee. Luca Cardelli, Alan Dearle, Stephane Grumbach, Laks Lakshmanan, Leonid Libkin, Gianni Mecca, Fausto Rabitti, Peter Schwarz, Dan Suciu, David Toman. * Further information. See the URL above. INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP'99) November 29 - December 4, 1999, Las Cruces, New Mexico Call for papers http://www.cs.nmsu.edu/~complog/conferences/iclp99 * Topics. Papers are sought in all areas of logic programming including (but not restricted to): Theory, Semantics, Formalisms, Non-monotonic reasoning, Implementation, Compilation, Memory Management, Parallelism, Language Issues, Constraints, Concurrency, Objects, Functions, Environments, Program Analysis, Program Transformation, Debugging, Higher Order, Types, Modes, Programming Techniques, Artificial Intelligence, Applications, Deductive Databases, Software Engineering, and Natural Language * Submission. The primary means of submission will be electronic, in Postscript format. Details on the procedure and alternatives can be found at the ICLP'99 web site. Regardless of the submission method, a letter or e-mail message accompanying the paper must contain a plain text abstract of about 200 words and the names, e-mail addresses if possible, and postal addresses of all authors. The abstracts must be received by May 4, 1999. The full submissions must be received by May 10, 1999. Both are hard deadlines. * Invited Speakers. Ken Bowen, Vladimir Lifschitz, Fernando Pereira, Bernhard Thalheim. * Program committee. A. Bossi, M. Carlsson, P. Codognet, V. Dahl, A. Davison, M. Garcia de la Banda, B. Demoen, D. De Schreye (chair), J. Dix, B. Freitag, G. Gupta, M. Hanus, S. Hoelldobler, A. King, F. Sadri, G. Levi, D. Miller, L.M. Pereira, R. Ramakrishnan, P. Stuckey, M. Truszczynski, K. Ueda, P. Van Hentenryck, P. Van Roy, A. Voronkov. TYPED LAMBDA CALCULI AND APPLICATIONS (TLCA '99) April 7-9, 1999, L'Aquila, Italy Call for participation http://w3.dm.univaq.it/tlca99 * See the above URL for further details. THE THIRD INTERNATIONAL TBILISI SYMPOSIUM ON LANGUAGE, LOGIC AND COMPUTATION Batumi, Georgia, September 12-16, 1999 Call for papers http://www.illc.uva.nl/Batumi/ * Topics. The Symposium welcomes papers on current research in all aspects of Linguistics, Logic and Computation, including but not limited to: Natural language semantics/pragmatics; Algebraic and relational semantics; Natural language processing; Logic in AI and natural language; Natural language and logic programming; Automated reasoning; Natural language and databases; Information retrieval from text; Natural language and internet; Constructive logic and modal systems. * Submission. Abstracts of papers. not exceeding 2000 words, should be submitted to email@example.com before April 15, 1999. * Invited speakers. J. van Benthem, G. Gottlob, J. D. McCawley, J. M. Font, I. Hodkinson, I. Melchuk, A. Zaenen. * Program co-chairs. D. de Jongh, Th. Gamkrelidze, A. Voronkov. * Program committee. A. Anisimov, Ju. Apresjan, J. van Benthem, W. Blok, N. Chanishvili, R. Cooper, Ju. Ershov, J. Ginzburg, R. Goldblatt, E. Hajicova, L. Jablonskij, Z. Khasidashvili, V. Matrosov, H. Ono, B. Partee, G. Sambin, E. Vallduvi. THE 5TH INTERNATIONAL SPIN WORKSHOP ON THEORETICAL ASPECTS OF MODEL CHECKING July 5, 1999, Trento, Italy (part of FLoC'99) Call for papers http://www.ics.ele.tue.nl/~dennis/5thSPIN99/ * Topics. Theory (automata, algorithms, reduction methods, logic, real-time, abstraction, modularity, hierarchy, refinement, implementation, fairness, symmetry relation, storage methods, caching methods); Short tutorials or surveys on a topical subject related to SPIN model checking; Analyses of shortcomings, possible extensions, benefits of existing tools; Empirical studies, measurements, tool comparisons. * Keynote Speaker. John Rushby. * Submission. Papers, no longer than 20 pages, can be submitted by email in Postscript format to D.R.Dams@ele.tue.nl before April 1, 1999. * Program Committee. Dennis Dams, Mieke Massink, Gerard Holzmann, Ed Brinksma, Marco Daniele, Bengt Jonsson. FLoC'99 WORKSHOP ON SYMBOLIC MODEL CHECKING (SMC'99) July 6, 1999, Trento, Italy Call for papers http://afrodite.itc.it:1024/~cimatti/smc99/ * The aim of the workshop is to bring together active developers and users of symbolic model checkers, compare state of the art model checking techniques (e.g. compositional reasoning, abstraction, partitioning), discuss experimental results and experience reports, and promising directions for future research. * Submission. A submission should include an extended abstract not exceeding ten pages. All submissions should be sent to the organizers in postscript format by March 26, 1999. * Keynote speakers. Ken McMillan, Fabio Somenzi. * Organizers. Alessandro Cimatti (firstname.lastname@example.org), Orna Grumberg (email@example.com). * Program committee. Adnan Aziz, Sergio Campos, Alessandro Cimatti, Edmund Clarke, Danny Geist, Fausto Giunchiglia, Orna Grumberg, Markus Kaltenbach, Carl Pixley. ON-LINE REPOSITORY OF FORMAL METHODS EDUCATIONAL MATERIALS http://www.cs.indiana.edu/formal-methods-education/ TYPES SUMMER SCHOOL: THEORY AND PRACTICE OF FORMAL PROOFS August 30 - September 10, 1999, French Riviera, France organized by the Esprit Working Group: Types for proofs and programs. http://www-sop.inria.fr/types-sum-school.html * Organizers. J. Despeyroux, G. Dowek, M. Hofmann, B. Nordstrom. * Scope. This two weeks' course is for postgraduate students, researchers and industrials who want to learn about interactive proof development. There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics which give relevant theoretical background. Several talks will be devoted to the presentation of applications. The proof assistants presented in the school represent the current state-of-the-art in interactive theorem proving. Participants will get extensive opportunities to use the systems in a workstation environment for developing their own proofs. * Speakers. H. Barendregt, B. Nordstrom, Th. Coquand, P. Martin-Löf, JL. Krivine, Y. Lafont, T. Nipkow, S. Berardi. * Application. The deadline for application is May 17, 1999. RESEARCH FELLOW IN LOGIC AND AUTOMATED REASONING Mechanising First-Order Temporal Logic" Project Department of Computing and Mathematics Manchester Metropolitan University, Manchester, UK http://www.doc.mmu.ac.uk/RESEARCH/LoCo/mfotl-rf-advert99.html * See the URL above for further details. BOOK ANNOUNCEMENT Mystic, Geometer, and Intuitionist: The Life of L.E.J. Brouwer Volume 1: The Dawning Revolution by Dirk van Dalen Oxford University Press, 1999, ISBN 0-19-850297-4 * Luitzen Egbertus Jan Brouwer is one of the most remarkable scientists of the twentieth century. With strong mystical leanings, he single-handedly started to revise mathematics. On the basis of an all-embracing philosophy, he advocated a mathematics and science which is a mental constructive activity. He became famous for his topology (e.g. the fixed point theorem) and intuitionism. Among his many other activities there is his membership of the socio-linguistic Signific Circle. His intuitionistic work was largely ignored until a revival in the sixties, mainly through the work of Kleene and Kreisel. His keen sense for justice made him a party in many conflicts, scientific and political. E.g. he worked to undo the boycott of German scientists. His discussion with David Hilbert (the Grundlagenstreit) made him a legend during his lifetime. Although Brouwer got offers from Berlin and Gottingen, he preferred to stay in Amsterdam, so that he could live in the artist community at Laren, where he led a life of quiet unconventionality. Volume 1 deals with the mystical, topological and intuitionistic work of Brouwer. The topics "Grundlagenstreit" and "dimension theory" will be treated in the second volume. SCHOOL IN LOGIC AND COMPUTATION Heriot-Watt University, Edinburgh, 10-13 April 1999 Call for abstracts and Participation http://www.cee.hw.ac.uk/~fairouz/eefschool.html * Lecturers. Samson Abramsky, Henk Barendregt, Robert Constable, Dirk van Dalen, Mariangola Dezani-Ciancaglini, Assaf Kfoury, Claude Kirchner, Jan-Willem Klop, Andrew Pitts, Pawel Urzyczyn. * Workshops. 1.Types in computation. Speaker: Herman Geuvers. 2.Proof search in computation. Speaker: Roy Dyckhoff. 3.Rewriting in computation. Speaker: Roberto Di Cosmo. * Submission. Workshops are soliciting talks on work in progress and open problems from both young and established researchers. To submit a talk, send a two page abstract in postscipt to firstname.lastname@example.org no later than Friday 5 March. * Grants. Grants cover registration and accommodation, leaving only travel and some local expenses to be paid. Grants are restricted to PhD students aged 35 or younger with nationality in the European Union or Norway, Israel, Iceland or Liechtenstein. See the web page for the application procedure. * Registration and further information. See the URL above or send mail to Fairouz Kamareddine (email@example.com).