Program - POPL 2017

Detailed Table Session Timeline Detailed Timeline

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

You're viewing the program in a time zone which is different from your device's time zone change time zone

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

09:00 - 10:00	Opening SessionCoqPL at Auditorium Chair(s): Emilio Jesús Gallego Arias MINES ParisTech

09:00 60m Talk		Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL I: Robbert Krebbers Delft University of Technology, Netherlands

10:30 - 12:10	Morning SessionCoqPL at Auditorium Chair(s): Alan Schmitt Inria

10:30 25m Talk		IxFree: Step-Indexed Logical Relations in Coq CoqPL Piotr Polesiuk File Attached
10:55 25m Talk		Logical Relations in Iris CoqPL Amin Timany imec - Distrinet, KU Leuven, Robbert Krebbers Delft University of Technology, Netherlands, Lars Birkedal Aarhus University File Attached
11:20 25m Talk		Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL Edwin Westbrook Galois, Inc., Gregory Malecha UCSD File Attached
11:45 25m Talk		ppsimpl: a reflexive Coq tactic for canonising goals CoqPL Frédéric Besson File Attached

14:00 - 15:30	Midday SessionCoqPL at Auditorium Chair(s): Sandrine Blazy University of Rennes 1, France

14:00 60m Talk		Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL I: Nicolas Tabareau Inria, France
15:00 30m Demonstration		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria

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

19:00 - 21:00	Social EventCoqPL at CoqPL-social-event-room

19:00 2h Social Event		CoqPL Social Event CoqPL

CoqPL 2017 Program

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

CoqPL 2017 Program

Switch Program View

Program Display Configuration

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Get Calendar (iCal)

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