The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

The publisher has requested that we do not post our own versions of this for several months, so if you would like a free copy, your best bet is to register and download it while it is still available (before September 10th). Registering is free and painless, thankfully.

Talia

On Fri, Sep 6, 2019 at 2:11 AM Arnaud Bailly <arnaud.oqube AT gmail.com> wrote:

This looks interesting. Is there a version of the paper that can be downloaded freely?

-- 

Arnaud Bailly - @dr_c0d3

On Thu, Sep 5, 2019 at 7:43 PM Mario Alvarez <mmalvare AT eng.ucsd.edu> wrote:

Sorry about accidentally replying-all here. I will be more careful in the future.

--Mario

On Thu, Sep 5, 2019, 1:39 PM Mario Alvarez <mmalvare AT eng.ucsd.edu> wrote:

Congratulations! This seems like it will be quite useful to the community.

How is everything else going?

--Mario

On Thu, Sep 5, 2019, 1:36 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi Coq-Club,

We are happy to announce the publication (on September 3, 2019) of an extensive survey of the scientific literature on proof engineering for software systems using proof assistants:

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages (FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.

The article is available for free download at the URL above until around September 10, 2019.

---

Most of the authors are Coq users, and we believe the survey can be useful to the Coq community, both as a distillation of existing knowledge and for its comparisons with other proof assistants.

If you find any errors not already documented in our errata, please report them as a GitHub issue, submit a pull request for the errata source file, or contact us directly. Omissions are also welcome, as are questions about confusing text.

The small verified regular _expression_ matcher Coq project used as a motivating example in chapter 2 of the paper is available on Github.

And of course, thank you to everyone who helped make this possible.

Talia, Karl, Ilya, Milos, and Zach