Verification of Implementations of Distributed Systems Under Churn (CoqPL 2017 - The Third International Workshop on Coq for Programming Languages)

Sun 15 - Sat 21 January 2017

Who

Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog

Track

CoqPL 2017

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 21 Jan 2017 17:15 - 17:40 at Auditorium - Afternoon Session Chair(s): Matthieu Sozeau

File attachments

Abstract (CoqPL_2017_paper_12.pdf)	193KiB

Ryan Doenges

University of Washington

United States

James R. Wilcox

University of Washington

United States

Doug Woos

University of Washington

United States

Zachary Tatlock

University of Washington, Seattle

United States

Karl Palmskog

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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