Scifaro

中文

使用 Isabelle/HOLCF-Prelude 认证 HLint 提示

计算机科学中的逻辑 2013-06-07 v1

作者: Joachim Breitner , Brian Huffman , Neil Mitchell , Christian Sternagel

在 arXiv 上查看 ↗ PDF ↗

摘要

我们提出了 HOLCF-Prelude，这是在 Isabelle/HOLCF 中对 Haskell 标准预库 (prelude) 大部分内容的形式化。将此形式化应用于 HLint 所建议的提示，使我们能够对其进行形式化认证。

关键词

形式化验证 Isabelle/HOLCF Haskell 预库 HLint 认证提示函数式编程定理证明

引用

@article{arxiv.1306.1340,
  title  = {Certified HLints with Isabelle/HOLCF-Prelude},
  author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel},
  journal= {arXiv preprint arXiv:1306.1340},
  year   = {2013}
}

备注

1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 5 pages