Stream: Coq Platform devs & users

Topic: Coq's vibrant ecosystem

Andrew Appel (Dec 16 2021 at 20:46):

The Coq Platform developers might enjoy reading this paper, especially Section 7.
https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf

Andrew W. Appel. 2022. Coq’s vibrant ecosystem for verification engineering (Invited paper).
In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), January 17–18, 2022, Philadelphia, PA, USA.
ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3497775.3503951
[Note, the doi.org link won't start working until mid-January 2022, use the princeton.edu link until then]

Enrico Tassi (Dec 17 2021 at 06:37):

Thanks!

Théo Zimmermann (Dec 17 2021 at 10:21):

This is great! Thanks a lot for writing this piece. Is it still time to report typos?

Gaëtan Gilbert (Dec 17 2021 at 10:48):

could be of interest outside the platform stream

Andrew Appel (Dec 17 2021 at 13:14):

Maybe if you report a typo within the next 2 hours . . .
And yes, it should be of interest outside the platform stream, that's why I'm publishing it in CPP.

Alix Trieu (Dec 17 2021 at 13:29):

Andrew Appel said:

Maybe if you report a typo within the next 2 hours . . .

I believe the C semantics used by RefinedC is called Caesium and not Caeserium (in Section 3).

Andrew Appel (Dec 17 2021 at 13:46):

Note to Theo: Thanks for the two typo reports, but one of them is not a typo. "binary tries" is correct. See also this paper:
https://arxiv.org/abs/2110.05063
Efficient Extensional Binary Tries, by A. W. Appel and X. Leroy, 2021

Note to Alix: Thanks for the typo report.

Enrico Tassi (Dec 17 2021 at 13:56):

About that paper, I see it benchmarks cbn. Not sure what it exactly mean, but the cbn user facing reduction procedure in coq is call by name, while the lazy one is (way more optimized and) call by need. Just in case.

Andrew Appel (Dec 17 2021 at 15:54):

Note: The correct title of the paper ends with "(Invited Talk)", not "(Invited Paper)". So please cite as,
Andrew W. Appel. 2022. Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk).
In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22), January 17–18, 2022, Philadelphia, PA, USA.
ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3497775.3503951

Karl Palmskog (Dec 18 2021 at 13:31):

I did some updates to https://github.com/coq-community/awesome-coq based on projects mentioned in the preprint.

Karl Palmskog (Dec 18 2021 at 18:44):

read the preprint a bit closer now, only question mark that came up for me was that the mentioned refinement from MathComp matrices to lists of lists (and then further to Clight) was seemingly done manually? I think that refinement is nowadays available near-automatically via ParamCoq+CoqEAL, but not sure when it was added there.

Bas Spitters (Dec 18 2021 at 18:50):

@Andrew Appel Thanks for the nice overview! Some quick remarks
As you know, both fiat-crypto and bedrock have been useful to construct correct C-programs.

p5. Coq's stdlib classical real numbers are now based on the constructive real numbers.
Computing with constructive real numbers is entirely practical. E.g. the work by Russell O'Connor and my work with @Robbert Krebbers
http://www.springerlink.com/content/m380454267180372/
http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

Bas Spitters (Dec 18 2021 at 18:51):

@Karl Palmskog Good point about CoqEAL. The project seems a bit stalled though...

Karl Palmskog (Dec 18 2021 at 18:53):

CoqEAL is maintained and in the Coq Platform (and recently got big additions thanks to porting of ForMath work by Yves Bertot), but I guess it may need more examples and better marketing. One approach is to use it as an incubator for MathComp-related formalization work that then gets integrated into math-comp repo proper.

Bas Spitters (Dec 19 2021 at 08:40):

@Karl Palmskog I meant that I haven't seen it used so much as I expected to see it used.

Karl Palmskog (Dec 19 2021 at 10:01):

the relatively low impact of CoqEAL may be partly due to its complex chain of dependencies (MathComp + extensions + ParamCoq), which were rarely available for the latest stable Coq version until now

Théo Zimmermann (Dec 19 2021 at 13:40):

Another reason could be that it has been nearly abandoned for many years, but it is in better shape now.

Karl Palmskog (Dec 19 2021 at 13:41):

Agree, but one recent impressive piece of work that used CoqEAL: https://github.com/math-comp/Apery

Bas Spitters (Dec 20 2021 at 10:28):

Thanks. I didn't know that it was used in Apery!

I guess the integration of param-coq with meta-coq is still waiting on an excited phd-student?

Karl Palmskog (Dec 20 2021 at 11:44):

Paramcoq was also recently used here: https://github.com/pi8027/stablesort

Unfortunately the Paramcoq to MetaCoq port may not be very publishable, and may be too complex for a master's thesis, so I have a hard time seeing it happen soon...

Bas Spitters (Dec 20 2021 at 21:02):

Thanks. That seems like a nice use case.

Karl Palmskog (Dec 21 2021 at 17:39):

Since real numbers were mentioned, Vincent gave a nice breakdown of how standard library real numbers currently work in Coq here: https://stackoverflow.com/questions/69683736/real-numbers-in-coq

Karl Palmskog (Feb 05 2022 at 23:15):

Andrew's very nice keynote talk is now up on YouTube: https://www.youtube.com/watch?v=StQ40osfQTo

Last updated: Jun 03 2023 at 05:01 UTC