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:39:33 -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-oi1-f169.google.com
- Ironport-phdr: 9a23:oGyiVxHg9gW++Vm8oPHBGZ1GYnF86YWxBRYc798ds5kLTJ7zpMmwAkXT6L1XgUPTWs2DsrQY0rCQ6v+/Ej1eqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAnctMsbjYRmJ6sw1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2vpxN9w4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDoxykCgm2BePvzSJDi2Py3a0kyeshCx/J3Q09FN8JtXTUqc/6NKMMUe+v1qnH0y7OYO1Q2Tfy8oTIbwwuoeqRUr5qb8Xe1FQvGhrDg16Np4LlODaV2f4Ms2id9+dgTfivi2kgqwF/vDevwMgsiojPho0L1F/E7yR5wIA6JdGiT057e9GkHINftyGbK4t2Qt4iTHpytCkmzb0GvIa3fC4NyJUp3x7fdueIc4yJ4hL4VOaePy14hGl/dL2jgBay9E6twfD/WMmsyFtGsDZJn93Wun0O1xHf8NWLR/p/80u7xDqC1gTe5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3zjKCMd0Uk/vGk6+PmYrn7v5OcOZJ4hwD6P6g0lcy/BuM4MgcKX2eF4+izyLrj/UjhTLVLiP05jLXZvYjEKcgHoqO1GQxY34Y55xqiDjqr0s4UkWQGIV9BYB6HipLmO1DKIPD2F/e/hFGsnS9ux/DDJLLhBovNIWLZkLj/Zrty9UhcyAUpwdBC+51UEawOLOjtVUDsqdzUFgU5PBCsw+b7FNV90ZsTVn6IAq+AKa/drVuI5v80LOSXf48UuDP9K+A/6PL0jH85n0Udfaiz0pcNZnC4BKcuH0LMan31x9wFDG0ivwwkTeWshkfRfyRUYiOXVrg94XkSDJyvF4rRDtSohbWFwi6hE7VbYG8AF1uXHTHle5jSCKREUz6bPsI0ym9MbrOmUYJ0jUjy5j+/8KJuK6/vwgNdrYjqjYQn6uvc0ww57jAyAsiAgTnUEjNE21gQTjpz55hR5ExwzlDZj/p9iv1cUNtSvrZHC1lrc5HbyON+Bpb5XQeTJo7YGmbjec2vBHQKdvx0xtYPZ0hnHND70kLO2SXsHrQOm/qGCIFmq68=
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.