The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

A tentative program and extended abstracts for the Coq workshop at ITP
is now available:

http://www.cs.ru.nl/~spitters/program.html

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