Refinement Type Refutations
summary
Systematically turns bidirectional refinement type rules into refutations and defines must-instantiation as the concrete set of term inhabitants that prove a typing failure. Implements the method in HayStack, an extension to LiqidHaskell, which automatically finds and interactively displays counterexamples. Evaluated on LiqidHaskell and G2 benchmarks, it finds refutations for 99.7% of benchmarks and runs roughly an order of magnitude faster than G2, including support for abstract, bounded refinements and reflection.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 3:34Refinement type checks fail
- 5:41Type failures with refinements
- 8:11Must instantiation in practice
- 8:32Arithmetic expression case study
- 10:00Evaluator with refinement types
- 11:49Exploring counterexamples
- 12:11Evaluating refutations
- 14:00Performance challenges
- 14:23Summary
related talks
34mLiquid Haskell: Verification with Refinement Types
46mRefinement Types from Light to Deep Verification
29mExplicit Refinement Types
16mA Hoare-Logic Style Refinement Types Formalisation
58mLiquidHaskell: Liquid Types for Haskell
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
35mThe Mastermind behind Refinement Types
21mChecking Equivalence in a Non-strict Language