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
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00: KeynoteCoqPL at Watercourt A
Chair(s): Yves BertotINRIA
09:00 - 10:00
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 - 10:55
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
File Attached
10:55 - 11:20
Talk
Typed Template Coq
CoqPL
Simon Boulier, Matthieu SozeauInria, Nicolas TabareauInria, France, Abhishek AnandCornell University
File Attached
11:20 - 11:45
Talk
Elpi: an extension language for Coq
CoqPL
File Attached
11:45 - 12:10
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 - 14:25
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 - 14:50
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 - 15:30
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 - 16:25
Talk
Phantom Types for Quantum Programs
CoqPL
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
16:25 - 16:50
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
16:50 - 17:15
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
17:15 - 17:40
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin WestbrookGalois, Inc.
File Attached
17:40 - 18:05
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change