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

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
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
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 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