Tue 19 Jun 2018 16:40 - 16:45 at Columbus Ballroom B - Lightning Talks

Establishing that two programs are contextually equivalent is hard, yet essential for reasoning about semantics preserving program transformations such as compiler optimizations. The Vellvm project aims to use Coq to formalize and reason about LLVM program transformations and as part of this project we are using a variant of Levy’s call-by-push-value language. I will talk about how we establish the soundness of an equational theory for call-by-push-value and about how we used our equational theory to significantly simplify the verification of classic optimizations.

Tue 19 Jun

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