SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 09:40 - 10:00 at OOPSLA/ECOOP - R-2
Thu 19 Nov 2020 21:40 - 22:00 at OOPSLA/ECOOP - R-2

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.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: R-2OOPSLA at OOPSLA/ECOOP +12h
09:00 - 09:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Pre-print
09:20 - 09:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaCSIRO's Data61/University of New South Wales, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanCarnegie Mellon University, USA
09:40 - 10:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland, College Park, USA, James ParkerUniversity of Maryland, Patrick RedmondUniversity of California, Santa Cruz, USA, Lindsey KuperUniversity of California, Santa Cruz, Michael HicksUniversity of Maryland, Niki VazouIMDEA Software Institute
10:00 - 10:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
21:00 - 22:20: R-2OOPSLA at OOPSLA/ECOOP
21:00 - 21:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Pre-print
21:20 - 21:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaCSIRO's Data61/University of New South Wales, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanCarnegie Mellon University, USA
21:40 - 22:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland, College Park, USA, James ParkerUniversity of Maryland, Patrick RedmondUniversity of California, Santa Cruz, USA, Lindsey KuperUniversity of California, Santa Cruz, Michael HicksUniversity of Maryland, Niki VazouIMDEA Software Institute
22:00 - 22:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University