[pl-seminar] Talk today

[Calvin Smith <cjsmith@xxxxxxxxxxx>]

Howdy all,

Stephen is presenting at the PL seminar today at noon in cs4310. See below for the talk abstract:

The Coq theorem prover is a powerful tool for verifying that program specifications satisfy various properties. In this presentation, I will introduce Coq using an example of verifying insertion sort. Then, I will illustrate how Coq has been used to verify C programs by establishing correspondences between C structures and Coq structures.  This demonstrates a very common technique in Coq, which has also been used to verify properties of LLVM bitcode and of operating systems.

Thanks,

Calvin