The Coq Workshop 2011

Venue: ITP, Nijmegen.

Program
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)

To the workshop homepage. Contact: Bas Spitters