CATEGORY THEORY AND COMPUTER SCIENCE (CTCS-6)
7th-11th August 1995, University of Cambridge, UK
In conjunction with the third Cambridge Summer Meeting in Category Theory.
* Topics. The purpose of the conference series is the advancement of the
foundations of computing using the tools of category theory, algebra,
geometry and logic. Whilst the emphasis is upon applications of
category theory, it is recognised that the area is highly
interdisciplinary and the organising committee welcomes submissions in
related areas. Topics central to the conference include: Models of
computation, Program logics and specification, Type theory and its
semantics, Domain theory, Linear logic and its applications, Categorical
programming. Submissions purely on category theory are also acceptable
as long as the applicability to computing is evident.
* Submissions. Send 5 hard copies of a draft paper (maximum of 20 pages)
by February 1, 1995 to Dr. David Pitt, Department of Mathematical and
Computing Sciences, University of Surrey, Guildford, Surrey, GU2 5XH,
United Kingdom.
* Organising and Programme Committee. S. Abramsky, P.-L. Curien,
P. Dybjer, P. Johnstone, G. Longo, G. Mints, J. Mitchell, E. Moggi,
D. Pitt, A. Pitts, A. Poigne, D. Rydeheard, F-J. de Vries, E. Wagner.
7TH CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV'95)
July 3 - July 6, 1995, Liege, BELGIUM,
* CFP via FTP. LaTeX & Postscript(tm) versions of the Call for Papers
available by anonymous FTP from ftp.montefiore.ulg.ac.be
(139.165.16.58) in directory pub/cav95.
* Topics. This conference is the seventh in a series dedicated to
advancing theory and practice of computer-assisted formal
verification. It is centered on the theme that computer assistance is
essential for wider use of verification techniques, but encourages all
styles of verification approaches and a variety of applica- tion
areas. It covers the spectrum from theory to concrete applications,
with emphasis on verification tools and algorithms and techniques
needed for their implementation. The conference will include
contributed papers, invited papers, tutorials, and tool
demonstrations. The conference boundaries are not rigid. In the past,
papers on the following topics have been enthusiastically received.
o Application areas: synchronous & asynchronous circuits, computer arithmetic,
protocols, distributed algorithms, real-time systems, hybrid systems.
o Tools and Methods based on: state-space exploration, model-checking,
automated deduction, and theorem proving.
o Theoretical issues: decidability of verification problems for a variety of
formalisms, computational complexity results, verification algorithms.
Any paper of potential interest for computer-aided verification is considered.
* Submission. Authors may submit a paper by mailing ELECTRONICALLY a
self-contained Postscript(tm) version to the address
cav95-submit@montefiore.ulg.ac.be (strongly encouraged) AND by sending
5 copies of it to the Program Chairman. UNPRINTABLE ELECTRONIC
submissions for which paper copies are not received will not be
considered. Length is limited to 12 typed pages (with normal font
sizes, line spacing, margins, etc.) Each submission should provide
sufficient detail for the program committee to assess the merit of the
contribution. Simultaneous submission to other conferences with
proceedings, or submission of already published material is not
allowed. Submission deadline: Jan. 20, 1995; notification: Mar. 19, 1995.
Accepted papers will be published in the conference proceedings
(Springer-Verlag Lecture Notes in Computer Science series).
* Program chairman: Pierre Wolper, Universite de Liege, Institut Montefiore,
B28, Grande Traverse 10, B-4000 Liege, BELGIUM. cav95@montefiore.ulg.ac.be
* Program committee: R. Alur, R. Brayton, C. Courcoubetis, W. Damm,
R. De Simone, R. Devillers, E. Allen Emerson, S. Garland, O. Grumberg,
N. Halbwachs, T. Henzinger, R. Koymans, G. Leduc, K. McMillan, J. Parrow,
N. Shankar, F. Somenzi, B. Steffen, P. Varaiya, M. Vardi, T. Yoneda.
* Steering committee: E. Clarke, R. Kurshan, A. Pnueli, J. Sifakis.
5TH INTERNATIONAL CONFERENCE ON DATABASE THEORY (ICDT)
January 10-13, 1995, Prague, Czech Republic
An international conference on theoretical aspects of databases.
* Program Highlights. Invited talks: Data on Air: An Introduction to
Wireless and Mobile Computing, Tomasz Imielinski, Rutgers University,
USA; Spatial Databases, the Final Frontier, Jan Paredaens, University of
Antwerp, Belgium. Tutorials: Parallel Database Systems, Gerhard Weikum,
University of the Saarland, Saarbruecken, Germany; Languages for
Polynomial-time Queries -- an Ongoing Quest, Phokion Kolaitis.
* Further Information. Dr. Marcela Bezouskova, Dept. of Control
Engineering, Faculty of Electrical Engineering, Czech Technical
University, Karlovo nam. 13, CZ - 12135 PRAGUE 2. Phone: +42 2 295664
or +42 2 24357488. Fax: +42 2 290159. E-mail: k335@lab.felk.cvut.cz.
MASTER OF LOGIC PROGRAM
Institute for Logic, Language and Computation (ILLC)
University of Amsterdam
* Specialisation Areas and Courses. Logic and Mathematics: recursion
theory; constructivism and proof theory; modal logic and formal
arithmetic; lambda calculus; reasoning with probability and
uncertainty; extensional and intensional logics. Logic, Philosophy
and Linguistics: logical semantics; Montague grammar; non-standard
notions of inference; meaning and context; natural language
question-answering systems; seminar in logical semantics. Logic and
Computer Science: computational learning theory; structured complexity
theory; theorem proving; semantics of programming languages; theory
and practice of logic programming; language processing. All courses
are taught in English.
* ILLC Permanent Staff. Krzysztof Apt; Johan van Benthem; Jan Bergstra;
Jacob Brunekreef; Kees Doets; Peter van Emde Boas; Theo Janssen; Dick
de Jongh; Paul Klint; Michiel van Lambalgen; Piet Rodenburg; Leen
Torenvliet; Anne Troelstra; Paul Vitanyi; Renate Bartsch; Jeroen
Groenendijk; Martin Stokhof; Frank Veltman; Remco Scha; Henk Zeevat;
* Brochure. Send your postal address by regular mail, e-mail of fax,
and state `brochure Master of Logic'. ILLC, Plantage Muidergracht 24,
1018 TV Amsterdam, The Netherlands. E-mail: illc@fwi.uva.nl. Fax:
+31 20 525 5206.
WORKSHOP ON LOGIC, DOMAINS, AND PROGRAMMING LANGUAGES
(Preliminary Announcement)
May 24-27, 1995, Darmstadt, Germany
The Workshop on Logic, Domains, and Programming Languages is aimed at
computer scientists and mathematicians alike, who share an active
interest in the mathematical foundations of computer science.
* Topics. The scope of the workshop encompasses all aspects of
Programming Language Semantics ranging from purely theoretical topics
to concrete applications and implementations of semantic
methods. Possible workshop topics are, for example, Lambda Calculi and
Functional Programming, Domain Theory, Denotational and Algebraic
Semantics, Type Theories, Linear Logic, Process Algebras, and
Concurrency.
* Invited Speakers. Samson Abramsky, Imperial College, London, United
Kingdom. Olivier Danvy, Aarhus University, Denmark. Peter O'Hearn,
Syracuse University, Syracruse, N.Y., USA. Frank Pfenning, Carnegie
Mellon University, Pittsburgh, USA. Gordon D. Plotkin, University of
Edinburgh, United Kingdom. Helmut Schwichtenberg, Universit"at
M"unchen, Germany. Dana S. Scott, Carnegie Mellon University,
Pittsburgh, USA. Bent Thomsen, European Computer-Industry Research
Center, M"unchen, Germany.
* Submissions. Send a title and an abstract of your intended
presentation to ldpl95@mathematik.th-darmstadt.de by JANUARY 15, 1995.
Talk slots will be filled on a ``first come, first served'' basis.
Pre-registration is invited.
* Award. The University of Darmstadt will award Dana Scott an honorary
degree on Wednesday, May 24.
* Organizers: K.H. Hofmann, M. Huth, A. Jung, and K. Keimel.
* Further Information. Dr. Michael Huth, Workshop on Logic, Domains,
and Programming Languages, AG 1, Fachbereich Mathematik, Technische
Hochschule Darmstadt, 64289 Darmstadt, Germany. Email:
ldpl95@mathematik.th-darmstadt.de.
ERLANGEN/LEIPZIG WORKSHOP ON FINITE AND NONMONOTONIC MODEL THEORY
Universit\"at Erlangen-N\"urnberg, March 26--30, 1995.
* Topics. Model theoretical aspects of finite structures; the
relationship to computational complexity; model theory of nonmonotonic
inference operations.
* Submissions. Participants who wish to give a 30 minute contributed
talk should submit an extended abstract of at most five pages not
later than January 15, 1994 to the address below (e-mail submissions
of TeX or LaTeX files are welcome). It is planned to publish the
Proceedings of the workshop.
* Invited Speakers. J\"org Flum (Freiburg), Michal Krynicki (Warsaw),
Kerkko Luosto (Helsinki), Marcin Mostowski (Warsaw), Yachin Pnueli
(Berlin).
* Program Committee. J. W. Degen, K. Leeb (Erlangen), J. Makowsky
(Haifa), J. V\"a\"an\"anen (Helsinki).
* Organizing Committee. J. W. Degen, J. Johannsen, U. Weigand
(Erlangen), H. Herre (Leipzig).
* Correspondence. J. W. Degen, Lehrstuhl f\"ur Informatik I,
Universit\"at Erlangen, Martensstrasse 3, D-91058 Erlangen, Germany.
E-mail: lcu@informatik.uni-erlangen.de.
KGS-AILA JOINT MEETING ON MODEL THEORY
August 21-24, 1995, Florence, Italy
Held by the Kurt Goedel Society and the Italian Association of Logic
and its Applications. The meeting coincides with the Goedel Society's
4th Kurt Goedel Colloquium and will be affiliated to the International
LMPS-IUHPS Symposium on Logic, Methodology and Philosophy of Science,
held August 19-25 in Florence.
* Program Committee. Maurice Boffa (Co-chair), Mons, Belgium; Gregory
Cherlin, Rutgers, U.S.A.; Ulrich Felgner, Tuebingen, Germany; Wilfrid
Hodges, London, U.K.; Annalisa Marcja (Co-chair), Florence, Italy;
Daniele Mundici (Chair), Milan, Italy; Gabriel Sabbagh, Paris, France.
* Invited Speakers. Zoe Chatzidakis, David Evans, Ehud Hrushovski,
Angus MacIntyre, Dave Marker, Francis Oger, Mike Prest, Anand Pillay,
Zachary Robinson, Philipp Rothmaler, Carlo Toffalori.
* Submissions. Three copies of a full paper, preferably in LaTeX
format, before February 1, 1995, to the program committee chairman,
Daniele Mundici, at the address below. All papers should be original,
and in their final form. The Proceedings will be published in a
special issue of the Annals of Pure and Applied Logic. All papers
shall be refereed.
* Program Chair. Daniele Mundici, Department of Computer Science,
University of Milan, via Comelico 39-41, I-20135 Milan, Italy. Phone:
+39 (0)2 55006247. Fax: +39 (0)2 55006253. E-mail:
mundici@imiucca.csi.unimi.it.
* LMPS-IUHPS Information. LMPS, Centro Servizi di Segreteria, via
A. Lapini, 1, I-50136 Florence, Italy. Phone: +39 (0)55 670369. Fax:
+39 (0)55 660236.
DIMACS CENTER FOR DISCRETE MATHEMATICS AND THEORETICAL COMPUTER SCIENCE
1995-6 SPECIAL YEAR ON LOGIC AND ALGORITHMS
[Unabridged announcement. Last item in newsletter.]
DIMACS is a Science and Technology Center funded by the NSF, whose
participating institutions are Rutgers University, Princeton
University, AT&T Bell Laboratories, and Bellcore. Research and
education activities at DIMACS focus on such areas as analysis of
algorithms, combinatorics, complexity, computational algebra, discrete
and computational geometry, discrete optimization and graph theory. A
primary activity of the Center is to sponsor year-long research
programs on specific topics of current interest, and one such program
is this Special Year on Logic and Algorithms.
A dichotomy in theoretical computer science is best demonstrated by
looking at the 1994 Handbook of Theoretical Computer Science. Volume
A discusses algorithms and complexity, while Volume B treats formal
models and semantics. Theoretical computer science in the United
States is largely "Vol. A"-ish, while European theoretical computer
science is largely "Vol. B"-ish. The goal of this Special Year is to
bridge the gap between the two branches, focusing on three bridge
areas: Computer-Aided Verification, Finite-Model Theory, and Proof
Complexity. All three are emerging research areas that fit naturally
between Vol. A and Vol. B.
Below is a brief description of each topic, and a tentative list of
workshops associated with that topic. We also plan a series of
week-long tutorials, one in each topic, intended to introduce
students, recent graduates, and professionals from other areas to the
topic.
We invite applications for visiting and postdoctoral positions at
DIMACS in connection with the Special Year. We encourage people to
apply to NSF or other granting agencies for support to be used at
DIMACS, as well as applying to DIMACS itself. Many funding deadlines
fall between mid-October and mid-November, which calls for speedy
action by those who are interested in visiting DIMACS. For more
information on these positions, likely granting agencies, or anything
else, contact DIMACS as described at the end of this announcement.
Computer-Aided Verification
Computer-Aided Verification studies algorithms and structures for
verifying properties of programs. It draws upon techniques from graph
theory, combinatorics, automata theory, complexity theory, Boolean
functions and algebras, logic, Ramsey theory and linear programming.
Since the DIMACS CAV workshop in 1990, worldwide interest in CAV has
grown enormously, not only in academia but in companies like Intel,
DEC, Sun and AT&T. This creates an unusual and rewarding opportunity
to see theory put directly into practice.
We plan workshops in "Timing verification and hybrid systems" and
in "Computational and complexity issues in automated verification".
Finite-Model Theory
Model theory is the study of mathematical structures which satisfy
sets of axioms. Recent work on the FINITE models of a set of axioms
has yielded elegant connections with theoretical computer science,
including model-theoretic characterizations of complexity classes.
Further, when a class of finite mathematical structures (e.g. graphs)
is equipped with probability measures, one can often develop powerful
meta-theorems called zero-one laws, which give conditions under which
probabilities must approach zero or one as the structure size goes to
infinity.
We plan workshops in "Finite models and descriptive complexity" and
in "Logic and random structures".
Proof Complexity
Two related notions of "proof complexity" currently motivate
research at the interface between computer science and logic. One
notion centers on the length of a proof, and the other on the
complexity of the inference steps within the proof.
It is well known that NP=co-NP iff all propositional tautologies
have short proofs. But the connection between proof length and
complexity theory goes much deeper. Lower bounds on circuits are
closely tied to those on proof length in restricted systems, and
advances on one front often lead quickly to progress on the other.
By restricting the complexity of inference steps within a proof,
one obtains a fragment of Peano Arithmetic called Bounded Arithmetic,
which defines exactly the predicates in the polynomial hierarchy.
Exciting recent work has shown that if certain theories of bounded
arithmetic can prove lower bounds in complexity theory, then
corresponding cryptographic systems cannot be secure.
We plan a single, four-day workshop on "Feasible arithmetic and
lengths of proofs".
Other Interactions
As usual, this DIMACS Special Year aims to be inclusive, not
exclusive. Many other areas, beyond the organizers' ken, would mesh
with these themes. This fourth, "catch-all" topic is intended to
encourage all scientists who might benefit from interaction with
logicians, combinatorialists and computer scientists, and with the
topics we HAVE listed.
Federated Logic Conference
As part of this Special year, DIMACS will host a Federated Logic
Conference (FLC). FLC will be modeled after the successful Federated
Computer Research Conference (FCRC). The goal is to battle
fragmentation of the technical community by bringing together
synergetic conferences that apply logic to computer science. The
following conferences will participate in FLC: CADE (Conference on
Automated Deduction), CAV (Conference on Computer-Aided Verification),
LICS (IEEE Symp. on Logic in Computer Science), and RTA (Conference on
Rewriting Techniques and Applications). The four conferences will span
eight days, with only two-way parallelism at any given time. We will
make special efforts to bring about interaction between the various
conferences. The meeting will take place in late June, 1996, on one
of the Rutgers campuses.
For Further Information
You can use several methods to contact the DIMACS center.
By email: center@dimacs.rutgers.edu
(For information on visiting, fellows@dimacs.rutgers.edu)
By telephone: 908-445-5928
By FAX: 908-445-5932
By mosaic/www/lynx: http://dimacs.rutgers.edu/
By gopher: gopher dimacs.rutgers.edu
By TELNET: telnet dimacs.rutgers.edu and login as "info"
By post: DIMACS Center
Rutgers University
P.O. Box 1179
Piscataway, NJ 08855-1179
You can also contact the following people:
DIMACS Associate Director for Research:
Steve Mahaney
DIMACS Center Administrator:
Maryann Holtsclaw
Special Year Organizing Committee:
Eric Allender, Rutgers U.
Bob Kurshan, AT&T Bell Labs
Moshe Vardi, Rice U.
Special Year Publicity Chair:
Stephen Bloch, Adelphi U.
Special Year Steering Committee:
Paul Beame, U. Washington
Sam Buss, U. California, San Diego
Gregory Cherlin, Rutgers U.
Ed Clarke, Carnegie Mellon U.
Steve Cook, U. Toronto
Allen Emerson, U. Texas
Joan Feigenbaum, AT&T Bell Labs
Orna Grumberg, Technion
Phokion Kolaitis, U. California, Santa Cruz
Daniel Leivant, Indiana U.
Richard Lipton, Princeton U.
Amir Pnueli, Weizmann Institute
Peter Winkler, AT&T Bell Labs