|
Comments
POPL and CoqPL 2016
POPL 2016 was just held a few weeks ago in Saint Petersburg, Florida, bringing together many researchers in programming languages to learn about the latest developments in the field. As usual, it was an exciting event for the Coq community. Early in the week, Robert Rand and I led an introductory Coq tutorial. Later, there was a special meeting to announce DeepSpec, an ambitious research effort to develop and integrate several verified software components, many of which use Coq. Near the end, Xavier Leroy received an award for the most influential POPL paper of 2006, for Formal Verification of a Compiler Back-end, where he introduced the CompCert verified C compiler.
Besides all these events, this year also featured the second edition of the CoqPL workshop. Its main attraction may have been the release of the long-awaited Coq 8.5. Matthieu Sozeau and Maxime Dénès gave a detailed presentation of its main new features, which include asynchronous proof checking and editing, universe polymorphism, and a new tactic engine. Congratulations to the Coq team for the great work!
Another fun talk was by Clément Pit-Claudel, where he announced company-coq, a set of Proof General extensions brings many nice editing features for Coq code in Emacs. These include: automatically prettifying code (for instance, replacing forall by ∀), auto-completion, code folding, and improved error messages, among many others. If you work with Coq under Emacs, you should definitely give it a try!