Stream: Miscellaneous

Topic: Papers that reference Coq code inline


view this post on Zulip Karl Palmskog (Dec 09 2021 at 11:33):

Are there any good examples of research papers that reference Coq code inline? Doesn't necessarily mean a link to a GitHub repo, just an unambiguous reference to where the "Coq equivalent" of some concept explained in a paper can be found.

view this post on Zulip Yannick Forster (Dec 09 2021 at 16:42):

I'm not sure I'm getting the question wrong, but I've been using the coqtheorempackage extensively in the last years (github.com/yforster/coqtheorem). It gives an easy way to link definitions, lemmas, and theorems to coqdoc-generated code, see for example https://doi.org/10.4230/LIPIcs.CSL.2021.21

view this post on Zulip Yannick Forster (Dec 09 2021 at 16:44):

image.png

view this post on Zulip Yannick Forster (Dec 09 2021 at 16:44):

My cursor was not included in the screenshot, but it's right over Lemma 1

view this post on Zulip Karl Palmskog (Dec 09 2021 at 16:52):

thanks, that's approximately what I was looking for

view this post on Zulip Dan Frumin (Dec 14 2021 at 22:06):

Examples from UniMath: https://arxiv.org/pdf/1705.04296.pdf and https://arxiv.org/pdf/1903.01152.pdf


Last updated: Aug 19 2022 at 20:03 UTC