coq-to-ocaml-to-js
Code generator
Generates safe and fast JavaScript code from mathematical proofs using Coq, OCaml, BuckleScript, Rollup, Terser, and Closure Compiler
Proof of concept to generate safe and fast JavaScript
24 stars
2 watching
2 forks
Language: JavaScript
last commit: about 4 years agobucklescriptcoqjavascriptocamlproof
Related projects:
| Repository | Description | Stars |
|---|---|---|
 formal-land/coq-of-ocaml | Transforms OCaml code into formal, verifiable Coq code to prove complex properties | 255 |
 klakplok/goji | Generates OCaml bindings from high-level descriptions of JavaScript libraries | 44 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 xavierleroy/coq2html | Generates HTML documentation from Coq source files by folding proof scripts and producing auxiliary CSS and JavaScript files | 30 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 lexifi/gen_js_api | Generates OCaml bindings for JavaScript libraries | 175 |
 routineco/ocaml-nanoid | Generates unique, secure strings for use in applications. | 20 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 ocaml-ppx/ppx_deriving | A library simplifying type-driven code generation in OCaml | 469 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 senchalabs/jsduck | Generates documentation for JavaScript code using Markdown and infers information from the code itself. | 1,503 |
 impermeable/coq-waterproof | Helps write formal proofs in a more readable format | 33 |
| ocaml-ppx/ppx_deriving_yojson | A tool that generates JSON serialization and deserialization functions for OCaml types | 157 |