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

[Skip to Readme]


Versions 1.0
Dependencies array (==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.*) [details]
License PublicDomain
Author Daniel Seidel
Stability Unknown
Category Language
Uploaded Fri Mar 11 17:07:18 UTC 2011 by DanielSeidel
Distributions NixOS:1.0
Downloads 294 total (4 in the last 30 days)
0 []
Status Docs available [build log]
Successful builds reported [all 1 reports]




Maintainer's Corner

For package maintainers and hackage trustees

Readme for free-theorems-seq

Readme for free-theorems-seq-1.0

The module free-theorems-seq-0.1 can be installed via

cabal install

or the following way:

runhaskell Setup.hs configure --user
runhaskell Setup.hs build
runhaskell Setup.hs haddock
runhaskell Setup.hs install

runhaskell Setup.hs haddock builds the documentation.
This step is not necessary.

After installation the modules
are available.

The functionality of the library is also available via a webinterface
that is either available via the package at

or can be used online at