benediktahrens / Monads
Licence: unlicense
Coq code accompanying several articles on semantics of functional programming languages
Labels
Projects that are alternatives of or similar to Monads
Autosubst
Automation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (+144.44%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+6144.44%)
Mutual labels: coq
Cufp 2015 Tutorial
An introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (+0%)
Mutual labels: coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+7455.56%)
Mutual labels: coq
Micro Policies Coq
Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (+100%)
Mutual labels: coq
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+5411.11%)
Mutual labels: coq
Finset
A Coq library for extensional finite sets and comprehension
Stars: ✭ 6 (-33.33%)
Mutual labels: coq
Jscoq
A port of Coq to Javascript -- Run Coq in your Browser
Stars: ✭ 380 (+4122.22%)
Mutual labels: coq
Fiat Crypto
Cryptographic Primitive Code Generation by Fiat
Stars: ✭ 359 (+3888.89%)
Mutual labels: coq
COMPILATION
This Coq theory compiles under Coq 8.3pl5, available from https://coq.inria.fr/distrib/V8.3pl5/files/ . Earlier patch levels should also work; I have tested with 8.3pl2.
Create a Makefile by calling
$ coq_makefile -f Make > Makefile
and compile by calling
$ make
WARNING : The compilation of some of the files consumes up to 2GB of memory. Make sure you dispose of sufficient reserves of ram before compiling the code.
WORK WITH THE CODE
Call coqide as follows from the root of the library:
$ coqide -R . CatSem
CONTENT
Read the file "./DESCRIPTION" for a description of the content of each file.
BRANCHES
Each branch below, printed in boldface, corresponds to an article, printed in italic.
- JFR: Initial Semantics for higher-order typed syntax in Coq
- MSCS: Modules over relative monads for syntax and semantics
- REDUCTION_RULES: Initial Semantics for Reduction Rules
All the articles are also available from my webpage.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].