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
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:30: DICE-FOPARA - III at S11
Chair(s): Patrick BaillotCNRS & ENS Lyon
dice-fopara-2019-papers14:00 - 14:45
Bruce KapronUniversity of Victoria, Florian SteinbergINRIA Saclay
dice-fopara-2019-papers14:45 - 15:30
Emmanuel Hainry, Bruce KapronUniversity of Victoria, Jean-Yves Marion LORIA, Romain PéchouxINRIA / LORIA