Automatically Generating Counterexamples to Naive Free Theorems
| Authors: | D. Seidel and J. Voigtländer |
|---|---|
| Published: | In 10th International Symposium on Functional and Logic Programming (FLOPS'10, acceptance rate 21/49), Sendai, Japan, Proceedings, volume 6009 of LNCS, pages 175-190, Springer, April 2010. |
| DOI: | 10.1007/978-3-642-12251-4_14 |
| BibTeX: | SV10.bib |
| Abstract: | Disproof can be as important as proof in studying programs and programming languages. In particular, side conditions in a statement about program behavior are sometimes best understood and explored by trying to exhibit a falsifying example in the absence of a condition in question. Automation is as desirable for such falsification as it is for verification. We develop formal and implemented tools for counterexample generation in the context of free theorems, i.e., statements derived from polymorphic types a la relational parametricity. The machinery we use is rooted in constraining the type system and in intuitionistic proof search. |
| Download: | AutomaticallyGeneratingCounterexamplesToNaiveFreeTheorems.pdf |
| Rights: | Copyright held by Springer. |
The implementation of the algorithm presented in this paper is accessible via a web interface here.