system
Unix effects library
A library of Unix effects implemented in the Coq functional programming language
Library of Unix effects for Coq.
23 stars
3 watching
1 forks
Language: Coq
last commit: about 5 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| coq-io/io | A Coq library that enables the use of effects in functional programming with references to a global state | 64 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 167 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
 coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 heades/system-f-coq | An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
| coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 45 |
| 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 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 515 |
 mattam82/coq-equations | A package for defining functions in Coq using dependent types and pattern-matching. | 223 |