Write a Blog >>

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 Jan
Times are displayed in 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 WiesNew York University
11:45
22m
Talk
Recurrence Extraction for Functional Programs through Call-by-Push-Value
Research Papers
Alex KavvosAarhus University, Edward MorehouseWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
Link to publication DOI File Attached
12:07
22m
Talk
Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell
Research Papers
Martin Adam Thomas HandleyUniversity of Nottingham, Niki VazouIMDEA Software Institute, Graham HuttonUniversity of Nottingham, UK
Link to publication DOI Media Attached File Attached