ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 14:00 - 14:45 at S11 - III Chair(s): Patrick Baillot

Motivated by recent results of Kapron and Steinberg (LICS 2018) we introduce new forms of iteration on length in the setting of applied lambda-calculi for higher-type poly-time computability. In particular, in a type-two setting, we consider functionals which capture iteration on input length which bound interaction with the type-one input parameter, by restricting to a constant either the number of times the function parameter may return a value of increasing size, or the number of times the function paramater may be applied to an argument of increasing size. We prove that for any constant bound, the iterators obtained are equivalent, with respect to lambda definability over type one poly-time functions, to the recursor of Cook and Urquhart which captures Cobham’s notion of limited recursion on notation in this setting.

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:30
IIIDICE-FOPARA at S11
Chair(s): Patrick Baillot CNRS & ENS Lyon
14:00
45m
Talk
Type-two Iteration with Bounded Query Revision
DICE-FOPARA
Bruce Kapron University of Victoria, Florian Steinberg INRIA Saclay
14:45
45m
Talk
Tiered complexity at higher order
DICE-FOPARA
Emmanuel Hainry , Bruce Kapron University of Victoria, Jean-Yves Marion LORIA, Romain Péchoux INRIA / LORIA