(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
This paper presents an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Liquid Haskell augments Haskell with refinement types—our work allows such types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell’s core proof infrastructure. The design sheds light on the interplay between modular proofs and typeclass resolution, which in Haskell is coherent by default, but in other dependently typed languages is not.
We demonstrate the utility of our extension by using Liquid Haskell to modularly verify that 34 instances satisfy the laws of five standard typeclasses. More substantially, we implement a framework for programming distributed applications based on conflict-free replicated data types (CRDTs). We define a typeclass whose Liquid Haskell type captures the mathematical properties CRDTs should satisfy; prove in Liquid Haskell that these properties are sufficient to ensure that replicas’ states converge despite out-of-order update delivery; implement (and prove correct) several instances of our CRDT typeclass; and use them to build two realistic applications, a multi-user calendar event planner and a collaborative text editor.
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50
|(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
|(PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Kayvan Memarian University of Cambridge, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWSLink to publication DOI Authorizer link Pre-print
|(POPL 2021) Data Flow Refinement Type Inference
|(PLDI 2021) RbSyn: type- and effect-guided program synthesis
Sankha Narayan Guria University of Maryland, College Park, Jeffrey S. Foster Tufts University, David Van Horn University of MarylandLink to publication DOI Authorizer link Pre-print