The free-theorems-seq package

[Tags: library, public-domain]

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 or available offline via the package

Related to this package you may be interested in the online free theorem generator at that is also available offline via 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 or used via a webinterface at


Change logNone available
Dependenciesarray (==0.*), base (>=1), bytestring (>=, containers (>=, free-theorems (>=0.3.1 && <0.4), haskell-src (>=, mtl (>=, old-locale (==1.*), old-time (==1.*), parsec (==3.*), pretty (==1.*), syb (>=, utf8-string (>= && <0.4), xhtml (==3000.*)
AuthorDaniel Seidel
UploadedFri Mar 11 17:07:18 UTC 2011 by DanielSeidel
Downloads208 total (14 in last 30 days)
StatusDocs available [build log]
Successful builds reported [all 1 reports]




Maintainers' corner

For package maintainers and hackage trustees