coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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==
Congratulations! This seems like it will be quite useful to the community.How is everything else going?--MarioOn 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
- [Coq-Club] Proof engineering survey paper published, Talia Ringer, 09/05/2019
- Re: [Coq-Club] Proof engineering survey paper published, Mario Alvarez, 09/05/2019
- Re: [Coq-Club] Proof engineering survey paper published, Mario Alvarez, 09/05/2019
- Re: [Coq-Club] Proof engineering survey paper published, Arnaud Bailly, 09/06/2019
- Re: [Coq-Club] Proof engineering survey paper published, Arnaud Bailly, 09/06/2019
- Re: [Coq-Club] Proof engineering survey paper published, Talia Ringer, 09/07/2019
- Re: [Coq-Club] Proof engineering survey paper published, Arnaud Bailly, 09/07/2019
- Re: [Coq-Club] Proof engineering survey paper published, Arnaud Bailly, 09/06/2019
- Re: [Coq-Club] Proof engineering survey paper published, Mario Alvarez, 09/05/2019
- Re: [Coq-Club] Proof engineering survey paper published, Mario Alvarez, 09/05/2019
Archive powered by MHonArc 2.6.18.