| | All
sessions take place in auditorium 8.11:00- | 12:00
| James S.
Royer, Syracuse U, USA Invited
talk: **Programs for feasible functionals** |
12:00- | 12:30
| Paulo Oliva, U Aarhus, Denmark
**On
modified bar recursion** Modified
bar recursion is a variant of Spector's bar recursion
which can be used to give a realizability interpretation of the classical
axiom of dependent choice. This realizability allows for the extraction of
witnesses from proofs of forall-exists-formulas in classical analysis. In
this talk I shall report on results regarding the relationship between
modified and Spector's bar recursion. I shall also show that a seemingly
weak form of modified bar recursion is as strong as "full" modified bar
recursion in higher
types. |
14:00- | 15:00
| Neil Immerman, U Massachusetts, USA Invited
talk: **Descriptive programming** |
15:00- | 15:30
| G. E. Ostrin, U Bern, Switzerland S.
S. Wainer, U Leeds, UK
**Computational
complexity in a weak arithmetic** A
formal theory, analogous to Peano Arithmetic, is developed
whereby the variables are separated into two kinds; those that can be
quantified over and those that relate to inductions. The resulting theory
has strength significantly weaker than Peano Artithmetic: the provably
recursive functions now being exactly Grzegorczyk's class *E*³. By
further restricting the induction formulas with
respect to formula complexity the provably recursive functions now relate
to a known function hierarchy that sits neatly between Grzegorczyk's
classes *E*² and *E*³. |
16:00- | 16:30
| Daniel Leivant, Indiana U Bloomington, USA
**Facets
of ramification** Ramification
of set abstraction in Type Theory was proposed by
Whitehead and Russell, and adapted by Shütte to
second order logic. Over the last decade odd ramification of data was
proposed and studied, with the aim of regulating computational behavior and
guaranteeing computational feasibility. We establish here the unity of the
two forms of ramification, by showing that ramified induction is syntactic
sugar for ramified second-order logic with closed comprehension. |
16:30- | 17:00
| Maria Emilia Maietti, U Padova, Italy Eike
Ritter, U Birmingham, UK
**Normalization
bounds in rudimentary linear lambda calculus** Surprisingly
we show that in rudimentary intuitionistic linear
lambda calculus there are no linear bounds for normalizing terms under
substitutions when commuting conversions are considered. We show that such
a bound exists if we only count beta-reductions or consider evaluation to
values of closed terms. |
17:00- | 17:30
| Peter Mĝller Neergaard, Brandeis U, USA Harry
G. Mairson, Brandeis U, USA
**LAL
is square: Representation and expressiveness in light affine
logic** We
focus on how the choice of input-output representation has a
crucial impact on the expressiveness of so-called "logics of polynomial time."
Our analysis
illustrates this dependence in the context of *Light Affine
Logic* (LAL), which is both a restricted version of Linear Logic, and a
primitive functional programming language with restricted sharing of
arguments. By slightly relaxing representation conventions, we derive
doubly-exponential expressiveness bounds for this "logic of polynomial time."
We emphasize that
*squaring* is the unifying idea that relates upper bounds on
cut eliminations for LAL with lower bounds on representation.
Representation issues arise in the simulation of DTIME[2^{2n}], where we construct *uniform families* of proof-nets
encoding Turing Machines.
Specifically, the dependence on *n* only affects
the number of enclosing *boxes*. A related technical
improvement is the simulation of DTIME[*n*^{k}] in depth
*O*(log*k*) LAL proof-nets. The resulting upper bounds on
cut elimination then satisfy the properties of a *first-class* polynomial
Turing Machine simulation, where there
is a fixed polynomial slowdown in the simulation of any polynomial
computation. |
| |