PLDI 2018 (series) / DeepSpec 2018 (series) / DeepSpec 2018 /
A Formal Equational Theory for Call-By-Push-Value
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 JunDisplayed time zone: Eastern Time (US & Canada) change
Tue 19 Jun
Displayed time zone: Eastern Time (US & Canada) change
16:10 - 17:35 | |||
16:10 5mTalk | 5-minute Lightning Talks DeepSpec | ||
16:15 5mTalk | Simplicity for Smart Contracts DeepSpec | ||
16:20 5mTalk | Machine-Verified Machine Learning DeepSpec Gordon Stewart Ohio University | ||
16:25 5mTalk | Verification of Union-Find in C DeepSpec | ||
16:30 5mTalk | Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats DeepSpec Clément Pit-Claudel MIT CSAIL | ||
16:35 5mTalk | LLVM's IR and Call-By-Push-Value Lambda Calculus DeepSpec | ||
16:40 5mTalk | A Formal Equational Theory for Call-By-Push-Value DeepSpec Christine Rizkallah The University of Melbourne | ||
16:45 5mTalk | Serializability for Distributed Protocols DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA | ||
16:50 5mTalk | A Quick Hack to ask any SMT Solver if my Coq Goal is True DeepSpec Samuel Gruetter Massachusetts Institute of Technology | ||
