io
Effect library
A Coq library that enables the use of effects in functional programming with references to a global state
A library for effects in Coq.
64 stars
6 watching
4 forks
Language: Coq
last commit: over 2 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| coq-io/system | A library of Unix effects implemented in the Coq functional programming language | 23 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |
 coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
 mattam82/coq-equations | A package for defining functions in Coq using dependent types and pattern-matching. | 223 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 67 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
 deepspec/interactiontrees | A library for representing recursive and impure programs in the Coq proof assistant language. | 206 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |