- Albert Atserias
(Barcelona)
- Notions of Average-Case Complexity
for Random 3-SAT
- By viewing random 3-SAT as a distributional
problem, we go over some of the notions of average-case
complexity that were considered in the literature. We
note that for dense formulas the problem is polynomial-time
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 meta-logic 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 meta-logic. Since we
restrict to the finite case, the ability of the meta-logic 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 no-side 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 one-step 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 Context-Free Dynamic Logic;
- The question of polymorphic collapse;
- Higher-order push-down 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 on-line
version of the conference
proceedings is available at Springer www site.
Last modified:
Sep 14, 2004, 13:16