Automatically Generating Counterexamples to Naive Free Theorems

摘要

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.