FLoC '02 - ICC Sunday July 21st

ICC on Sunday

Detailed program
Sunday July 21st, 2002
See also the unified by-slot program

All sessions take place in auditorium 8.

Session 4

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.

Session 5

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³.

Session 6

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^2ⁿ], 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(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 computation.