 | |
All
sessions take place in auditorium 1.Chair:
Samson Abramsky | 09:00- | 09:30
| C.-H. L. Ong, Oxford U, UK
Observational
equivalence of 3rd-order idealized Algol is
decidable
We
prove that observational equivalence of 3rd-order finitary
Idealized Algol (IA) is decidable using Game Semantics. By modelling state
explicitly in our games, we show that the denotation of a term M of
this fragment of IA (built up from finite base
types) is a compactly innocent strategy-with-state i.e. the strategy is
generated by a finite view function fM. Given any
such fM, we construct a real-time deterministic
pushdown automata (DPDA) that recognizes the complete plays of the
knowing-strategy denotation of M. Since such
plays characterize observational equivalence, and there is an algorithm for
deciding whether any two DPDAs recognize the same language, we obtain a
procedure for deciding observational equivalence of 3rd-order finitary IA.
This algorithmic representation of program meanings, which is
compositional, provides a foundation for model-checking a wide range of
behavioural properties of IA and other cognate programming languages.
Another result concerns 2nd-order IA with full recursion: we show that
observational equivalence for this fragment is undecidable. |
| 09:30- | 10:00
| Martin Hyland, U Cambridge, UK
Andrea
Schalk, U Cambridge, UK
Games
on graphs and sequantially realizable functionals
We
present a new category of games on graphs and derive from it a
model for Intuitionistic Linear Logic. Our category has the computational
flavour of concrete data structures but embeds fully and faithfully in an
abstract games model. It differs markedly from the usual Intuitionistic
Linear Logic setting for sequential algorithms. However, we show that with
a natural exponential we obtain a model for PCF essentially equivalent to
the sequential algorithms model. We briefly consider a more extensional
setting and the prospects for a better understanding of the Longley
Conjecture. |
| 10:00- | 10:30
| Olivier Laurent, U Paris VII, France
Polarized
games
We
generalize the intuitionistic Hyland-Ong games to a notion of
polarized games allowing games with plays starting by proponent moves. The
usual constructions on games are adjusted to fit this setting yielding a
game model for polarized linear logic with a definability result. As a
consequence this gives a complete game model for various classical systems:
LC, lambda-mu calculus, ... for both call-by-name and call-by-value
evaluations. |
Chair:
Andre Scedrov | 11:00- | 11:30
| Abbas Edalat, Imperial College, UK
Andre
Lieutier, Dassault Systemes Provence and LMC/IMAG, France
Domain
theory and differential calculus (functions of one
variable)
We
introduce a data type for differentiable functions in the
framework of domain theory. Using a new structure, called tie of maps,
which provide finitary information about the differential properties of a
Scott continuous map, we define the derivative of a Scott continuous
function on the domain of intervals, which is itself a Scott continuous
function. This leads to a domain-theoretic generalization of the
fundamental theorem of calculus. The central part of this work is to
construct a domain for differentiable real valued functions of a real
variable. The classical C¹ functions,
equipped with its C¹ norm, is embedded into
the set of maximal elements of this domain, which is a countably based
bounded complete continuous domain with an effective structure. The
construction can be generalized to Ck and C∞ functions and, in future, to functions of
several variables and analytic functions. While the question of
computability for differentiable functions have been studied in the
literature, this seems to be the first time that a proper data type for
differential calculus is proposed which brings smooth mathematics in the
realm of domain theory and type theory. As an immediate application, we
present a domain-theoretic and effective generalization of Picard's
theorem, which provides a data type and an algorithm for solving
differential equations given by a vector field and an initial condition. At
each step of computation of this algorithm, one gets an approximation which
is an interval piecewise polynomial function with rational coefficients
that provides precise information on the solution. |
| 11:30- | 12:00
| Alex Simpson, U Edinburgh, UK
Computational
adequacy for recursive types in models of
intuitionistic set theory
We
present a general axiomatic construction of models of FPC, a
recursively typed lambda-calculus with call-by-value operational semantics.
Our method of construction is to obtain such models as full subcategories
of categorical models of intuitionistic set theory. This allows us to
obtain a notion of model that encompasses both domain-theoretic and
realizability models. We show that the existence of solutions to recursive
domain equations, needed for the interpretation of recursive types, depends
on the strength of the set theory. The internal set theory of an elementary
topos is not strong enough to guarantee their existence. However, solutions
to recursive domain equations do exist if models of intuitionistic
Zermelo-Fraenkel set theory are used instead. We apply this result to
interpret FPC, and we provide necessary and sufficient conditions on a
model for the interpretation to be computationally adequate, i.e. for the
operational and denotational notions of termination to agree. |
| 12:00- | 12:30
| Daniele Varacca, U Aarhus, Denmark
The
powerdomain of indexed valuations
This
paper is about combining nondeterminism and probabilities.
We study this phenomenon from a domain theoretic point of view. In domain
theory, nondeterminism is modeled using the notion of powerdomain, while
probability is modeled using the powerdomain of valuations. Those two
functors do not combine well, as they are. We define the notion of
powerdomain of indexed valuations, which can be combined nicely with the
usual nondeterministic powerdomain. We show an equational characterization
of our construction. Finally we discuss the computational meaning of
indexed valuations, and we show how they can be used, by giving a
denotational semantics of a simple imperative language. |
Chair:
Daniel Leivant | 14:00- | 15:00
| Stephen
A. Cook, U Toronto, Canada
Invited
lecture: Complexity Classes, Propositional Proof Systems, and Formal
Theories |
| 15:00- | 15:30
| William Hesse, U Massachusetts, USA
Neil
Immerman, U Massachusetts, USA
Complete
problems for dynamic complexity classes
We
present the first complete problems for dynamic complexity
classes including the classes Dyn-FO and DynThC°,
the dynamic classes corresponding to relational calculus and (polynomially
bounded) SQL, respectively. The first problem we show complete for Dyn-FO
is a single-step version of the circuit value problem (SSCV).
Of
independent interest, our construction also produces a first-order formula,
ζ, that is in a sense universal for
all first-order formulas. Since first-order formulas are stratified by
quantifier depth, the first-order formula ζ emulates formulas of
greater depth by iterated
application. As a corollary we obtain a fixed quantifier block, QBC, that
is complete for all first-order quantifier blocks. |
Chair:
Phokion Kolaitis | 16:00- | 16:30
| Albert Atserias, Techn. U of Catalonia, Spain
Unsatisfiable
random formulas are hard to certify
We
prove that every property of 3CNF formulas that implies
unsatisfiability and is expressible in Datalog has asymptotic probability
zero when formulas are randomly generated by taking 6n non-trivial
clauses of exactly three literals uniformly
and independently. Our result is a consequence of designing a winning
strategy for Duplicator in the existential k-pebble game on the
structure that encodes the 3CNF formula
and a fixed template structure encoding a satisfiable formula. The winning
strategy makes use of certain extension axioms that we introduce and hold
almost surely on a random 3CNF formula. An interesting feature of our
result is that it brings the fields of Propositional Proof Complexity and
Finite Model Theory together. To make this connection more explicit, we
show that Duplicator wins the existential pebble game on the structure
encoding the Pigeonhole Principle and the template structure above.
Moreover, we also prove that there exists a 2k-Datalog program
expressing that an input 3CNF formula has
a Resolution refutation of width k. As a
consequence to our result and the known size-width relationship in
Resolution, we obtain new proofs of the exponential lower bounds for
Resolution refutations of random 3CNF formulas and the Pigeonhole
Principle. |
| 16:30- | 17:00
| Michael Soltys, McMaster U, Canada
Stephen
A. Cook, U Toronto, Canada
The
proof complexity of linear algebra
We
introduce three formal theories of increasing strength for
linear algebra in order to study the complexity of the concepts needed to
prove the basic theorems of the subject. We give what is apparently the
first feasible proofs of the Cayley-Hamilton theorem and other properties
of the determinant, and study the propositional proof complexity of matrix
identities. |
| 17:00- | 17:30
| Daniel Leivant, Indiana U Bloomington, USA
Calibrating
computational feasibility by abstraction rank
We
characterize computationally the functions provable in second
order logic with set existence restricted to natural classes of first order
formulas. A classification of first-order set-existence by implicational
rank yields a natural hierarchy of complexity classes within the class of
Kalmar-elementary functions: The functions over {0,1}* constructively provable
using set existence for formulas of
implicational rank ≤k are precisely
the functions computable in deterministic time O(expk(n)), where exp0=∪k(λn.nk),
and expk+1=2expk.
(For k>0 provability here is by
normal deductions, a demonstrably necessary proviso.) In particular,
set-existence for positive formulas yields exactly PTime. We thus obtain
lean and natural formalisms for codifying feasible mathematics, which are
expressive both in allowing second order definitions and reasoning, and in
incorporating equational programming and reasoning about program
convergence in a direct and uncoded style.
Through a formula-as-type
morphism, we also obtain a link with lambda definability, which we exhibit
in the full paper: The functions over {0,1}*
definable in the polymorphic lambda calculus F2 over a base
of type of words, using first-order
type-arguments of rank ≤k, are
precisely the functions computable in deterministic time O(expk(n)) (again, for k>0 definability is by
normal λ-terms.) The poly-time case was
proved (directly) in D. Leivant/J.Y. Marion, Lambda-caluclus
characterizations of poly-time, Fund.Inform.19, pp. 167-184,
1993. |
Chair:
Gordon Plotkin | 17:30- | 17:40
| Jonathan Ford, U New England, Australia
Ian
A. Mason, U New England, Australia
Natarajan
Shankar, SRI International, USA
Short
presentation: Lessons learned from formal developments in PVS |
| 17:40- | 17:50
| Sylvain Soliman, INRIA Rocquencourt, France
Short
presentation: CLP implementation of a phase model checker |
| 17:50- | 18:00
| Jens Chr. Godskesen, IT U of
Copenhagen, Denmark
Thomas
Hildebrandt, IT U of Copenhagen, Denmark
Vladimiro
Sassone, U Sussex, UK
Short
presentation: An overview of MR, a calculus of mobile resources |
| 18:00- | 18:10
| Claudia Faggian, U Cambridge, UK
Short
presentation: Ludics dynamics: Designs and interactive observability |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
