Skip to main content

Research Repository

Advanced Search

All Outputs (2)

Liquidate your assets: reasoning about resource usage in liquid Haskell (2019)
Journal Article
Handley, M., Vazou, N., & Hutton, G. (2019). Liquidate your assets: reasoning about resource usage in liquid Haskell. Proceedings of the ACM on Programming Languages, 4, 1-27. https://doi.org/10.1145/3371092

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 pro... Read More about Liquidate your assets: reasoning about resource usage in liquid Haskell.

Call-by-need is clairvoyant call-by-value (2019)
Journal Article
Hackett, J., & Hutton, G. (2019). Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages, 3(ICFP), 1-21. https://doi.org/10.1145/3341718

Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics, which uses a heap to memoise the results of delayed... Read More about Call-by-need is clairvoyant call-by-value.