Liquid proof macros
Liquid proof macros
复制标题
防液宏
DOI：
10.1145/3546189.3549921
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Lampropoulos, Leonidas
中科院分区：
文献类型：
--
作者：
Blanchette, Henry;Vazou, Niki;Lampropoulos, Leonidas
Liquid Haskell是Haskell程序的流行验证器， 利用SMT求解器的强大功能减轻用户的举证负担。 然而，这种力量并非没有代价： 让Liquid Haskell相信一个程序是正确的 通常需要向底层求解程序提供提示， 这是一个冗长乏味的过程，有时需要复杂的 了解Liquid Haskell的内部工作原理。在本文中，我们提出了Liquid Proof Macros，一个可扩展的 元编程技术和框架，用于简化 Liquid Haskell Proofs的开发 我们描述如何利用模板Haskell生成Liquid Haskell proof terms，通过一个战术启发的DSL接口，了解更多 简洁和用户友好的证明， 我们展示了这个框架的功能， 从现有的Liquid Haskell基准测试中获得了各种各样的证明。
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.
登录
查看更多内容
触发选择策略以稳定程序验证者
DOI：
--
发表时间：
2016
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
K. Leino;Clément Pit
通讯作者：
Clément Pit
三年 Sledgehammer 经验，自动和交互式定理证明者之间的实用联系
DOI：
--
发表时间：
2012
期刊：
IWIL@LPAR
影响因子：
--
作者：
Lawrence Charles Paulson;J. Blanchette
通讯作者：
J. Blanchette
DOI：
10.1007/s10817-018-9458-4
发表时间：
2018
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Czajka Ł;Kaliszyk C
通讯作者：
Kaliszyk C
所有人的定理证明：液体 Haskell 中的等式推理（功能性珍珠）
DOI：
10.1145/3242744.3242756
发表时间：
2018
期刊：
Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell
影响因子：
--
作者：
Niki Vazou;Joachim Breitner;Rose Kunkel;David Van Horn;G. Hutton
通讯作者：
G. Hutton
利用归纳关系正确计算
DOI：
10.1145/3519939.3523707
发表时间：
2022
期刊：
Programming Language Design and Implementation
影响因子：
--
作者：
Paraskevopoulou, Zoe;Eline, Aaron;Lampropoulos, Leonidas
通讯作者：
Lampropoulos, Leonidas