Write a Blog >>
CoqPL 2018
Mon 8 - Sat 13 January 2018 Los Angeles, California, United States
co-located with POPL 2018
POPL 2018 (series) / CoqPL 2018 (series) / Omni Hotel /

Room information: Watercourt A

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
Keynote at Watercourt A
Chair(s): Yves Bertot INRIA
09:00
60m
Talk
CoqHammer: Strong Automation for Program Verification
Lukasz Czajka University of Innsbruck, Cezary Kaliszyk University of Innsbruck
File Attached
10:30 - 12:10
Tactics and Proof Engineering at Watercourt A
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
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
Enrico Tassi INRIA
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
Andrew Bedford Laval University
File Attached
14:00 - 14:50
PL Metatheory at Watercourt A
Chair(s): Steve Zdancewic University of Pennsylvania
14:00
25m
Talk
Locally Nameless at Scale
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
Martin Bodin CMM
File Attached
14:50 - 15:30
Coq developers talk & panel at Watercourt A
14:50
40m
Talk
Session with the Coq Development Team
Matthieu Sozeau Inria, Maxime Dénès INRIA, Yves Bertot INRIA
File Attached
16:00 - 18:05
Semantics and Synthesis at Watercourt A
Chair(s): Ilya Sergey University College London
16:00
25m
Talk
Phantom Types for Quantum Programs
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
Abhishek Anand Cornell University, Greg Morrisett Cornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
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
Edwin Westbrook Galois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
Dan Frumin Radboud University, Robbert Krebbers Delft University of Technology
File Attached

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:0030
Watercourt A

Keynote

Tactics and Proof Engineering

PL Metatheory

Coq developers talk & panel

Semantics and Synthesis

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
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