Newsletter 58
February 9, 1999
[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 (benedikt@bell-labs.com), Leonid Libkin
(libkin@bell-labs.com), Jouko Vaananen (jvaanane@cc.helsinki.fi).
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, nch@research.bell-labs.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: kgc99@dbai.tuwien.ac.at, crm@crm.es.
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: kolaitis@cse.ucsc.edu email: koletsos@math.ntua.gr
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 lpar99@csd.uu.se 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 fct99@info.uaic.ro, 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: dbpl99@dcs.gla.ac.uk. 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 dekker@philo.uva.nl 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 (cimatti@irst.itc.it),
Orna Grumberg (orna@cs.technion.ac.il).
* 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
fairouz@cee.hw.ac.uk 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 (fairouz@cee.hw.ac.uk).