Hackage :: [Package]

free-theorems-counterexamples: Automatically Generating Counterexamples to Naive Free Theorems

[ language, library, program, public-domain ] [ Propose Tags ] [ Report a vulnerability ]

This program is to verify (or to put into question) strictness conditions on free theorems that arise if a polymorphic lambda calculus is enriched by general recursion. Given a type the program either returns an instance of the corresponding unrestricted free theorem that does not hold and thereby verifies the need of the additional restrictions or it returns without finding such an instantiation and thereby suggests (but not proves) that the strictness conditions are superfluous. The underlying algorithm is described in "Automatically Generating Counterexamples to Naive Free Theorems" (FLOPS'10) by Daniel Seidel and Janis Voigtländer. A webinterface for the program is also available at http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi.

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/cgi-bin/hackage-scripts/package/free-theorems-webui. Also interesting may be the tool polyseq that generates "optimal" free theorems in a polymorphic lambda calculus with selective strictness. Polyseq can be downloaded at http://hackage.haskell.org/cgi-bin/hackage-scripts/package/polyseq but the functionality is as well provided via a webinterface at http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi.

[Skip to Readme]

Modules

  • Language
    • Haskell
      • FreeTheorems
        • Variations
          • CounterExamples
            • Common
              • Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
            • Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind
            • Internal
              • Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended
            • Parser
              • Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.3, 0.3.0.1, 0.3.0.2, 0.3.1.0
Dependencies base (>=1), cgi, containers (>=0.1.0.1), free-theorems (>=0.3.1.3), haskell-src (>=1.0), haskell-src-exts (>=0.3.9), HUnit (>=1.2), mtl (>=1.0), pretty (>=1.0.0.0), syb (>=0.1.0.0), utf8-string, xhtml [details]
Tested with ghc ==7.6.1
License LicenseRef-PublicDomain
Author Daniel Seidel, Joachim Breitner
Maintainer ds@iai.uni-bonn.de
Category Language
Uploaded by DanielSeidel at 2013-02-14T13:36:17Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables counterexamples.cgi
Downloads 3297 total (14 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Successful builds reported [all 8 reports]

Readme for free-theorems-counterexamples-0.3.1.0

[back to package description] 
The module free-theorems-counterexamples-0.3 can be installed 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
        Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind
        Language.Haskell.FreeTheorems.Variations.CounterExamples.Algorithm.ExFindExtended
        Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
        Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
are available.

To start the webinterface do

$ ./test.sh

then it runs under  http://localhost:8002/

The webinterface can also be found under

http://www-ps.iai.uni-bonn/cgi-bin/exfind.cgi

Enjoy.