Proposal to add SyDRec

[palmskog]

Move a project to coq-community

Project name: SyDRec

Initial author(s): Simon Robillard

Current URL: https://github.com/simonr89/SyDRec

Kind: OCaml plugin

License: CeCILL-C

Description: Plugin that allows generating catamorphisms and accompanying fusion lemmas from inductive types. This provides support for the "derivation-style" program development advocated by Richard Bird and others (see the book Algebra of Programming). The theory and implementation is described in the paper Catamorphism Generation and Fusion Using Coq.

Status: Appears unmaintained. Last supported version of Coq is 8.4.

New maintainer: looking for a volunteer