VenueOmni Hotel
Room nameWatercourt A
Floor0
Room InformationNo extra information available
Program

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

Conference Day
Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
KeynoteCoqPL at Watercourt A
Chair(s): Yves BertotINRIA
09:00
60m
Talk
CoqHammer: Strong Automation for Program Verification
CoqPL
Lukasz CzajkaUniversity of Innsbruck, Cezary KaliszykUniversity of Innsbruck
File Attached
10:30 - 12:10
Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin DelawarePurdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier, Matthieu SozeauInria, Nicolas TabareauInria, France, Abhishek AnandCornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew BedfordLaval University
File Attached
14:00 - 14:50
PL MetatheoryCoqPL at Watercourt A
Chair(s): Steve ZdancewicUniversity of Pennsylvania
14:00
25m
Talk
Locally Nameless at Scale
CoqPL
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania
File Attached
14:25
25m
Talk
A Coq Formalisation of a Core of R
CoqPL
File Attached
14:50 - 15:30
Coq developers talk & panelCoqPL at Watercourt A
14:50
40m
Talk
Session with the Coq Development Team
CoqPL
File Attached
16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya SergeyUniversity College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin WestbrookGalois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached

Conference Day
Sat 13 Jan

Displayed time zone: Tijuana, Baja California change