Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationCPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022
EditorsAndrei Popescu, Steve Zdancewic
PublisherAssociation for Computing Machinery, Inc
Pages2-11
Number of pages10
ISBN (Electronic)9781450391825
DOIs
StatePublished - Jan 17 2022
Event11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022 - Philadelphia, United States
Duration: Jan 17 2022Jan 18 2022

Publication series

NameCPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022

Conference

Conference11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022
Country/TerritoryUnited States
CityPhiladelphia
Period1/17/221/18/22

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Software

Keywords

  • nil
  • None

Fingerprint

Dive into the research topics of 'Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)'. Together they form a unique fingerprint.

Cite this