search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
189 stars 48 forks source link

Add the libraries for undecidability and first-order logic to the Platform #386

Open palmskog opened 11 months ago

palmskog commented 11 months ago

Coq Library of Undecidability Proofs is a collection of definitions and results related to computability, not least the halting problem. For example, it allows Coq users to prove that some property is undecidable. The library was recently relicensed under the reusability-friendly MPL-2.0 license.

Coq Library for First-Order Logic is a library containing syntax, semantics and proof systems of first-order logic, building on the undecidability library. This library was recently relicensed under the permissive MIT license, a license known for making extensive reuse possible.

Since these two libraries formalize important basic computer science concepts that are not available in the Coq standard library and are not provided by other Platform packages (other than as isolated small fragments), I propose that these two libraries are included in the Platform. For example, if the community is aware of this FOL formalization, other FOL formalizations can be proved equivalent.

Maintainers of these two libraries I have interacted with include @yforster @dominik-kirst @dmxlarchey @mrhaandi

yforster commented 11 months ago

Thanks for bringing this up Karl, I'm in favour of including both!

I just prepared for an opam release compatible with 8.18 for coq-library-undecidability, @dominik-kirst and @JoJoDeveloping will soon do the same for coq-library-fol.

In the line of basic computer science concepts there is also https://github.com/uds-psl/coq-library-complexity with the Cook-Levin theorem and a time equivalence proof for Turing machines and lambda-calculus, but it's (probably) forever stuck on 8.16 due to a lack of maintainers.

yforster commented 11 months ago

I've filed https://github.com/coq-community/manifesto/issues/150 for coq-library-complexity to look for a new maintainer, maybe we get lucky :)

yforster commented 9 months ago

There is a release for coq-library-fol now. Is there anything else we need to do for both libraries to be included in the platform? CC @dominik-kirst

palmskog commented 9 months ago

From my perspective, everything technically required is there, hopefully we can hear from the editorial board on a decision soon akin to here, cc @ybertot

I also hope we can get https://github.com/coq/platform/issues/344 resolved, since coq-library-undecidability depends on it.