Liquid Haskell extends Haskell with a refinement type system. Refinement types add predicates to types, which allow users to specify properties about their code. Due to the Curry-Howard isomorphism, users can prove these properties are satisfied by writing programs as proof. In our research, we encode and verify security and correctness properties about Haskell programs using Liquid Haskell. For one project, we show that LWeb, a dynamic information flow control (IFC) framework for database-backed web applications, enjoys non-interference. In another project, we prove that replicated data types, which are used to build distributed applications, satisfy required mathematical properties to ensure strong convergence.

Publications related to this project:

• Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell. Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou. (Conditionally accepted to OOPSLA 2020.)
• LWeb: Information Flow Security for Multi-Tier Web Applications, POPL 2019. James Parker, Niki Vazou, and Michael Hicks.