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

We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between processes and stand in a Curry-Howard correspondence with intuitionistic linear logic. The main innovation is to enrich session types with the temporal modalities next ($\bigcirc$A), always ($\Box$A), and eventually ($\Diamond$A), to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The resulting temporal session types uniformly express properties such as the message rate of a stream, the latency of a pipeline, the response time of a concurrent queue, or the span of a fork/join parallel program. The analysis is parametric in the cost model and the presentation focuses on communication cost as a concrete example. The soundness of the analysis is established by proofs of progress and type preservation using a timed multiset rewriting semantics. Representative examples illustrate the scope and usability of the approach.

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