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: