PLV has a new blog!

Hi all,

We just launched our new blog at! Multiple members of our lab were looking for an informal way to share research updates, Coq tips, tutorials, and new ideas, so we set one up.

We’re launching with a few posts already, plus a small intro page at :

Happy reading! And please get in touch if you’d like to write a guest post or follow up on one of the things we wrote :slight_smile:

PS: We’re also using this blog to try out a new toolkit that I wrote over the last year to facilitate authoring and browsing Coq-heavy documents (I talked about it to some of you in the past). I’ll write more about this soon, but I’m hoping to submit a short paper about it in the near future, so a proper announcement and public release will have to wait until the paper is out of review. In the meantime, if you’re interested and would like to read a draft or get access to the repo, please send me an email or catch me at the Coq workshop!



Discourse takes the : at the end as part of the link, so it 404s; to fix the URL, take the final : back out. :white_check_mark: