Update related (connection between selfification and our work).

Update practical (mentions n0=1 for our examples).

Makefile

 default:
 	latexmk -pdf -bibtex main.tex
 
+
+
+
 clean:
 	rm -rf *.synctex* *.blg *.dvi *.aux *.fdb_latexmk *.log *.fls *.xcp *.out

main.bib

@@ -258,15 +258,6 @@ url={http://www.cduce.org/papers/frisch_phd.pdf}
 }
 
 
-@PhdThesis{Pet19phd,
-  author = 	 {Tommaso Petrucciani},
-  title = 	 {Polymorphic Set-Theoretic Types for Functional Languages},
-  school = 	 {Joint Ph.D.\ Thesis, Università di Genova and Université Paris Diderot},
-  month = mar,
-  url = {https://tel.archives-ouvertes.fr/tel-02119930},
-  year = 	 2019,
-  note = {Available at \url{https://tel.archives-ouvertes.fr/tel-02119930}},
-  }
 
 
 @article{castagna2019gradual,

practical.tex

@@ -27,7 +27,11 @@ the algorithmic system $\vdashA$ as well as all the type operations
 defined in this work. One optimization that our implementation
 features (with respect to the formal presentation) is the use of a
 memoization environment in the code of the $\Refine {e,t}{\Gamma}$
-function, which allows the inference to avoid unnecessary traversals of $e$.
+function, which allows the inference to avoid unnecessary traversals
+of $e$.
+Lastly, while our prototype allows the user to specify a particular
+value for the $n_0$ parameter, the default value of $1$ is sufficient
+to check all examples we present in the following sections.
 }
 
 \subsection{Experiments}

related.tex

@@ -261,13 +261,16 @@ language and their approach is extended with polymorphism, dynamic
 dispatch and record types.
 \rev{%%%
 A problem that is faced by refinement type systems is the one of
-propagating in the branches of a test the information learned on
-a \emph{sub-expression} of a tested expression. A solution
+propagating in the branches of a test the very precise information
+learned from the test (usually that some equality between terms holds).  A solution
 that is for instance chosen by~\citet{OTMW04} and \citet{KF09} is to devise a
 meta-function that recursively explores both a type and an expression
-and propagates the type information on the sub-expressions. This
+and constructs a more precise \emph{dependent} type. In the dependent
+type, fresh variables are introduced to name sub-expressions and
+record the new constraints.
+This
 process---called \emph{selfification} in the cited works---roughly
-corresponds to our $\constrf$ function (see Section~\ref{sec:typenv}).
+corresponds to a our $\constrf$ and \Refinef{} functions (see Section~\ref{sec:typenv}).
 Another approach is the one followed by \citet{RKJ08} which is
 completely based on a program transformation, namely, it consists in putting the term
 in \emph{administrative normal form} (\cite{SF92}). Using a program
@@ -377,8 +380,11 @@ Racket~\cite{THF10} the type-system associates to an expression a
 quadruple formed by its type, two logical propositions, and an object which is
 a pointer to the environment for the type hypothesis about the
 expression and, as such, it plays the role of our extended type
-environments. Likewise, the \emph{selfification} of ... \textbf{KIM
-PLEASE ADD A LINE ON THIS POINT}.
+environments. Likewise, the \emph{selfification} of \cite{OTMW04}
+and \cite{KF09}, propagates the precise type constraints learned
+during a test. However, in the latter, whole the information can be
+kept at the type level, since dependent types contains terms and can
+introduce variables, while in our approach the mapping is kept in an environment.
 Nevertheless, we are confident that even this last non-standard aspect
 of our system can be removed and that occurrence typing can be
 explained in a pure standard type-theoretic setting.