Provable Optimizations in Coq

Proving that optimization passes are correct with the formal verification assistant Coq.

These views do not in any way represent those of NVIDIA or any other organization or institution that I am professionally associated with. These views are entirely my own.

What is Coq?

It’s a programming language to help the programmer prove things.

Written on Oct 6th, 2022