package coq-simple-io

  1. Overview
  2. No Docs
IO monad for Coq

Install

Dune Dependency

github.com Edit opam file Versions (14)

Authors

  1. L
    Li-yao Xia
  2. Y
    Yishuai Li

Maintainers

  1. L
    Li-yao Xia <lysxia@gmail.com>

Sources

1.8.0.tar.gz
sha512=0210b900855874071f9862d9a72e97561ed1568ebaab850889a05b2602c0cc03a0b4f201e6ae1f6ed4d18182c59c9f6a104e868710719c0c88583dab681ee4da

Description

This library provides tools to implement IO programs directly in Coq, in a similar style to Haskell. Facilities for formal verification are not included.

IO is defined as a parameter with a purely functional interface in Coq, to be extracted to OCaml. Some wrappers for the basic types and functions in the OCaml Stdlib module are provided. Users are free to define their own APIs on top of this IO type.

Tags

date:2022-09-13 logpath:SimpleIO keyword:extraction keyword:effects

Published: 14 Sep 2022

Dependencies (5)

  1. cppo build & >= "1.6.8"
  2. coq-ext-lib >= "0.10.0"
  3. coq >= "8.11" & < "8.20~"
  4. ocamlfind
  5. ocaml >= "4.08.0"

Dev Dependencies (1)

  1. ocamlbuild with-test & >= "0.9.0"

Conflicts

None