name: free-theorems-counterexamples
version: 0.3.1.0
license: PublicDomain
author: Daniel Seidel, Joachim Breitner
maintainer: ds@iai.uni-bonn.de
synopsis: Automatically Generating Counterexamples to Naive Free Theorems
description:
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
.
.
Related to this package you may be interested in the online free theorem generator
at that is also available offline via
.
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
but the functionality is as well provided via a webinterface at
.
category: Language
tested-with: GHC==7.6.1
build-type: Simple
cabal-version: >= 1.2.3
extra-source-files:
Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs
Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestGen.hs
testcgi.py
test.sh
README
library
build-depends:
mtl >= 1.0
, haskell-src >= 1.0
, haskell-src-exts >= 0.3.9
, pretty >= 1.0.0.0
, containers >= 0.1.0.1
, HUnit >= 1.2
if impl(ghc >= 6.10)
build-depends:
base >= 4
, syb >= 0.1.0.0
else
build-depends:
base >= 1 && < 4
exposed-modules:
Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind
Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType
Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon
Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended
other-modules:
Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync
Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.M
Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.TimeOut
executable counterexamples.cgi
main-is:
counterexamples-cgi.hs
build-depends:
xhtml, cgi, utf8-string, free-theorems >= 0.3.1.3
extensions:
FlexibleContexts
, DeriveDataTypeable
, ScopedTypeVariables