OPCT 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
co-located with POPL 2019
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
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
File Attached
14:50
40m
Demonstration
Session with the Coq Development Team
CoqPL

Sat 19 Jan

Displayed time zone: Belfast change