free-theorems-seq

Given a term, this program calculates a set of "optimal" free theorems that hold in a lambda calculus with selective strictness. It omits totality (in general, bottom-reflection) and other restrictions when possible. The underlying theory is described in the paper "Taming Selective Strictness" (ATPS'09) by Daniel Seidel and Janis Voigtländer. A webinterface for the program is running online at http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi or available offline via the package http://hackage.haskell.org/package/free-theorems-seq-webui. Related to this package you may be interested in the online free theorem generator at http://www-ps.iai.uni-bonn.de/ft that is also available offline via http://hackage.haskell.org/package/free-theorems-webui. Additionally interesting may be the counterexample generator for free theorems that exemplifies the need of strictness conditions imposed by general recursion. It can be downloaded at http://hackage.haskell.org/package/free-theorems-counterexamples or used via a webinterface at http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi.