Stream: Coq users

Topic: Template repo for program verification

Karl Palmskog (Sep 05 2020 at 09:36):

Inspired by Emilio's template repo for plugins, I created a template repo for Coq program verification that showcases a lot of recent features added by the community, such as CI, using Dune, etc.

• Writeup/summary: https://coq.discourse.group/t/a-template-for-organizing-a-coq-program-verification-project/1039
• Repo: https://github.com/palmskog/coq-program-verification-template

Théo Zimmermann (Sep 05 2020 at 09:57):

@Karl Palmskog Cross-posting is not necessary: all Discourse posts are already relayed on Zulip.

Karl Palmskog (Sep 05 2020 at 09:58):

well, I'm never personally going to have any casual conversation in a Zulip-Discourse relay topic, and Discourse itself is terrible for casual questions/chat.

Karl Palmskog (Sep 05 2020 at 10:03):

also, the repo link is absent from the relay post

Karl Palmskog (Sep 08 2020 at 13:20):

I guess my choice of program verification framework (VST) was timely, since a book describing it was just released to the public: https://www.cs.princeton.edu/~appel/papers/plcc.pdf

Last updated: Oct 01 2023 at 19:01 UTC