| 9:00- 9:30 |
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud and Santiago Zanella Béguelin |
Automated Game-Based Cryptographic Proofs |
| 9:30-10:00 |
Maxime Dénès and Yves Bertot |
Experiments with computable matrices in the Coq system (slides) |
| 10:00-10:15 |
Ken Madlener, Sjaak Smetsers and Marko Van Eekelen |
Formal Component-Based Semantics (slides) |
| 10:15-10:30 |
Hendrik Tews |
Automatic library compilation and proof tree visualization for Coq Proof General (slides) |
| 10:30-11:15 |
Coffee |
|
| 11:15-11:45 |
Christian Doczkal and Gert Smolka |
Constructive Formalization of Classical Modal Logic (slides) |
| 11:45-12:15 |
Lionel Rieg |
The static debugger: classical realizability rescuing the programmer (slides) |
| 12:15-12:30 |
Emmanuel Polonowski |
Generic Environments in Coq (slides) |
| 12:30-14:00 |
Lunch |
|
| 14:00-14:30 |
Robbert Krebbers and Bas Spitters |
Computer certified efficient exact reals in Coq (slides) |
| 14:30-15:00 |
Erik Martin-Dorel |
Univariate and Bivariate Integral Roots Certificates Based on Hensel Lifting |
| 15:00-15:15 |
Jean-Marie Madiot and Pierre-Marie Pédrot |
Constructive axiomatic for the real numbers (slides) |
| 15:15-15:30 |
Guillaume Allais |
Using reflection to solve some differential equations (slides) |
| 15:30-16:00 |
Coffee |
|
| 16:00-17:00 |
Coq dev team |
Recent developments (slides) |