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.