[Haskell'22] Liquid Proof Macros

Описание: Liquid Proof Macros (Video, Haskell 2022)
Henry Blanchette, Niki Vazou, and Leonidas Lampropoulos
(University of Maryland at College Park, USA; IMDEA Software Institute, Spain; University of Maryland at College Park, USA)

Abstract: Liquid Haskell is a popular verifier for Haskell programs,
leveraging the power of SMT solvers to ease users' burden of proof.
However, this power does not come without a price:
convincing Liquid Haskell that a program is correct
often necessitates giving hints to the underlying solver, which can be
a tedious and verbose process that sometimes requires intricate
knowledge of Liquid Haskell's inner workings.


In this paper, we present Liquid Proof Macros, an extensible
metaprogramming technique and framework for simplifying the
development of Liquid Haskell proofs.
We describe how to leverage Template Haskell to generate Liquid
Haskell proof terms, via a tactic-inspired DSL interface for more
concise and user-friendly proofs,
and we demonstrate the capabilities of this framework by automating
a wide variety of proofs from an existing Liquid Haskell benchmark.

Article: https://doi.org/10.1145/3546189.3549921

Supplementary archive: https://doi.org/10.1145/3554302 (Badges: Artifacts Available)

Supplementary web page: https://github.com/Riib11/lh-tactics-...

ORCID: https://orcid.org/0000-0002-9415-0944, https://orcid.org/0000-0003-0732-5476, https://orcid.org/0000-0003-0269-9815

Video Tags: Liquid Haskell, Proof Macros, Tactics, icfpws22haskellmain-p57-p, doi:10.1145/3546189.3549921, doi:10.1145/3554302, orcid:0000-0002-9415-0944, orcid:0000-0003-0732-5476, orcid:0000-0003-0269-9815, Artifacts Available

Presentation at the Haskell 2022 conference, September 15–16, 2022, https://icfp22.sigplan.org/home/haske...
Sponsored by ACM, ACM SIGPLAN, https://www.sigplan.org/