sessions take place in auditorium 8.
Royer, Syracuse U, USA|
talk: Programs for feasible functionals
||Paulo Oliva, U Aarhus, Denmark|
modified bar recursion
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
||Neil Immerman, U Massachusetts, USA|
talk: Descriptive programming
||G. E. Ostrin, U Bern, Switzerland|
S. Wainer, U Leeds, UK
complexity in a weak arithmetic
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³.
||Daniel Leivant, Indiana U Bloomington, USA|
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.
||Maria Emilia Maietti, U Padova, Italy|
Ritter, U Birmingham, UK
bounds in rudimentary linear lambda calculus
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.
||Peter Mĝller Neergaard, Brandeis U, USA|
G. Mairson, Brandeis U, USA
is square: Representation and expressiveness in light affine
focus on how the choice of input-output representation has a
crucial impact on the expressiveness of so-called "logics of polynomial time."
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[22n], 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[nk] in depth
O(logk) 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