search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to add RelationExtraction #25

Open palmskog opened 5 years ago

palmskog commented 5 years ago

Move a project to coq-community

Project name: RelationExtraction

Initial author(s): Catherine Dubois, David Delahaye, and Pierre-Nicolas Tollitte

Current URLs: https://github.com/coq-contribs/relation-extraction https://github.com/picnic/RelationExtraction https://github.com/herbelin/RelationExtraction

Kind: OCaml plugin

License: GPL3

Description: A plugin for generating functions from inductive types which make this possible. The functions can either be functions inside Coq or functions in an extraction language, such as OCaml. The underlying theory and implementation of the plugin is described in the paper Producing Certified Functional Code from Inductive Specifications.

Status: Currently maintained by Coq devs in Coq-contribs

New maintainer: looking for a volunteer

palmskog commented 5 years ago

I'm uncertain whether the functionality of the plugin is superceded by related efforts such as Equations, but the customized extraction functionality could be instructive to plugin writers.

herbelin commented 4 years ago

@cathdubois and I worked on an upgrade of relation-extraction based on @picnic's version. The current status is that it compiles for 8.10.

As far as I understand the projects of @cathdubois, there is no need to port the version currently at http://github.com/coq-contribs/relation-extraction.

herbelin commented 4 years ago

I now ported my fork of @picnic's version to v8.12.