# Soutenance de thèse de Théo Zimmermann le 12 décembre

**URL:** <https://discourse.rocq-prover.org/t/soutenance-de-these-de-theo-zimmermann-le-12-decembre/513>\
**Category:** Annonces\
**Created:** [November 30, 2019, 11:56am UTC](https://discourse.rocq-prover.org/t/soutenance-de-these-de-theo-zimmermann-le-12-decembre/513 "2019-11-30T11:56:02Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [November 30, 2019, 11:56am UTC](https://discourse.rocq-prover.org/t/soutenance-de-these-de-theo-zimmermann-le-12-decembre/513/1 "2019-11-30T11:56:02Z")

</div>

Bonjour,

J’ai le plaisir de vous inviter à ma soutenance de thèse, intitulée :

Challenges in the collaborative evolution of a proof language and its ecosystem

Soit, en français :

Défis dans l’évolution collaborative d’un langage de preuve et de son écosystème

Une version préliminaire du manuscrit est disponible à cette adresse :

> **[memoirthesis.pdf](https://www.irif.fr/_media/users/theo/memoirthesis.pdf)**
>
> 1928.47 KB

La soutenance aura lieu en français. Elle se tiendra le 12 décembre  
2019 à 14h en salle 2014, au deuxième étage du bâtiment Sophie Germain  
(place Aurélie Nemours, Paris 13). Elle sera suivie d’un traditionnel  
pot en salle 3052, au troisième étage du même bâtiment.

Le jury est composé de : Benoît Combemale et Jean-Rémy Falleri  
(rapporteurs), Pierre Courtieu, Anne Etien, Tom Mens et Ralf Treinen  
(examinateurs), Hugo Herbelin et Yann Régis-Gianas (directeurs de  
thèse).

Résumé en français :

Dans cette thèse, je présente l’application de méthodes et de  
connaissances en génie logiciel au développement, à la maintenance et  
à l’évolution de Coq —un assistant de preuve interactif basé sur la  
théorie des types— et de son écosystème de paquets. Coq est développé  
chez Inria depuis 1984, mais sa base d’utilisateurs n’a cessé de  
s’agrandir, ce qui suscite désormais une attention renforcée quant à  
sa maintenabilité et à la participation de contributeurs externes à  
son évolution et à celle de son écosystème de plugins et de  
bibliothèques.

D’importants changements ont eu lieu ces dernières années dans les  
processus de développement de Coq, dont j’ai été à la fois un témoin  
et un acteur (adoption de GitHub en tant que plate-forme de  
développement, tout d’abord pour son mécanisme de pull request, puis  
pour son système de tickets, adoption de l’intégration continue,  
passage à des cycles de sortie de nouvelles versions plus courts,  
implication accrue de contributeurs externes dans les processus de  
développement et de maintenance open source). Les contributions de  
cette thèse incluent une description historique de ces changements, le  
raffinement des processus existants et la conception de nouveaux  
processus, la conception et la mise en œuvre de nouveaux outils  
facilitant l’application de ces processus, et la validation de ces  
changements par le biais d’évaluations empiriques rigoureuses.

L’implication de contributeurs externes est également très utile au  
niveau de l’écosystème de paquets. Cette thèse contient en outre une  
analyse des méthodes de distribution de paquets et du problème  
spécifique de la maintenance à long terme des paquets ayant un seul  
responsable.

Résumé en anglais :

In this thesis, I present the application of software engineering  
methods and knowledge to the development, maintenance, and evolution  
of Coq —an interactive proof assistant based on type theory— and its  
package ecosystem. Coq has been developed at Inria since 1984, but has  
only more recently seen a surge in its user base, which leads to much  
stronger concerns about its maintainability, and the involvement of  
external contributors in the evolution of both Coq, and its ecosystem  
of plugins and libraries.

Recent years have seen important changes in the development processes  
of Coq, of which I have been a witness and an actor (adoption of  
GitHub as a development platform, first for its pull request  
mechanism, then for its bug tracker, adoption of continuous  
integration, switch to shorter release cycles, increased involvement  
of external contributors in the open source development and  
maintenance process). The contributions of this thesis include a  
historical description of these changes, the refinement of existing  
processes, and the design of new ones, the design and implementation  
of new tools to help the application of these processes, and the  
validation of these changes through rigorous empirical evaluation.

Involving external contributors is also very useful at the level of  
the package ecosystem. This thesis additionally contains an analysis  
of package distribution methods, and a focus on the problem of the  
long-term maintenance of single-maintainer packages.