hout: Non-interactive proof assistant monad for first-order logic.
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
and several proof tactics similar to those found in Coq.
Other useful defintions for using Hout can be found in
[Skip to Readme]
|Dependencies||base (>=4.7 && <5), indexed [details]|
|Copyright||2020 Isaac van Bakel|
|Author||Isaac van Bakel|
|Category||Type System, Logic|
|Source repo||head: git clone https://github.com/ivanbakel/hout-prover|
|Uploaded||by ivanbakel at 2020-04-11T22:04:39Z|
|Downloads||290 total (0 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
|Status||Docs available [build log]
Last success reported on 2020-04-11 [all 1 reports]