This tool allows you to run the algorithm described in the paper “Automatically Generating Counterexamples to Naive Free Theorems” (FLOPS'10) by Daniel Seidel and Janis Voigtländer.

You may also want to try the following related tools:

• “Automatic Generation of Free Theorems”
• “Taming Selective Strictness”

Please enter a type. You can prepend it with a list of type variables that should not be considered for counterexample generation, e.g. “a b. ((a,c) -> b) -> b”.

The source code is available for download.

© 2010 Daniel Seidel <ds@iai.uni-bonn.de> and Joachim Breitner <mail@joachim-breitner.de>