Daniel Seidel, Janis Voigtländer. Automatically Generating Counterexamples to Naive Free Theorems. In Matthias Blume, Naoki Kobayashi, Germán Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Volume 6009 of Lecture Notes in Computer Science, pages 175-190, Springer, 2010. [doi]
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 falsifi cation as it is for verifi cation. 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.