Papers etc.¶
Papers¶
To learn about the theory behind Liquid Types, I recommend reading first the PLDI 2008 paper and then the ESOP 2013 paper. Alternatively, one lazy weekend, you could curl up with:
Haskell¶
- REST: Integrating Term Rewriting with Program Verification, ECOOP 2022
- Refinement Reflection: Complete Verification with SMT, POPL 2018
- Local Refinement Typing, ICFP 2017
- Bounded Refinement Types, ICFP 2015
- Refinement Types For Haskell, ICFP 2014
- LiquidHaskell in the Real World, Haskell 2014
- Abstract Refinement Types, ESOP 2013
ML¶
- Liquid Types, PLDI 2008
- Type-based Data Structure Verification, PLDI 2009
- Dsolve: Safety Verification via Liquid Types, CAV 2010
- HMC: Verifying Functional Programs with Abstract Interpreters, CAV 2011
C¶
- Low-level Liquid Types, POPL 2010
- Deterministic Parallelism With Liquid Effects, PLDI 2012
- Verifying C With Liquid Types, CAV 2012
Talks¶
- Untangle your spaghetti with Liquid Haskell (slides)
- Resource Analysis with Refinement Types, YOW! Lambda Jam 2021
- Liquid Haskell: Theorem Proving for All, Haskell Exchange 2018
- Scrap your Bounds Checks with Liquid Haskell, Haskell Exchange 2017 (slides)
The following talks are good tutorial introductions to the techniques.
Other articles¶
- Assumptions for Liquid Haskell in the Large, Tweag blog 2023
- A Dialog with Liquid Haskell, Tweag blog 2022
- Why Liquid Haskell Matters, Tweag blog 2022
- Compile-time memory safety using Liquid Haskell, Haskell for all blog 2015
People¶
Liquid Types have been developed in the UCSD Programming Systems group by
- Alexander Bakst
- Ranjit Jhala
- Ming Kawaguchi
- Patrick Rondon
- Eric Seidel
- Michael Smith
- Anish Tondwalkar
- Chris Tetreault
- Niki Vazou
Thanks¶
This work is funded by NSF grants CCF-0644361, CNS-0720802, CCF-0702603, and generous gifts from Microsoft Research.