Call for Sponsors: First-class Liquid Haskell

[Iceland_jack]

[Paper] Quotient Haskell: Lightweight Quotient Types for All

Abstract Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We de…