DIMACS 1995-96 Special Year on Logic and Algorithms
Call for Visitor & Postdoctoral Fellowship Applications
The DIMACS Center for Discrete Mathematics and Theoretical Computer
Science announces its 1995-96 Special Year on Logic and Algorithms.
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.
DIMACS will announce other postdoc and visitor application deadlines
in November, 1994.
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, SGI,
Motorola, 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: 732-445-5932
- By post:
- DIMACS Center
- Rutgers University
- 96 Frelinghuysen Road
- Piscataway, NJ 08854-8018
You can also contact the following people:
For prompt discussion of applying for visiting faculty fellowships,
postdoctoral fellowships, etc.:
- Eric Allender, allender@cs.rutgers.edu
- Moshe Vardi, vardi@cs.rice.edu
Special Year Organizing Committee:
- Eric Allender, Rutgers U. allender@cs.rutgers.edu
- Bob Kurshan, AT&T Bell Labs k@research.att.com
- Moshe Vardi, Rice U. vardi@cs.rice.edu
Special Year Publicity Chair:
- Stephen Bloch, Adelphi U. sbloch@boethius.adelphi.edu
Special Year Steering Committee:
- Paul Beame, U. Washington beame@cs.washington.edu
- Sam Buss, U. California, San Diego sbuss@gentzen.ucsd.edu
- Gregory Cherlin, Rutgers U.
- Ed Clarke, Carnegie Mellon U. Edmund_Clarke@cs.cmu.edu
- Steve Cook, U. Toronto sacook@theory.toronto.edu
- Allen Emerson, U. Texas emerson@cs.utexas.edu
- Joan Feigenbaum, AT&T Bell Labs jf@research.att.com
- Orna Grumberg, Technion orna@cs.technion.ac.il
- Phokion Kolaitis, U. California, Santa Cruz kolaitis@cs.ucsc.edu
- Daniel Leivant, Indiana U. leivant@cs.indiana.edu
- Richard Lipton, Princeton U. rjl@cs.princeton.edu
- Amir Pnueli, Weizmann Institute amir@wisdom.weizmann.ac.il
- Peter Winkler, AT&T Bell Labs pw@research.att.com
Index of Special Year on Logic and Algorithms
DIMACS Homepage
Contacting the Center
Document last modified on October 19, 1998.