diff --git a/bib/programming.bib b/bib/programming.bib
index ecf95fb..01c4eec 100644
--- a/bib/programming.bib
+++ b/bib/programming.bib
@@ -16,12 +16,12 @@ howpublished = {\url{https://github.com/scolobb/nsmux}}
 }
 
 @misc{sympy,
-title = {SymPy homepage},
+title = {{S}ym{P}y homepage},
 howpublished = {\url{http://www.sympy.org}}
 }
 
 @misc{categories,
-title = {A category theory module for SymPy},
+title = {A category theory module for {S}ym{P}y},
 author = {Sergiu Ivanov},
 howpublished = {\url{https://github.com/scolobb/sympy}}
 }
diff --git a/recherche.tex b/recherche.tex
index c3ae81b..97b06d6 100644
--- a/recherche.tex
+++ b/recherche.tex
@@ -51,15 +51,16 @@ longtemps dans la théorie des langages formels, surtout la variante
 sans contexte qui généralise les opérations de concaténation et
 quotient, deux opérations
 fondamentales~\cite{Haussler82,KariPhD}. L'inspiration qui a motivé
-l'introduction de ces opérations vient de la linguistique, car elles
-semblent modéliser assez précisément les procédés de construction des
-phrases dans une langue vivante~\cite{Marcus69,PaunKluwer97}. Il a été
-montré récemment que l'insertion et l'effacement possèdent une
-inspiration biologique et qu'ils formalisent l'hybridation erronée des
-brins d'ADN ({\em mismatched DNA annealing})~\cite{PRSbook}. De plus,
-il a été découvert que même l'édition de l'ARN ({\em RNA editing})
-réalisé par certains protozoaires consiste généralement en des ajouts
-et des suppressions dans des brins d'ARN.
+l'introduction de l'insertion et l'effacement vient de la
+linguistique, car elles semblent modéliser assez précisément les
+procédés de construction des phrases dans une langue
+vivante~\cite{Marcus69,PaunKluwer97}.  Il a été montré récemment que
+l'étude de l'insertion de l'effacement est intéressante du point de
+vue biologique, car ses opérations formalisent l'hybridation erronée
+des brins d'ADN ({\em mismatched DNA annealing})~\cite{PRSbook}. De
+plus, il a été découvert que même l'édition de l'ARN ({\em RNA
+  editing}) réalisée par certains protozoaires consiste généralement
+en des ajouts et des suppressions dans des brins d'ARN.
 
 De manière intuitive, une règle d'insertion rajoute une sous-chaîne à
 une chaîne de caractères dans un contexte donné. Une règle
@@ -70,23 +71,23 @@ un ensemble fini de règles d'insertion
 et d'effacement ; il engendre un langage en appliquant ces règles
 séquentiellement à un ensemble fini de mots dits axiomes. La
 complexité d'un système d'insertion/effacement est décrite par le
-6-uplet $(n,m,m'; p,q,q')$ dit taille, où les premiers trois composant
+6-uplet $(n,m,m'; p,q,q')$ dit taille, où les premiers trois composants
 représentent la longueur maximale de la sous-chaîne insérée et la
 taille maximale des contextes à gauche et à droite, alors que les
 trois derniers composants décrivent les mêmes paramètres pour les
 règles d'effacement.
 
 Dans le cadre de ma thèse nous nous sommes intéressés tout d'abord à
-des systèmes d'insertion/sup\-pres\-sion de taille $(1,m,0; 1,q,0)$,
+des systèmes d'insertion/ef\-face\-ment de taille $(1,m,0; 1,q,0)$,
 c'est-à-dire aux systèmes dans lesquels toutes les règles n'ont pas de
 contexte à droite et insèrent ou suppriment un caractère. Nous avons
 montré que ces systèmes engendrent tous les langages rationnels, et
 même certains langages algébriques. D'un autre côté, nous avons prouvé
 que pour tout système de taille $(1,m,0;1,q,0)$ avec $m\geq 2$ ou
-$n\geq 2$ il existe un système de taille $(1,2,0; 1,1,0)$ et un autre
-de taille $(1,1,0; 1,2,0)$ qui le simulent. Nous nous sommes aussi
+$q\geq 2$ il existe un système de taille $(1,2,0; 1,1,0)$ et un autre
+de taille $(1,1,0; 1,2,0)$ qui le simule. Nous nous sommes
 intéressés aussi aux systèmes de taille $(1,1,0;1,1,0)$ qui, malgré
-leur simplicité apparente, peuvent eux aussi engendrer des langages
+leur simplicité apparente, peuvent engendrer des langages
 non algébriques. Afin de mieux analyser le comportement dynamique de
 ces systèmes, nous avons introduit un outil de représentation
 graphique de leurs dérivations.
@@ -96,9 +97,9 @@ trois mécanismes de contrôle : contrôle par graphe ({\em graph
   control}), contrôle semi-conditionnel ({\em semi-conditional
   control}) et contextes aléatoires ({\em random context
   control}). Nous avons prouvé que les systèmes équipés de ces
-mécanismes étaient Turing complets avec de très petites
+mécanismes sont Turing complets avec de très petites
 règles. Notamment, nous avons prouvé que le contrôle semi-conditionnel
-augmentait la puissance d'expression des systèmes
+augmente la puissance d'expression des systèmes
 d'insertion/effacement de taille $(1,0,0;1,0,0)$, c'est-à-dire des
 systèmes avec des règles sans contexte, est les rend Turing complets.
 
@@ -119,8 +120,8 @@ La complétude computationnelle des réseaux de processeurs
 introduction~\cite{CMVMS2001,CVS97}. Des variations au modèle ont été
 proposées plus tard et prouvées Turing complètes elles
 aussi~\cite{AMVR2006,CMVMS2003}. Nous nous sommes intéressés plutôt à
-l'universalité et à la minimisation du nombre de règles d'insertion,
-d'effacement et de substitution dans les réseaux universels. Nous
+l'universalité et à la minimisation du nombre de règles
+dans les réseaux universels. Nous
 avons ainsi construit des réseaux universels à 4, 5 et 7 règles
 seulement, avec des fonctions de codage différentes.
 
@@ -131,8 +132,8 @@ telle machine possède un nombre fini de registres, qui peuvent
 contenir des entiers non négatifs. Le programme d'une machine à
 registres est une liste étiquetée d'instructions élémentaires :
 l'incrément d'un registre, le décrément d'un registre et le teste si
-un registre est vide. Les machines à registres sont ainsi un modèle
-très proche de l'organisation des ordinateurs digitaux habituels.
+un registre est vide. Les machines à registres sont ainsi
+très proches de l'organisation des ordinateurs digitaux habituels.
 
 Il a été montré que les machines à registres sont Turing complets, et
 qu'en plus n'importe quelle fonction calculable sur les entiers non
@@ -174,7 +175,7 @@ La dernière partie de ma thèse porte sur l'universalité des systèmes
 de réécriture de multiensembles avec des inhibiteurs et aussi des
 réseaux de Petri avec des arcs inhibiteurs --- deux modèles qui sont
 fondamentalement similaires. En effet, un état (marquage) d'un réseau
-de Petri est décrit comme une fonction qui associe à chaque place le
+de Petri est décrit par une fonction qui associe à chaque place le
 nombre de jetons qu'elle contient ; or le marquage est un
 multiensemble sur l'alphabet des symboles qui désignent les
 places. Les transitions de réseaux de Petri correspondent ainsi aux
@@ -188,7 +189,7 @@ d'étendre le pouvoir d'expression de ces modèles, dont l'idée des
 inhibiteurs. Dans les réseaux de Petri, un arc inhibiteur entre une
 place et une transition empêche celle-ci de se déclencher si la place
 n'est pas vide. De la même manière, on peut munir une règle de
-réécriture de multiensembles avec un ensemble de symboles qui ne
+réécriture de multiensembles avec une collection de symboles qui ne
 doivent pas être présents pour que la règle soit applicable. Il a été
 prouvé que les réseaux de Petri avec des arcs inhibiteurs et les
 systèmes de réécriture de multiensembles avec des inhibiteurs sont
@@ -210,7 +211,7 @@ nécessaires pour atteindre la complétude computationnelle : les
 réseaux de Petri avec un seul arc inhibiteur ne sont pas Turing
 complets~\cite{Reinhardt08}.
 
-Même si les résultats d'universalité présentés dans la dernière partie
+Même si les résultats portant sur l'universalité présentés dans la dernière partie
 de ma thèse apparaissent sous la forme de réseaux de Petri, la
 correspondance directe avec les systèmes de réécriture de
 multiensembles permet de formuler immédiatement les mêmes résultats
@@ -264,7 +265,7 @@ comportement désiré. J'ai participé à ce travail en développant un
 simulateur avec des moteurs des simulations échangeables pouvant être
 réalisés en des langages différents. J'ai notamment fourni un moteur
 de simulation utilisant la technologie OpenCL de programmation
-parallèle sur les cartes graphiques et un autre, plus flexible mais
+pour des architectures parallèles et un autre, plus flexible mais
 moins performant, implémenté en Haskell.
 
 En ce qui concerne le développement des algorithmes distribués, je me
@@ -275,7 +276,7 @@ de l'horloge globale rapproche le modèle des systèmes parallèles
 composés d'un certain nombre de processus qui interagissent. Dans mon
 travail, j'ai exprimé les mécanismes de synchronisation en termes de
 règles de réécriture de multiensembles et j'ai montré comment ces
-mécanismes pouvaient être utilisés pour la résolution des problèmes de
+mécanismes pouvaient être utilisés pour la résolution de problèmes de
 concurrence classiques.
 
 Nous avons continué l'exploration des algorithmes distribués en
@@ -286,7 +287,7 @@ avant est une méthode de déduction qui applique des implications
 logiques en partant des prémisses pour en déduire de nouvelles
 conclusions. Le chaînage avant consiste donc à construire toutes les
 conclusions déductibles à partir des axiomes jusqu'à ce que la
-proposition cible est obtenue. Par opposition, le chaînage arrière
+proposition cible soit obtenue. Par opposition, le chaînage arrière
 part des conclusions pour essayer de remonter aux axiomes. Le chaînage
 arrière a souvent tendance à explorer moins de possibilités et est
 préféré dans les cas d'utilisation pratiques. Il est remarquable que
@@ -369,7 +370,7 @@ tableau dans l'espace cartésien à deux dimensions peut contenir un
 nombre fini de cellules non vides disposées dans une configuration
 particulière, les autres cellules étant vides. Une règle de réécriture
 de tableaux qui rajoute une nouvelle cellule peut s'appliquer à un
-motif seulement si cette nouvelle cellule ne correspond pas à un
+motif seulement si cette nouvelle cellule correspond à un
 endroit vide dans le tableau d'origine.
 
 Ma contribution à l'étude des grammaires de tableaux a consisté à
@@ -433,7 +434,7 @@ et seront disponibles au public dès leur finalisation.
 
 Finalement, afin de faciliter la conception et la vérification de
 systèmes à réactions, j'ai implémenté un simulateur de ce modèle. Le
-code source du simulateur, ainsi qu'une documentation, est disponible
+code source du simulateur, ainsi que la documentation, est disponible
 en ligne~\cite{brsim}. J'ai aussi réalisé une interface
 Web~\cite{brsimweb} qui permet d'utiliser mon simulateur sans à avoir
 à télécharger et compiler le code.