Abstract is missing.
- Formal verification in Coq of program properties involving the global state effectJean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous. 1-16
- Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrièresSylvain Conchon, David Declerck, Luc Maranget, Alain Mebsout. 17-32
- What could Coq do for Database Software? - A Progress ReportYoichi Hirai, Reynald Affeldt. 33-48
- Exécution efficace de programmes ReactiveMLLouis Mandel, Cédric Pasteur. 49-64
- Unification des couleurs dans un $\lambda$-calcul polychromeBernard P. Serpette, Pascal Manoury, Emmanuel Chailloux. 65-76
- Une sémantique statique pour MongoDBAdrien Husson. 77-92
- Réseaux de Kahn à rafales et horloges entièresLouis Mandel, Adrien Guatto. 93-108
- Pretty-big-step-semantics-based Certified Abstract InterpretationMartin Bodin, Thomas Jensen, Alan Schmitt. 109-130
- Comment un chameau peut-il écrire un journal ?Julien Signoles. 131-148
- De la KAM avec un Processus d'Ordre Supe'rieurDamien Pous, Alan Schmitt. 149-158
- Analyse de dépendances et correction des réseaux de preuveMarc Bagnol, Amina Doumane, Alexis Saurin. 159-174
- Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseusePierre-Marie Pédrot, Amina Doumane, Alexis Saurin. 175-189