package coq-freespec-core
A framework for implementing and certifying impure computations in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
freespec.0.3.tar.gz
sha512=a4321066ef6267fc87a27b7b4ce7bd75db9878dcf33f7463ee3d11bdedb6a13f30008f7c20ca972c18e7d6f3bf8b0857409caf7fad60ecbd186e83b45fa1b7a1
Description
FreeSpec is a framework for the Coq proof assistant which allows to implement and specify impure computations. This is the core of the framework: it provides the foundation of the formalism, based on the freer monad, the reasoning theory and tactics to automate the reasoning.
Tags
date:2021-03-01 keyword:effects keyword:freer keyword:program logic category:Mathematics/Category Theory logpath:FreeSpec.CorePublished: 04 Mar 2021
Dependencies (4)
-
coq-ext-lib
>= "0.11.2" -
coq
>= "8.12" & < "8.14~" -
dune
>= "2.5" - ocaml
Dev Dependencies
None
Used by (2)
Conflicts
None
On This Page