<p>This is a soft question aimed at understanding whether there is any value to publishing formally verified <em>libraries</em>. I have formally verified (in Coq) implementations of:</p>

<ol>
<li><a href="https://github.com/bollu/diffgeo" rel="nofollow noreferrer">synthetic differential geometry</a></li>
<li><a href="https://github.com/bollu/scev-coq" rel="nofollow noreferrer">Chains of recurrences</a></li>
</ol>

<p>Are these of interest in terms of publication anywhere? what is the bar for "what can be formally verified and published"? Are these even "put on on Arxiv" worthy? In general, what's the boundary that separates "routine proof" from "publishable proof"?</p>

<p>Thanks a lot!</p>

CC BY-SA 4.0
2020-02-12T15:33:51.673Z
Places like CPP (certified proofs and programs) are certainly interested in experience reports for formalizing mathematics. Looking at the program from this last year many of the submissions were about this (https://popl20.sigplan.org/home/CPP-2020#event-overview). I do not think that the sdg formalization you put is quite at the stage to be submitted though, since it is doesn't really contain any theorems, just statements of axioms.
daniel gratzer
CC BY-SA 4.0
2020-02-12T15:42:15.273Z
Thanks! I'd be interested in a spectrum of conferences: CPP looks far too demanding in terms of the scale of the proofs I'm interested in formalizing.
Siddharth Bhat
CC BY-SA 4.0
2020-02-12T15:42:45.090Z
Regarding synthetic differential geometry: I agree. That went on hiatus after I found out that building models for SDG is quite hard --- I was wondering if it was a good fit for CPP
Siddharth Bhat
CC BY-SA 4.0
2020-02-12T18:24:28.107Z
There are several, see e.g. [here](https://ncatlab.org/nlab/show/Archive+of+Formal+Proofs).
Martin Berger
<coq><automated-theorem-proving><formal-methods>
Journals or conferences to submit formally verified libraries?
Siddharth Bhat
# Journals or conferences to submit formally verified libraries?

(Asked by: username_0 on 2020-02-12)

This is a soft question aimed at understanding whether there is any value to publishing formally verified *libraries*. I have formally verified (in Coq) implementations of:

1. [synthetic differential geometry](https://github.com/bollu/diffgeo)
2. [Chains of recurrences](https://github.com/bollu/scev-coq)

Are these of interest in terms of publication anywhere? what is the bar for "what can be formally verified and published"? Are these even "put on on Arxiv" worthy? In general, what's the boundary that separates "routine proof" from "publishable proof"?

Thanks a lot!

**Tags:** coq, automated-theorem-proving, formal-methods

> **Comments:**
> **username_1**: Places like CPP (certified proofs and programs) are certainly interested in experience reports for formalizing mathematics. Looking at the program from this last year many of the submissions were about this (https://popl20.sigplan.org/home/CPP-2020#event-overview). I do not think that the sdg formalization you put is quite at the stage to be submitted though, since it is doesn't really contain any theorems, just statements of axioms.  
> **username_0**: Thanks! I'd be interested in a spectrum of conferences: CPP looks far too demanding in terms of the scale of the proofs I'm interested in formalizing.  
> **username_0**: Regarding synthetic differential geometry: I agree. That went on hiatus after I found out that building models for SDG is quite hard --- I was wondering if it was a good fit for CPP  
> **username_2**: There are several, see e.g. [here](https://ncatlab.org/nlab/show/Archive+of+Formal+Proofs).  

---

## 0 answers

