I'm doing a PhD in Proof Theory, during which I proved some new constructive and fairly elementary results (in the sense that they do not depend on a lot of previous facts). I've published these on their mathematical merits. I also formalized them in Coq, partly as a Coq exercise, partly because it was fun. I plan to mention the formalizations in my thesis, but my supervisor strongly advised me to publish them somewhere as well. However I am very uncertain about that idea. I don't think the Coq formalizations are particularly ingenious on the Coq side, and the mathematical side was already published somewhere else, so where is the value?

What is your opinion on the matter? Is it worthwhile to publish such a thing? Is there a particular conference or journal for which this would be well-suited? I look forward to hearing your thoughts.

The Coq formalizations can be found on my gitlab page.

what some people do is to publish the math result and proof assistant formalization separately. This allows maximum dissemination of the results in the context of each audience. But it might also make it harder to reach top venues for both papers, since the split contributions are not as strong as they would be together

for example, it might make sense to publish something in a traditional math/logic journal and then submit the (description of the) formalization to CPP: https://popl22.sigplan.org/home/CPP-2022

the top journal for proof assistant based formalizations in general is arguably JAR: https://www.springer.com/journal/10817

since CPP just had a deadline, the next conference venue of choice might be ITP: https://itp-conference.github.io

I once opened a blank latex document fully intending to write a submission for CPP with one of these developments and then I realized there seemed to be nothing (relevant) to say. I felt like I should give a lot of context on the mathematical result, perhaps using Coq definitions instead of, uh, regular definitions, but overall it felt like I was just repeating the math paper. Is that the idea?

Thank you very much for the links!

I've only been in the CPP PC once, but what we look for are descriptions of how the formalization was done, i.e., the encoding of logics, properties, etc. Also what kind of automation was used, how much effort did it take, is it reusable, can it be connected to other libraries, how were the results validated.

if there is some interesting theoretical or practical application of a formally proved theorem that has been successfully done, this is a form of validation.

Great, that list is super helpful! I don't think these developments would score high on those parameters at all, so I guess I either add more interesting stuff or I just skip the publishing and keep them as a minor curiosity.

in my opinion, better (than not publishing at all) to at least publish the formalization in a workshop to get it rubber stamped (make sure they have a published proceedings with DOIs). Would also recommend putting the actual code on something like Zenodo. Otherwise, others may have to replicate the same work in the future.

for example, FLoC 2022 will have lots of workshops to choose from.

but probably the best practical way to get formalizations persisted is to get them included in a bigger maintained library. Unfortunately, I don't know if there are libraries like that (related to proof theory) for Coq now.

Yeah, there should be a logic library instead of many mini logic libraries. I know that other people are working on similar enough Coq developments that it would make sense to join them.

Thanks a lot for the suggestions, I didn't know about Zenodo nor FLoC, and that is precisely the kind of thing I was hoping to learn! I do agree that publishing something is better than nothing, but I feel reasonably sure that this is not CPP material. It's nice to know there are alternatives.

for example, we have encodings of FOL and PA inherited from the Gödel proof in Hydras & Co.: https://github.com/coq-community/hydra-battles

But I think they have this also at USL using different approaches: https://github.com/uds-psl/coq-library-undecidability

Last updated: Dec 06 2023 at 14:01 UTC