hackage.haskell.org : 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.
Registry
-
Source
- Homepage
- JSON
purl: pkg:hackage/hout
Keywords:
bsd3
, library
, logic
, type-system
, Propose Tags
, curry-howard-isomorphism
, monad
, proof-assistant
License: BSD-3-Clause
Latest release: over 5 years ago
First release: over 5 years ago
Downloads: 408 total
Stars: 37 on GitHub
Forks: 1 on GitHub
See more repository details: repos.ecosyste.ms
Last synced: 12 days ago