Watercourt A - POPL 2018

VenueOmni Hotel

Room nameWatercourt A

Floor0

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT-08:00) Tijuana, Baja California.

Use conference time zone: (GMT-08:00) Tijuana, Baja CaliforniaSelect 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 13 Jan
Displayed time zone: Tijuana, Baja California change

09:00 - 10:00	KeynoteCoqPL at Watercourt A Chair(s): Yves Bertot INRIA

09:00 60m Talk		CoqHammer: Strong Automation for Program Verification CoqPL Lukasz Czajka University of Innsbruck, Cezary Kaliszyk University of Innsbruck File Attached

10:30 - 12:10	Tactics and Proof EngineeringCoqPL at Watercourt A Chair(s): Benjamin Delaware Purdue University

10:30 25m Talk		A “destruct” Tactic for Mtac2 CoqPL Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET File Attached
10:55 25m Talk		Typed Template Coq CoqPL Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell University File Attached
11:20 25m Talk		Elpi: an extension language for Coq CoqPL Enrico Tassi INRIA File Attached
11:45 25m Talk		Coqatoo: Generating Natural Language Versions of Coq Proofs CoqPL Andrew Bedford Laval University File Attached

14:00 - 14:50	PL MetatheoryCoqPL at Watercourt A Chair(s): Steve Zdancewic University of Pennsylvania

14:00 25m Talk		Locally Nameless at Scale CoqPL Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania File Attached
14:25 25m Talk		A Coq Formalisation of a Core of R CoqPL Martin Bodin CMM File Attached

14:50 - 15:30	Coq developers talk & panelCoqPL at Watercourt A

14:50 40m Talk		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria, Maxime Dénès INRIA, Yves Bertot INRIA File Attached

16:00 - 18:05	Semantics and SynthesisCoqPL at Watercourt A Chair(s): Ilya Sergey University College London

16:00 25m Talk		Phantom Types for Quantum Programs CoqPL Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania File Attached
16:25 25m Talk		Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL Abhishek Anand Cornell University, Greg Morrisett Cornell University File Attached
16:50 25m Talk		Towards Context-Aware Data Refinement CoqPL Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University File Attached
17:15 25m Talk		Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin Westbrook Galois, Inc. File Attached
17:40 25m Talk		A calculus for logical refinements in separation logic CoqPL Dan Frumin Radboud University, Robbert Krebbers Delft University of Technology File Attached

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Watercourt A	CoqPL Keynote																		CoqPL Tactics and Proof Engineering																																										CoqPL PL Metatheory										CoqPL Coq developers talk & panel														CoqPL Semantics and Synthesis

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Watercourt A	CoqPL CoqHammer: Strong Automation for Program Verification 09:00 - 10:00																		CoqPL A “destruct” Tactic for Mtac2 10:30 - 10:55					CoqPL Typed Template Coq 10:55 - 11:20					CoqPL Elpi: an extension language for Coq 11:20 - 11:45					CoqPL Coqatoo: Generating Natural Language Versions of Coq Proofs 11:45 - 12:10																											CoqPL Locally Nameless at Scale 14:00 - 14:25					CoqPL A Coq Formalisation of a Core of R 14:25 - 14:50					CoqPL Session with the Coq Development Team 14:50 - 15:30														CoqPL Phantom Types for Quantum Programs 16:00 - 16:25					CoqPL Revisiting Parametricity: Inductives and Uniformity of Propositions 16:25 - 16:50					CoqPL Towards Context-Aware Data Refinement 16:50 - 17:15					CoqPL Mechanizing the Construction and Rewriting of Proper Functions in Coq 17:15 - 17:40					CoqPL A calculus for logical refinements in separation logic 17:40 - 18:05

Room information: Watercourt A

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change

CoqPL

CoqPL

CoqPL

CoqPL

CoqPL

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Watercourt A

Program Display Configuration

Sat 13 JanDisplayed time zone: Tijuana, Baja California change

Sat 13 JanDisplayed time zone: Tijuana, Baja California change

CoqPL

CoqPL

CoqPL

CoqPL

CoqPL

Sat 13 JanDisplayed time zone: Tijuana, Baja California change

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change

Sat 13 Jan
Displayed time zone: Tijuana, Baja California change