CertiCoq: A verified compiler for Coq (CoqPL 2017 - The Third International Workshop on Coq for Programming Languages) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, Matthew Weaver

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

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

When

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

File attachments

Abstract (CoqPL_2017_paper_3.pdf)	134KiB

Abhishek Anand

Andrew W. Appel

Princeton

Greg Morrisett

Cornell University

Zoe Paraskevopoulou

Princeton University, USA

United States

Randy Pollack

Harvard University

Olivier Savary Belanger

Princeton University

Canada

Matthieu Sozeau

Inria

France

Matthew Weaver

Princeton University

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

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