Skip to content

Commit

Permalink
Add project info to README
Browse files Browse the repository at this point in the history
  • Loading branch information
4ever2 committed Jul 10, 2024
1 parent 0ace12a commit d2d91c4
Showing 1 changed file with 27 additions and 1 deletion.
28 changes: 27 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,29 @@
# coq-elm-extraction
# Coq Elm Extraction
[![Build](https://github.com/AU-COBRA/coq-elm-extraction/actions/workflows/build.yml/badge.svg)](https://github.com/AU-COBRA/coq-elm-extraction/actions/workflows/build.yml)
[![GitHub](https://img.shields.io/github/license/AU-COBRA/coq-elm-extraction)](https://github.com/AU-COBRA/coq-elm-extraction/blob/master/LICENSE)
[![Documentation](https://img.shields.io/github/deployments/au-cobra/coq-elm-extraction/github-pages?label=docs)](https://au-cobra.github.io/coq-elm-extraction/)


A framework for extracting Coq programs to Elm.

## Meta

- Author(s):
- Danil Annenkov (initial)
- Mikkel Milo (initial)
- Jakob Botsch Nielsen (initial)
- Bas Spitters (initial)
- Eske Hoy Nielsen
- License: [MIT](LICENSE)
- Compatible Coq versions: 8.17 or later
- Additional dependencies: MetaCoq
- Coq namespace: `ElmExtraction`
- Related publication(s):
- [Extracting functional programs from Coq, in Coq](https://arxiv.org/abs/2108.02995) doi:[10.1017/S0956796822000077](https://doi.org/10.1017/S0956796822000077)
- ["Extending MetaCoq Erasure: Extraction to Rust and Elm"](https://dannenkov.me/papers/extraction-rust-elm-coq-workshop2021.pdf)
- ["Extracting Smart Contracts Tested and Verified in Coq"](https://arxiv.org/abs/2012.09138) doi:[10.1145/3437992.3439934](https://doi.org/10.1145/3437992.3439934)


## Documentation

For documentation see [ConCert](https://github.com/AU-COBRA/ConCert)

0 comments on commit d2d91c4

Please sign in to comment.