gdp: Reason about invariants and preconditions with ghosts of departed proofs.

[ bsd3, library, program, safe ] [ Propose Tags ]

Reason about invariants and preconditions with ghosts of departed proofs. The GDP library implements building blocks for creating and working with APIs that may carry intricate preconditions for proper use. As a library author, you can use gdp to encode your API's preconditions and invariants, so that they will be statically checked at compile-time. As a library user, you can use the gdp deduction rules to codify your proofs that you are using the library correctly.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.0.0.1, 0.0.0.2, 0.0.3.0
Dependencies base (>=4.7 && <5), gdp, lawful [details]
License BSD-3-Clause
Copyright (c) 2018 Matt Noonan
Author Matt Noonan
Maintainer matt.noonan@gmail.com
Category Safe
Home page https://github.com/matt-noonan/gdp#readme
Source repo head: git clone https://github.com/matt-noonan/gdp
Uploaded by mnoonan at 2019-11-13T00:39:06Z
Distributions LTSHaskell:0.0.3.0, NixOS:0.0.3.0, Stackage:0.0.3.0
Reverse Dependencies 4 direct, 7 indirect [details]
Executables gdp
Downloads 1943 total (21 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2019-11-13 [all 1 reports]

Readme for gdp-0.0.3.0

[back to package description]

gdp: Ghosts of Departed Proofs