Write a Blog >>

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program efficiency in the same setting, with the system’s existing verification machinery being used to ensure that the results are both valid and precise. To illustrate our approach, we analyse the efficiency of a wide range of popular data structures and algorithms, and in doing so, explore various notions of resource usage. Our experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and that the two can naturally be combined.

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 - 12:07
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 - 12:30
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