Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Wed 26 Sep 2018 15:46 - 16:10 at Stifel Theatre - Complexity and Bounds Chair(s): Ilya Sergey

Multi types—aka non-idempotent intersection types—have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps.

Starting from this observation, we refine and generalise a technique introduced by Bernadet & Lengrand to provide exact bounds for the maximal strategy. Our typing judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the lambda-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation).

Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Lengrand via a uniform technique and a complexity-based perspective. The two main novelties, instead, are exact split bounds for the leftmost strategy—the only strong strategy known to provide a %reasonable complexity measure—and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear %substitution calculus.

Wed 26 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:00 - 16:10
Complexity and BoundsResearch Papers at Stifel Theatre
Chair(s): Ilya Sergey University College London
15:00
23m
Talk
Parallel Complexity Analysis with Temporal Session Types
Research Papers
Ankush Das Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA
DOI
15:23
23m
Talk
Parametric Polymorphism and Operational Improvement
Research Papers
Jennifer Hackett University of Nottingham, UK, Graham Hutton University of Nottingham, UK
DOI
15:46
23m
Talk
Tight Typings and Split Bounds
Research Papers
Beniamino Accattoli Inria & Ecole Polytechnique, Stéphane Graham-Lengrand CNRS, France, Delia Kesner IRIF, France / University of Paris Diderot, France
DOI