December 6, 2024
Appearing at OOPSLA 2024, Refinement Type Refutations are an attempt to address “cryptic” or completely unreadable error messages that occur when using Refinement Type systems. These errors can occur from either the source code or the specification and a useful error message should be grounded in an understandable set of types for the user. This work extends LiquidHaskell with type-checking rules to obtain such refutations and provides an interactive user-interface called HayStack. The authors of this paper have an accompanying blog post at https://vusecpl.github.io/2024-06-29-type-refutations/. This talk will describe the approach and some examples in a “Papers We Love” style.
About Patrick LaFontaine
Patrick LaFontaine sits in desk 33 of Lawson 3133. Due to often writing incorrect code, he focuses on systems that will create correct code for him. His presentations are often described as “getting a few chuckles”(2024). Patrick is not a fan of bugs, in software or otherwise.