1
$\begingroup$

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
  2. Chains of recurrences

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!

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ 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 (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. $\endgroup$
    – daniel gratzer
    Feb 12, 2020 at 15:33
  • $\begingroup$ 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. $\endgroup$
    – Siddharth Bhat
    Feb 12, 2020 at 15:42
  • $\begingroup$ 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 $\endgroup$
    – Siddharth Bhat
    Feb 12, 2020 at 15:42
  • 1
    $\begingroup$ There are several, see e.g. here. $\endgroup$
    – Martin Berger
    Feb 12, 2020 at 18:24

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.