SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Tue 19 Oct 2021 14:20 - 14:35 at Zurich E - Types, Proofs, and Design Theory Chair(s): Alan Jeffrey

Liquid Haskell is an extension to the Haskell programming language that adds support for refinement types: data types augmented with SMT-decidable logical predicates that refine the set of values that can inhabit a type. Furthermore, Liquid Haskell’s support for refinement reflection enables the use of Haskell for general-purpose mechanized theorem proving. A growing list of large-scale mechanized proof developments in Liquid Haskell take advantage of this capability. Adding theorem-proving capabilities to a “legacy” language like Haskell lets programmers directly verify properties of real-world Haskell programs (taking advantage of the existing highly tuned compiler, run-time system, and libraries), just by writing Haskell. However, more established proof assistants like Agda and Coq offer far better support for interactive proof development and insight into the proof state (for instance, what subgoals still need to be proved to finish a partially-complete proof). In contrast, Liquid Haskell provides only coarse-grained feedback to the user – either it reports a type error, or not – unfortunately hindering its usability as a theorem prover.

In this paper, we propose improving the usability of Liquid Haskell by extending it with support for Agda-style typed holes and interactive editing commands that take advantage of them. In Agda, typed holes allow programmers to indicate unfinished parts of a proof, and incrementally complete the proof in a dialogue with the compiler. While GHC Haskell already has its own Agda-inspired support for typed holes, we posit that typed holes would be especially powerful and useful if combined with Liquid Haskell’s refinement types and SMT automation. We discuss how typed holes might work in Liquid Haskell, and we consider possible implementation approaches and next steps.

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
Types, Proofs, and Design TheoryHATRA at Zurich E
Chair(s): Alan Jeffrey Roblox
13:50
15m
Talk
Toward a Theory of Programming Language and Reasoning Assistant Design: Minimizing Cognitive Load
HATRA
Michael Coblenz University of Maryland at College Park
Link to publication
14:05
15m
Talk
Towards an Incremental Dataset of Proofs
HATRA
Hanneli Tavante McGill University
Pre-print
14:20
15m
Talk
Toward Hole-Driven Development with Liquid Haskell
HATRA
Patrick Redmond University of California at Santa Cruz, Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:35
15m
Talk
Toward SMT-Based Refinement Types in Agda
HATRA
Gan Shen University of California, Santa Cruz, USA, Lindsey Kuper University of California at Santa Cruz
Link to publication
14:50
20m
Talk
Paper discussion, session 2
HATRA