Enhancing Proof Development in Liquid- Haskell: Implementation and Evaluation of Typed Holes

Abstract

Refinement type systems provide mechanisms for specifying and verifying programs beyond what mainstream type systems can express. LiquidHaskell extends Haskell with refinement types, and beyond that, has evolved to be used as a theorem prover, akin to Agda or Idris. Unfortunately, it lacks a fundamental feature present in most proof assistants: the ability to inspect goals during proof development, for example, with typed holes. In this thesis, I implement typed hole support for LiquidHaskell addressing this limitation and taking an initial step towards more interactivity in LiquidHaskell.