Coq 8.6 rc1 发布,交互式证明辅助工具

来源: 投稿
作者: 王练
2016-12-10

Coq 8.6 rc1 发布了,Coq 是一款交互式证明辅助工具,采用OCaml开发,提供一套证明系统,可以编写证明,检查证明。Coq 也提供一套形式化语言,可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明(比如操作系统的安全性和编译器的正确性)。

更新内容:

  • A new, faster state-of-the-art universe constraint checker by Jacques-Henri Jourdan.

  • In CoqIDE and other asynchronous interfaces, more fine-grained asynchronous processing and error reporting by Enrico Tassi, making Coq capable of recovering from errors and continuing to process the document.

  • Better access to the proof engine features from Ltac: goal management primitives, range selectors and a typeclasses eauto engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.

  • Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others.

  • A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond, Pierre-Marie Pédrot and others.

  • Irrefutable patterns in abstractions, by Daniel de Rauglaudre.

  • The ssreflect subterm selection algorithm by Georges Gonthier and Enrico Tassi, now accessible to tactic writers through the ssrmatching plugin.

  • LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.

详情请查看 更新日志

下载地址:

展开阅读全文
2 收藏
分享
加载中
更多评论
0 评论
2 收藏
分享
返回顶部
顶部