package coq-freespec-core

  1. Overview
  2. No Docs
A framework for implementing and certifying impure computations in Coq

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. T
    Thomas Letan
  2. Y
    Yann Régis-Gianas

Maintainers

  1. T
    Thomas Letan <lthms@soap.coffee>

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.Core

Published: 04 Mar 2021

Dependencies (4)

  1. coq-ext-lib >= "0.11.2"
  2. coq >= "8.12" & < "8.14~"
  3. dune >= "2.5"
  4. ocaml

Dev Dependencies

None

Conflicts

None