Coq-community is looking for looking for volunteer maintainers of the Coq Library of Complexity Theory project.
As per the name, the library contains definitions and results related to computational complexity formalized in Coq, including NP-hardness, the Cook-Levin Theorem, NP-completeness results, and resource analysis of call-by-value lambda-calculus and Turing machines. Results from the library have been the subject of four research publications. The library builds on the Coq Library of Undecidability Proofs.
The project has been unmaintained since November 2022 and currently supports Coq 8.16. An initial task for a new maintainer would be to ensure that the latest released version of Coq (currently 8.18.0) is supported by the project.
To volunteer, please respond to this GitHub issue with brief motivation and summary of relevant experience for becoming a library maintainer. It is appreciated if volunteers also indicate their plans for the library which, e.g., could range from maintaining compatibility with the latest released version of Coq to making substantial additions.
When needed, maintainers can expect assistance and helpful advice on practical tasks such as continuous integration and packaging from experienced Coq-community contributors, many of whom are members of the Coq Team.