POPL 2019 (series) / CoqPL 2019 (series) /
CoqPL 2019 Program
This is the CoqPL 2019 program - see the full program for POPL 2019 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 19 JanDisplayed time zone: Belfast change
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 5mDay opening | Opening CoqPL | ||
09:05 60mTalk | Coq User Interfaces: Past, Present, and Future (Keynote) CoqPL | ||
10:05 25mTalk | Counterexamples for Coq Conjectures CoqPL Samuel Gruetter Massachusetts Institute of Technology File Attached |
11:15 - 12:30 | |||
11:15 25mTalk | 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 25mTalk | 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 25mTalk | 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 25mTalk | Reification of Shallow-Embedded DSLs in Coq with Automated Verification CoqPL File Attached | ||
14:25 25mTalk | Reifying and Translating a Monadic Fragment of Gallina CoqPL File Attached | ||
14:50 40mDemonstration | Session with the Coq Development Team CoqPL |
16:00 - 17:40 | |||
16:00 25mTalk | Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs CoqPL Qinxiang Cao Shanghai Jiao Tong University File Attached | ||
16:25 25mTalk | Teaching Discrete Mathematics to Early Undergraduates with Software Foundations CoqPL File Attached | ||
16:50 25mTalk | Ltac2: Tactical Warfare CoqPL File Attached | ||
17:15 25mTalk | Towards a Coq Formalisation of Build Systems CoqPL File Attached |