Robbert Krebbers
2018-11-29 13:09:50 UTC
The CoqPL'19 program is now online: on 19 January 2019, we will have
12 exciting talks on using Coq for building certified systems.
# Program
See https://popl19.sigplan.org/track/CoqPL-2019#program
## Invited talks
- Coq User Interfaces: Past, Present, and Future
Emilio Jesús Gallego Arias
- Session with the Coq Development Team
Maxime Dénès, Matthieu Sozeau
## Contributed talks
- Counterexamples for Coq Conjectures
Sam Gruetter
- Towards Mechanising Probabilistic Properties of a Blockchain
Kiran Gopinathan, Ilya Sergey
- Verifying Finality for Blockchain Systems
Karl Palmskog, Milos Gligoric, Lucas Peña, Grigore Rosu
- WIP: Formalizing the Concordium consensus protocol in Coq
Thomas Dinsdale-Young, Bas Spitters, Søren Eller Thomsen, Daniel Tschudi
- Reification of shallow-embedded DSLs in Coq with automated verification
Vadim Zaliva, Matthieu Sozeau
- Reifying and translating a monadic fragment of Gallina
Paolo Torrini
- Deep Embedded Hoare Logic for Building Machine-Checkable Foundational
Program Correctness Proofs
Qinxiang Cao
- Teaching Discrete Mathematics to Early Undergraduates with Software
Foundations
Michael Greenberg, Joseph C. Osborn
- Ltac2: Tactical Warfare
Pierre-Marie Pédrot
- Towards a Coq Formalisation of Build Systems
Georgy Lukyanov, Andrey Mokhov
# Venue / Registration
CoqPL'19 is co-located with POPL'19 in Cascais/Lisbon (Portugal). The
early registration deadline for POPL/CoqPL is 10 December 2018. More
information can be found at the POPL website:
https://popl19.sigplan.org/attending/Registration
12 exciting talks on using Coq for building certified systems.
# Program
See https://popl19.sigplan.org/track/CoqPL-2019#program
## Invited talks
- Coq User Interfaces: Past, Present, and Future
Emilio Jesús Gallego Arias
- Session with the Coq Development Team
Maxime Dénès, Matthieu Sozeau
## Contributed talks
- Counterexamples for Coq Conjectures
Sam Gruetter
- Towards Mechanising Probabilistic Properties of a Blockchain
Kiran Gopinathan, Ilya Sergey
- Verifying Finality for Blockchain Systems
Karl Palmskog, Milos Gligoric, Lucas Peña, Grigore Rosu
- WIP: Formalizing the Concordium consensus protocol in Coq
Thomas Dinsdale-Young, Bas Spitters, Søren Eller Thomsen, Daniel Tschudi
- Reification of shallow-embedded DSLs in Coq with automated verification
Vadim Zaliva, Matthieu Sozeau
- Reifying and translating a monadic fragment of Gallina
Paolo Torrini
- Deep Embedded Hoare Logic for Building Machine-Checkable Foundational
Program Correctness Proofs
Qinxiang Cao
- Teaching Discrete Mathematics to Early Undergraduates with Software
Foundations
Michael Greenberg, Joseph C. Osborn
- Ltac2: Tactical Warfare
Pierre-Marie Pédrot
- Towards a Coq Formalisation of Build Systems
Georgy Lukyanov, Andrey Mokhov
# Venue / Registration
CoqPL'19 is co-located with POPL'19 in Cascais/Lisbon (Portugal). The
early registration deadline for POPL/CoqPL is 10 December 2018. More
information can be found at the POPL website:
https://popl19.sigplan.org/attending/Registration