diff --git a/papers/icfp2021/related.tex b/papers/icfp2021/related.tex
index 609d71e9b52c00b277de400b8b9a6515cf6c17da..944f08108e584d2445e7052db7bd96455393949b 100644
--- a/papers/icfp2021/related.tex
+++ b/papers/icfp2021/related.tex
@@ -7,9 +7,9 @@ Several approaches were tried, targeting various verification frameworks, variou
 The  notion of \emph{linearizability} is central for specifying such libraries.
 \citet{dongol2015verifying} gave a survey of the different techniques used for linearizability of concurrent libraries at that time.
 %TODO : corriger l'entrée biblio de l'article d'Armaël pour la version finale
-Of particular interest in the context of separation logic is the technique of \emph{logical tomicity}, which has been recently proved to be equivalent to linearizability~\cite{gueneau2021theorems} in the context of a sequentially consistent model.
+Of particular interest in the context of separation logic is the technique of \emph{logical atomicity}, which has been recently proved to be equivalent to linearizability~\cite{gueneau2021theorems} in the context of a sequentially consistent model.
 This concept has been developed through several iterations over the last decade~\cite{da2014tada,iris-15,jacobs2011expressive,svendsen-birkedal-parkinson-hocap-13,jung-prophecies-20}.
-In the present work, we adapted an unpublished, modern version of Iris' logically atomic triples~\cite{jung-slides-2019}, and adapted it to the logic \cosmo{}.
+In the present work, we adapt an unpublished, modern version of Iris's logically atomic triples~\cite{jung-slides-2019}, to the setting of \cosmo{}.
 This is, to the best of our knowledge, the first use of logical atomicity in a weakly consistent setting.
 
 % TODO : je ne sais pas quoi dire de ça. Dans la mesure où ce n'est qu'un preprint arxiv, je propose de ne pas en parler pour l'instant.
@@ -22,8 +22,8 @@ This is, to the best of our knowledge, the first use of logical atomicity in a w
 Another popular approach for proving the correctness of concurrent libraries is the use of refinement with respect to a simpler implementation.
 This is the track chosen by ReLoc~\cite{frumin2018reloc}, which has recently been combined with logical atomicity~\cite{frumin2018reloc}.
 Interestingly, Reloc has been recently used for proving the correctness of a concurrent queue implementation, which is very close to ours~\cite{vindum-birkedal-21,vindum-frumin-birkedal-21}.
-However, this proof does not handle relaxed memory behaviors, so that it did not have to provide a solution to the problem of specifying the lack of happens-before relationship between some data structure accesses, which we discussed in \sref{sec:queue:spec:weak}.
-In particular, for this reason, our queue implementation \emph{is not} a refinement of a naive implementation which would use a lock for guarding a sequential implementation, so a refinement-based approach would be useful for proving our library correct.
+However, this proof does not handle relaxed memory behaviors, so that it does not have to provide a solution to the problem of specifying the lack of happens-before relationship between some data structure accesses, which we discussed in \sref{sec:queue:spec:weak}.
+In particular, for this reason, our queue implementation \emph{is not} a refinement of a naive implementation which would use a lock to protect a sequential implementation, so a refinement-based approach would be useful for proving our library correct.
 The refinement approach has also been used to prove correct some data structures used in a concurrent garbage collector~\cite{zakowski2018verified}.
 
 
@@ -36,7 +36,7 @@ As discussed in \sref{sec:queue:spec:weak}, even the definition of linearizabili
 % Causal Linearizability, Doherty and Derrick 2016
 % Des mêmes auteurs: https://arxiv.org/abs/1810.09612v1
 In contrast, other authors have developed new kinds of specifications which allow for weak behaviors of the library itself~\cite{krishna-emmi-enea-jovanovic-20,emmi-enea-19,raad-19}.
-We found that our method of combining logically atomic triples with views is expressive and allow for concise specifications at the same time.
+We found that our method of combining logically atomic triples with views is expressive and allows for concise specifications at the same time.
 %% % Constantin Enea, "Verifying Visibility-Based Weak Consistency".
 %% % Technique de preuve à base de simulations (ce n'est pas de la
 %% % logique de séparation), avec mise en oeuvre basé sur des prouveurs
@@ -62,7 +62,7 @@ We found that our method of combining logically atomic triples with views is exp
 %% client qui utilise plusieurs objets différents avec des specs différentes.
 %% Réponse pas très claire.
 %% \end{comment}
-Previous works include the generalization of various methods to weak-consistency: \citet{le2013correctws,le2013correctfifo} used manual methods directly tied to the axiomatic memory model to prove the correctness of a queue and of a work-stealing algorithm, while \citet{lahav2015owicki} adapted the Owicki-Gries methodology to the release-acquire fragment of the C11 memory model and applied it to verify a read-copy-update library.
+Previous works include the generalization of various methods to weak consistency: \citet{le2013correctws,le2013correctfifo} used manual methods directly tied to the axiomatic memory model to prove the correctness of a queue and of a work-stealing algorithm, while \citet{lahav2015owicki} adapted the Owicki-Gries methodology to the release-acquire fragment of the C11 memory model and applied it to verify a read-copy-update library.
 The idea of a separation logic for programs with a relaxed memory semantics has been first developed in the RSL logic~\cite{vafeiadis-narayan-13}, and further developed in subsequent work~\cite{turon-vafeiadis-dreyer-14,doko-vafeiadis-16,kaiser-17,dang-20,mevel-jourdan-pottier-20}.
 None of these papers addressed the problem of the full functional correctness of a data structure.
 In particular, the specification proposed for a circular buffer in GPS~\cite{turon-vafeiadis-dreyer-14} is a weak specification in the style of \sref{sec:queue:spec:sc:persistent}: in contrast to ours, it does not specify in which order the elements leave the queue.