Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof engineering survey paper published

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof engineering survey paper published


Chronological Thread 
  • From: Mario Alvarez <mmalvare AT eng.ucsd.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proof engineering survey paper published
  • Date: Thu, 5 Sep 2019 13:43:30 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mmalvare AT eng.ucsd.edu; spf=Pass smtp.mailfrom=mmalvare AT eng.ucsd.edu; spf=None smtp.helo=postmaster AT mail-ot1-f43.google.com
  • Ironport-phdr: 9a23:Xq20LhQJNoqQxCYymTpOFAZWJtpsv+yvbD5Q0YIujvd0So/mwa6yZh2N2/xhgRfzUJnB7Loc0qyK6vqmADNfqsff+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8Ubg4lvJqk1xxbIv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBNxw4HWYI+bOvlwcL7Dc9wGXmdORNpdWjZbD4+gc4cCDewMNvtYoYnnoFsOqAOzCw62C+P1yz9IgWL90LE+0+Q/Cw7GxhIvHtMTu3nTqdX1Mb0dUeSrzKbS1zXMcehb1in76IjHaBwhvO2DXaltfsbL10YgCh7Fg0yWpIf4MT2V0eENvHKa7+pmTe+vk3QnqwZ2ojih2MgsjIbJhoMTyl/a6yp52oc1Jdu3SEJhZt6kCpRQuzmVN4t3XsMiQ3xotz0gxrIavp67eTAGyJIgxx/Rc/yHbpOH4hbiVOaKITd3mmhleKmlixmu9kigz+vxXdS33lZStidJjMXAu3QX2xHQ6sWLUOVx8lq91TqV2A3e5OdJKl0um6XBMZ4u2Lswm4ITsUvdGi/2n137jKqMeUUl/uik8uPnYqn7qpOFOY95hQ/zPr4hmsy4BuQ4PQwOUHaB9eug073j+FX1QLRMjvIojqnUqI7WKdgfq6KjAAJY0pwv5wiiAzu6ytgVkncKIEpAeB2djojpP1/OIOr/Dfe6m1mslTJryOrCPr3/GJrNNGbMnaz/crZ75E5Q0hczwsxE551JEL0OPu/8WlLpuNzCEhA5KxC0w/rgCNhlyoweXnuPDraFP6PWrF+H/fkiI/KMZY8QoDbyMeIp5//ojX8jmF8SZ7Ol3ZUNaCPwIvMzKEKAJHHon90pEGEQvwN4Qva5pkeFVGt2bmyzWOoV4i8yEo+0RdPGQ4mpnrWb0Q+2GJIQe2tdBhaBHWq+JNbMYOsFdC/HepwpqTcDT7X0E9Z9hyHrjxfzzv9cFsSR4jcR7M6x2d56ofDYjh10+DBpXZzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPQqjvpXU8FY/P8PXwsnZ8eFkr5KTuvqUweERe+nDVarRtL8XGM0R9M1htgSOgNzR47kgRfE0C6nRbQSku7TCQ==

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




Archive powered by MHonArc 2.6.18.

Top of Page