Liquidate your assets: reasoning about resource usage in liquid Haskell

Handley, Martin; Vazou, Niki; Hutton, Graham

Abstract

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. We use the system’s existing verification machinery to ensure that the results of our cost analysis are valid, together with custom invariants for particular program contexts to ensure that the results of our analysis are 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.

Citation

Handley, M., Vazou, N., & Hutton, G. Liquidate your assets: reasoning about resource usage in liquid Haskell. Presented at 47th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 47th ACM SIGPLAN Symposium on Principles of Programming Languages
• Acceptance Date: Nov 11, 2019
• Publication Date: Dec 20, 2019
• Deposit Date: Nov 12, 2019
• Publicly Available Date: Jan 14, 2020
• Journal: Proceedings of the ACM on Programming Languages
• Electronic ISSN: 2475-1421
• Publisher: Association for Computing Machinery (ACM)
• Volume: 4
• Article Number: 24
• Pages: 1-27
• Series Title: Proceedings of the ACM on Programming Languages
• DOI: https://doi.org/10.1145/3371092
• Public URL: https://nottingham-repository.worktribe.com/output/3231921