hout
Hout is an in-Haskell non-interactive proof assistant for intuitionistic first-order logic, using Haskell's type system. If a proof written in Hout compiles, it is correct. Alternatively, Hout provides an indexed monad which, combined with Haskell's do notation, allows for writing Haskell code in the style of proof assistants. The main part of Hout's value is found in Hout.Prover.Tactics, which defines the Tactic monad and several proof tactics similar to those found in Coq. Other useful defintions for using Hout can be found in Hout.Prover.Proofs.
Ecosystem
hackage.haskell.org
hackage.haskell.org
Latest Release
almost 6 years ago
0.1.0.0
almost 6 years ago
Versions
1
1
Downloads
431 total
431 total
Loading...
Readme
Loading...
Links
| Registry | hackage.haskell.org |
| Source | Repository |
| Homepage | Homepage |
| JSON API | View JSON |
| CodeMeta | codemeta.json |
Package Details
| PURL |
pkg:hackage/hout
spec |
| License | BSD-3-Clause |
| First Release | almost 6 years ago |
| Last Synced | 16 days ago |
Repository
| Stars | 38 on GitHub |
| Forks | 1 on GitHub |