POPL 2017
Sun 15 - Sat 21 January 2017
Sat 21 Jan 2017 17:40 - 18:05 at Auditorium - Afternoon Session Chair(s): Matthieu Sozeau
Abstract (CoqPL_2017_paper_7.pdf)140KiB

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:05: Afternoon SessionCoqPL at Auditorium
Chair(s): Matthieu SozeauInria
16:00 - 16:25
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
File Attached
16:25 - 16:50
Talk
CertiCoq: A verified compiler for Coq
CoqPL
Abhishek Anand, Andrew AppelPrinceton, Greg MorrisettCornell University, Zoe ParaskevopoulouPrinceton University, USA, Randy PollackHarvard University, Olivier Savary BelangerPrinceton University, Matthieu SozeauInria, Matthew WeaverPrinceton University
File Attached
16:50 - 17:15
Talk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
CoqPL
Izumi AsakuraTokyo Institute of Technology, Japan, Hidehiko MasuharaTokyo Institute of Technology, Tomoyuki AotaniTokyo Institute of Technology
File Attached
17:15 - 17:40
Talk
Verification of Implementations of Distributed Systems Under Churn
CoqPL
Ryan DoengesUniversity of Washington, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Karl Palmskog
File Attached
17:40 - 18:05
Talk
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL
File Attached