POPL 2017
Sun 15 - Sat 21 January 2017
POPL 2017 (series) / CoqPL 2017 (series) / The Third International Workshop on Coq for Programming Languages /

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

CoqPL 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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:05
Afternoon SessionCoqPL at Auditorium
Chair(s): Matthieu Sozeau Inria
16:00
25m
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
Florian Faissole , Bas Spitters
File Attached
16:25
25m
Talk
CertiCoq: A verified compiler for Coq
CoqPL
Abhishek Anand , Andrew W. Appel Princeton, Greg Morrisett Cornell University, Zoe Paraskevopoulou Princeton University, USA, Randy Pollack Harvard University, Olivier Savary Belanger Princeton University, Matthieu Sozeau Inria, Matthew Weaver Princeton University
File Attached
16:50
25m
Talk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
CoqPL
Izumi Asakura Tokyo Institute of Technology, Japan, Hidehiko Masuhara Tokyo Institute of Technology, Tomoyuki Aotani Tokyo Institute of Technology
File Attached
17:15
25m
Talk
Verification of Implementations of Distributed Systems Under Churn
CoqPL
Ryan Doenges University of Washington, James R. Wilcox University of Washington, Doug Woos University of Washington, Zachary Tatlock University of Washington, Seattle, Karl Palmskog
File Attached
17:40
25m
Talk
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL
Nicolas Magaud
File Attached

Nicolas Magaud