 Albert Atserias
(Barcelona)
 Notions of AverageCase Complexity
for Random 3SAT
 By viewing random 3SAT as a distributional
problem, we go over some of the notions of averagecase
complexity that were considered in the literature. We
note that for dense formulas the problem is polynomialtime
on average in the sense of Levin. For sparse formulas
the question remains widely open despite several recent
attempts.
 Martin Hyland
(Cambridge)
 Abstract Interpretation of
Proofs: Classical Propositional Logic

Representative abstract interpretations of the proof theory of the
classical propositional calculus are described. These provide
invariants for proofs in the sequent calculus. The results of
calculations in simple cases are given and briefly discussed.
 Ken McMillan
(Berkeley)
 Applications of Craig
Interpolation to Model Checking
 Dale
Miller (INRIA)
 Bindings, mobility of bindings, and the
∇quantifier
 We present a metalogic that contains a new quantifier
∇ (for encoding “generic judgments”) and inference rules
for reasoning within fixed points of a given specification. We
then specify the operational semantics and bisimulation relations
for the finite πcalculus within this metalogic. Since we
restrict to the finite case, the ability of the metalogic to
reason within fixed points becomes a powerful and complete tool
since simple proof search can compute the unique fixed point. The
∇ quantifier helps with the delicate issues surrounding the
scope of variables within πcalculus expressions and their
executions (proofs). We shall illustrate several merits of the
logical specifications we write: they are natural and declarative;
they contain noside conditions concerning names of bindings while
maintaining a completely formal treatment of such bindings;
differences between late and open bisimulation relations are easy
to see declaratively; and proof search involving the application
of inference rules, unification, and backtracking can provide
complete proof systems for both onestep transitions and for
bisimulation. This work is joint with Alwen Tiu.
 Pawel Urzyczyn
(Warsaw)
 My (Un)Favourite Things
 The talk will be devoted to four open problems
I was unsuccessfully
trying to solve in the past. These problems concern:
 Regular and ContextFree Dynamic Logic;
 The question of polymorphic collapse;
 Higherorder pushdown stores and procedures;
 Polymorphic definability of recursive data types.
Each of these problems addresses a basic issue in the logical
foundations of computer science, and each has been open for a long
time. This talk aims at bringing back the challenge, and sorting out
the related confusions.
A BibTeX database is available as a separate
file.
An online
version of the conference
proceedings is available at Springer www site.
Last modified:
Sep 14, 2004, 13:16