Synthetic topology in HoTT for probabilistic programming (CoqPL 2017 - The Third International Workshop on Coq for Programming Languages) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Florian Faissole, Bas Spitters

Track

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

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

When

Sat 21 Jan 2017 16:00 - 16:25 at Auditorium - Afternoon Session Chair(s): Matthieu Sozeau

File attachments

Abstract (CoqPL_2017_paper_4.pdf)	175KiB

Florian Faissole

Bas Spitters

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

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

Session Program

Sat 21 Jan
Times are displayed in time zone: (GMT+01:00) 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 Florian Faissole, Bas Spitters 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 Nicolas Magaud File Attached