Mon 17 Jan 2022 09:00 - 10:00 at Salon III - Invited Talk Chair(s): Steve Zdancewic

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.

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
Coq’s vibrant ecosystem for verification engineeringInPerson
I: Andrew W. Appel Princeton
Link to publication