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]
Versions 0.0.0.1, 0.0.0.2
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/githubuser/gdp#readme
Source repo head: git clone https://github.com/matt-noonan/gdp
Uploaded by mnoonan at Mon Jun 18 02:02:57 UTC 2018
Distributions LTSHaskell:0.0.0.2, NixOS:0.0.0.2, Stackage:0.0.0.2
Executables gdp
Downloads 164 total (17 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2018-06-18 [all 1 reports]
Hackage Matrix CI

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for gdp-0.0.0.2

[back to package description]

gdp: Ghosts of Departed Proofs