SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 09:40 - 10:00 at SPLASH-I - R-2 Chair(s): Adrian Sampson, Sheng Chen
Thu 19 Nov 2020 21:40 - 22:00 at SPLASH-I - R-2 Chair(s): Sheng Chen, John Peter Campora

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 (meaning that resolution always selects the same implementation for a particular instantiating type), 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 replicated data types (RDTs). We define a typeclass whose Liquid Haskell type captures the mathematical properties RDTs 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 RDT 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 SPLASH-I +12h
Chair(s): Adrian SampsonCornell University, Sheng ChenUniversity of Louisiana at Lafayette
09:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
09:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
09:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
10:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached
21:00 - 22:20
R-2OOPSLA at SPLASH-I
Chair(s): Sheng ChenUniversity of Louisiana at Lafayette, John Peter CamporaUniversity of Louisiana at Lafayette
21:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
21:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
21:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
22:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached