@inproceedings{acd20d7edaba440fbf57efc8dd3c21f1,
title = "Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)",
abstract = "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.",
keywords = "None, nil",
author = "Appel, \{Andrew W.\}",
note = "Publisher Copyright: {\textcopyright} 2022 Owner/Author.; 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022 ; Conference date: 17-01-2022 Through 18-01-2022",
year = "2022",
month = jan,
day = "11",
doi = "10.1145/3497775.3503951",
language = "English (US)",
series = "CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022",
publisher = "Association for Computing Machinery, Inc",
pages = "2--11",
editor = "Andrei Popescu and Steve Zdancewic",
booktitle = "CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022",
}