[TYPES/announce] CoqPL 2019: Call for Participation

Robbert Krebbers types-announce at robbertkrebbers.nl
Thu Nov 29 08:09:17 EST 2018


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


More information about the Types-announce mailing list