package coq-freespec-ffi

  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. It can be used with coqffi to write certified software.

Tags

date:2021-03-01 keyword:foreign function interface category:Miscellaneous/Coq Extensions logpath:FreeSpec.FFI

Published: 04 Mar 2021

Dependencies (6)

  1. coq-simple-io >= "1.0" & < "2.0~"
  2. coq-coqffi = "1.0.0~beta5"
  3. coq-freespec-core = "0.3"
  4. coq >= "8.12" & < "8.14~"
  5. dune >= "2.5"
  6. ocaml

Dev Dependencies

None

Conflicts

None