一句话：提出 QuickSpec 的新理论探索架构，通过测试 Haskell 程序自动发现更复杂、更快的等式性质与引理。
QuickSpec 是一个理论探索系统，可自动测试 Haskell 程序并发现其中的等式性质；这些性质既有助于理解程序，也可作为引理辅助正确性证明。用户只需提供待测函数和 QuickCheck 数据生成器，系统便较大程度自动运行。此前包括早期 QuickSpec 在内的理论探索系统扩展性较差，难以发现复杂定律。本文提出一种新的理论探索架构，显著提升了可扩展性与速度。结果表明，新架构能找到远比以前复杂且更快的定律，并在函数式编程与数学问题上进行了演示。
Abstract QuickSpec is a theory exploration system which tests a Haskell program to find equational properties of it, automatically. The equations can be used to help understand the program, or as lemmas to help prove the program correct. QuickSpec is largely automatic: the user just supplies the functions to be tested and QuickCheck data generators. Previous theory exploration systems, including earlier versions of QuickSpec itself, scaled poorly. This paper describes a new architecture for theory exploration with which we can find vastly more complex laws than before, and much faster. We demonstrate theory exploration in QuickSpec on problems both from functional programming and mathematics.
@article{SmallboneJCA17,
title = {Quick specifications for the busy programmer},
author = {NICHOLAS SMALLBONE and MOA JOHANSSON and KOEN CLAESSEN and MAXIMILIAN ALGEHED},
journal = {Journal of Functional Programming},
volume = {27},
year = {2017},
doi = {10.1017/s0956796817000090}
}