TY - GEN
T1 - Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)
AU - Appel, Andrew W.
N1 - Publisher Copyright:
© 2022 Owner/Author.
PY - 2022/1/17
Y1 - 2022/1/17
N2 - Program verification in the large is not only a matter of mechanizing a program logic to handle the semantics of your programming language. You must reason in the mathematics of your application domain - and there are many application domains, each with their own community of domain experts. So you will need to import mechanized proof theories from many domains, and they must all interoperate. Such an ecosystem is not only a matter of mathematics, it is a matter of software process engineering and social engineering. Coq's ecosystem has been maturing nicely in these senses.
AB - Program verification in the large is not only a matter of mechanizing a program logic to handle the semantics of your programming language. You must reason in the mathematics of your application domain - and there are many application domains, each with their own community of domain experts. So you will need to import mechanized proof theories from many domains, and they must all interoperate. Such an ecosystem is not only a matter of mathematics, it is a matter of software process engineering and social engineering. Coq's ecosystem has been maturing nicely in these senses.
KW - None
KW - nil
UR - http://www.scopus.com/inward/record.url?scp=85124046468&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85124046468&partnerID=8YFLogxK
U2 - 10.1145/3497775.3503951
DO - 10.1145/3497775.3503951
M3 - Conference contribution
AN - SCOPUS:85124046468
T3 - CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022
SP - 2
EP - 11
BT - CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022
A2 - Popescu, Andrei
A2 - Zdancewic, Steve
PB - Association for Computing Machinery, Inc
T2 - 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022
Y2 - 17 January 2022 through 18 January 2022
ER -