The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

(cross-post from https://coq.discourse.group/t/plv-has-a-new-blog/925; 
consider following up there) 

Hi all,

We just launched our new blog at https://plv.csail.mit.edu/blog/! 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 
https://plv.csail.mit.edu/blog/pages/how-to.html:

- Some Coq tips:

  * How to write a type-safe unwrap (aka fromJust): Tips and tricks for 
writing functions that take proofs as arguments.
    https://plv.csail.mit.edu/blog/unwrapping-options.html
    
  * Computing with opaque proofs: Computations with dependent types often get 
stuck on rewrites that use opaque lemmas. When the corresponding equality is 
decidable, these lemmas don't need to be made transparent to unblock 
computation.
    https://plv.csail.mit.edu/blog/computing-with-opaque-proofs.html

- One experience report about preparing a talk for a virtual conference, 
since multiple people at PLDI asked us about our closed captions:

  * Recording and editing a talk for an online conference: A step-by-step 
guide on using guvcview, ffmpeg, and aegisub to assemble a talk video.
    https://plv.csail.mit.edu/blog/recording-a-conference-talk.html

- … and one tutorial, a guest post (!) written by Tej:

  * A brief introduction to Iris: Introduction to concurrency reasoning in 
the Iris framework, using a bank as an example program.
    https://plv.csail.mit.edu/blog/iris-intro.html

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 :)
Clément.

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!