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

deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
Talk
deepspec-2018-papers16:15 - 16:20
Talk
deepspec-2018-papers16:20 - 16:25
Talk
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
Talk
deepspec-2018-papers16:30 - 16:35
Talk
deepspec-2018-papers16:35 - 16:40
Talk
deepspec-2018-papers16:40 - 16:45
Talk
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Talk
Sam GruetterMassachusetts Institute of Technology