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
- 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.
-
… 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
- A brief introduction to Iris: Introduction to concurrency reasoning in the Iris framework, using a bank as an example program.
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!
