Andrew W. Appel

Coq’s vibrant ecosystem for verification engineering (invited talk)

2022

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 …