Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
POPL 2019 (series) / Hotel Cascais Miragem /

Room information: Sala VI

VenueHotel Cascais Miragem
Room nameSala VI
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 19 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote & Contributed Talks 1CoqPL at Sala VI
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
09:00
5m
Day opening
Opening
CoqPL

09:05
60m
Talk
Coq User Interfaces: Past, Present, and Future (Keynote)
CoqPL
Emilio Jesús Gallego Arias INRIA
10:05
25m
Talk
Counterexamples for Coq Conjectures
CoqPL
Samuel Gruetter Massachusetts Institute of Technology
File Attached
11:15 - 12:30
Contributed Talks 2CoqPL at Sala VI
Chair(s): Enrico Tassi INRIA
11:15
25m
Talk
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL
Kiran Gopinathan University College London, Ilya Sergey Yale-NUS College and National University of Singapore
File Attached
11:40
25m
Talk
Verifying Finality for Blockchain Systems
CoqPL
Karl Palmskog University of Texas at Austin, Milos Gligoric University of Texas at Austin, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
File Attached
12:05
25m
Talk
WIP: Formalizing the Concordium Consensus Protocol in Coq
CoqPL
Thomas Dinsdale-Young , Bas Spitters Aarhus University, Søren Eller Thomsen Aarhus University, Daniel Tschudi Aarhus University
File Attached
14:00 - 15:30
Contributed Talks 3 & Coq DevelopersCoqPL at Sala VI
Chair(s): Qinxiang Cao Shanghai Jiao Tong University
14:00
25m
Talk
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
CoqPL
Vadim Zaliva Carnegie Mellon University, USA, Matthieu Sozeau Inria
File Attached
14:25
25m
Talk
Reifying and Translating a Monadic Fragment of Gallina
CoqPL
Paolo Torrini
File Attached
14:50
40m
Demonstration
Session with the Coq Development Team
CoqPL
Maxime Dénès INRIA, Matthieu Sozeau Inria
16:00 - 17:40
Contributed Talks 4CoqPL at Sala VI
Chair(s): Robbert Krebbers Delft University of Technology
16:00
25m
Talk
Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs
CoqPL
Qinxiang Cao Shanghai Jiao Tong University
File Attached
16:25
25m
Talk
Teaching Discrete Mathematics to Early Undergraduates with Software Foundations
CoqPL
Michael Greenberg Pomona College, Joseph C. Osborn Pomona College
File Attached
16:50
25m
Talk
Ltac2: Tactical Warfare
CoqPL
Pierre-Marie Pédrot
File Attached
17:15
25m
Talk
Towards a Coq Formalisation of Build Systems
CoqPL
Georgy Lukyanov Newcastle University, UK, Andrey Mokhov Newcastle University, UK
File Attached

Sat 19 Jan

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Sala VI

CoqPL

Keynote & Contributed Talks 1

CoqPL

Contributed Talks 2

CoqPL

Contributed Talks 3 & Coq Developers

CoqPL

Contributed Talks 4

Sat 19 Jan

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Sala VI
CoqPL
Opening
09:00 - 09:05
CoqPL
Coq User Interfaces: Past, Present, and Future (Keynote)
09:05 - 10:05
CoqPL
Counterexamples for Coq Conjectures
10:05 - 10:30
CoqPL
Towards Mechanising Probabilistic Properties of a Blockchain
11:15 - 11:40
CoqPL
Verifying Finality for Blockchain Systems
11:40 - 12:05
CoqPL
WIP: Formalizing the Concordium Consensus Protocol in Coq
12:05 - 12:30
CoqPL
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
14:00 - 14:25
CoqPL
Reifying and Translating a Monadic Fragment of Gallina
14:25 - 14:50
CoqPL
Session with the Coq Development Team
14:50 - 15:30
CoqPL
Deep Embedded Hoare Logic for Building Machine-Checkable Foundational P ...
16:00 - 16:25
CoqPL
Teaching Discrete Mathematics to Early Undergraduates with Software Fou ...
16:25 - 16:50
CoqPL
Ltac2: Tactical Warfare
16:50 - 17:15
CoqPL
Towards a Coq Formalisation of Build Systems
17:15 - 17:40