Research results
Niki Vazou, researcher at the IMDEA Software Institute, Martin A.T. Handley and Graham Hutton, from the University of Nottingham, UK have developed “Liquidate your Assets” a paper they presented to POPL2020 . You may find it here.
Liquid Haskell is an extension of Haskell’s Type system that allows annotating types with refinement predicates. It is great for ensuring correctness of code, but it can also be used to improve the performance of code.
Vazou, Handley and Hutton have designed and implement a system that allows Liquid Haskell to be used to formally reason about the resource usage of pure Haskell programs. Moreover, it supports reasoning about correctness and efficiency properties in a combined, uniform manner. “Our system takes the form of a library and requires no modifications or extensions to the compiler” comments Niki Vazou.
They have proven that their library’s approach to cost analysis is correct with respect to an underlying model of execution cost using the metatheory of Liquid Haskell.
In the end, they have demonstrated the applicability of their library on a wide range of case studies, ranging from standard sorting algorithms to sophisticated relational cost properties.
