Ana de Almeida Borges (Oct 06 2021 at 18:04): Ana de Almeida Borges (Oct 06 2021 at 18:04):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.
Karl Palmskog (Oct 06 2021 at 18:11):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
Karl Palmskog (Oct 06 2021 at 18:12):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
Karl Palmskog (Oct 06 2021 at 18:14):the top journal for proof assistant based formalizations in general is arguably JAR: https://www.springer.com/journal/10817
Karl Palmskog (Oct 06 2021 at 18:16):since CPP just had a deadline, the next conference venue of choice might be ITP: https://itp-conference.github.io
Ana de Almeida Borges (Oct 06 2021 at 18:19):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?
Ana de Almeida Borges (Oct 06 2021 at 18:21):Thank you very much for the links!
Karl Palmskog (Oct 06 2021 at 18:21):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.
Karl Palmskog (Oct 06 2021 at 18:26):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.
Ana de Almeida Borges (Oct 06 2021 at 18:30):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.
Karl Palmskog (Oct 06 2021 at 18:33):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.
Karl Palmskog (Oct 06 2021 at 18:33):for example, FLoC 2022 will have lots of workshops to choose from.
Karl Palmskog (Oct 06 2021 at 18:36):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.
Ana de Almeida Borges (Oct 06 2021 at 18:41):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.
Ana de Almeida Borges (Oct 06 2021 at 18:42):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.
Karl Palmskog (Oct 06 2021 at 18:43):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: Apr 19 2024 at 18:01 UTC