POPL 2020 (series) / Research Papers /
Recurrence Extraction for Functional Programs through Call-by-Push-Value
Wed 22 Jan 2020 11:45 - 12:07 at Ile de France II (IDF II) - Reasoning about Program Complexity/Efficiency Chair(s): Thomas Wies
The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.
Slides (popl2020-recextr.pdf) | 1.80MiB |
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change
11:45 - 12:30 | Reasoning about Program Complexity/EfficiencyResearch Papers at Ile de France II (IDF II) Chair(s): Thomas Wies New York University | ||
11:45 22mTalk | Recurrence Extraction for Functional Programs through Call-by-Push-Value Research Papers Alex Kavvos Aarhus University, Edward Morehouse Wesleyan University, Daniel R. Licata Wesleyan University, Norman Danner Wesleyan University Link to publication DOI File Attached | ||
12:07 22mTalk | Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell Research Papers Martin Adam Thomas Handley University of Nottingham, Niki Vazou IMDEA Software Institute, Graham Hutton University of Nottingham, UK Link to publication DOI Media Attached File Attached |