... @@ -185,7 +185,7 @@ subtyping. Probably a consequence of the pandemic. ... @@ -185,7 +185,7 @@ subtyping. Probably a consequence of the pandemic. Of course, the new version of the related work section includes now a Of course, the new version of the related work section includes now a detailed comparison with the (indeed highly related) chapter 5 of the detailed comparison with the (indeed highly related) chapter 5 of the dissertations, (see: p30l??-??) and, yes, the function application dissertations, (see: p30-31) and, yes, the function application inversion of Kent is, in the spirit, the same as our worra operator inversion of Kent is, in the spirit, the same as our worra operator (we do not know whether the reviewers noticed that worra'' is an (we do not know whether the reviewers noticed that worra'' is an inverted arrow'': read it from right to left). inverted arrow'': read it from right to left). ... @@ -305,14 +305,14 @@ connections as well. For example, the proof system for the ... @@ -305,14 +305,14 @@ connections as well. For example, the proof system for the $$\vdash^{Path}$$ judgment is very similar to the proof system used in $$\vdash^{Path}$$ judgment is very similar to the proof system used in {[}23{]} (Figures 4 \& 7 there). {[}23{]} (Figures 4 \& 7 there). \begin{answer} \begin{answer} Done (see: p29l??-??) Done (see: p29 first 10 lines) \end{answer} \end{answer} The approach of generalizing the type environment to The approach of generalizing the type environment to prove a more general set of propositions (here, about arbitrary prove a more general set of propositions (here, about arbitrary expressions, there, about expressions with a limited set a pure expressions, there, about expressions with a limited set a pure functions, but see below) is also present in both. functions, but see below) is also present in both. \begin{answer} \begin{answer} Done (see: p32l???-???) Done (see: p32 third quarter of the page) \end{answer} \end{answer} \pagebreak \pagebreak ... @@ -322,7 +322,7 @@ difficulties in proofs of type soundness is discussed in {[}22{]}. ... @@ -322,7 +322,7 @@ difficulties in proofs of type soundness is discussed in {[}22{]}. \begin{answer} \begin{answer} We added a long discussion on this point, namely how to We added a long discussion on this point, namely how to handle the type preservation property, in the related work section when handle the type preservation property, in the related work section when comparing with {[}22{]} (see: p29l??-??) comparing with {[}22{]} (see: p29 last paragraph, till page 30) More generally, we also went more in depth in the comparison with the More generally, we also went more in depth in the comparison with the logical approach by THF, to highlight further limitations of our logical approach by THF, to highlight further limitations of our ... @@ -366,7 +366,8 @@ paper clearer. ... @@ -366,7 +366,8 @@ paper clearer. This is a very nice insight. We reproduced it (giving credits) in the This is a very nice insight. We reproduced it (giving credits) in the section on related work, which now ends with a long discussion on the section on related work, which now ends with a long discussion on the design space w.r.t. side effects and on our future plans to cope with design space w.r.t. side effects and on our future plans to cope with the presence of impure expressions. (see: p32l??-??) the presence of impure expressions. See: p32 (last paragraph) till page 33 \end{answer} \end{answer} ... @@ -385,7 +386,7 @@ unneeded: ... @@ -385,7 +386,7 @@ unneeded: \begin{answer}\label{complexity} \begin{answer}\label{complexity} We added a long discussion to explain the reasons of our We added a long discussion to explain the reasons of our choice. It is in the related work section (see: p29l ??-??) when choice. It is in the related work section (see: p29bottom p30top) when comparing with {[}22{]} (i.e. Tobin-Hochstadt\&Felleisen comparing with {[}22{]} (i.e. Tobin-Hochstadt\&Felleisen 2008). In a nutshell we prefer starting with a system that 2008). In a nutshell we prefer starting with a system that satisfies type preservation, define a sound but not-complete satisfies type preservation, define a sound but not-complete ... @@ -504,7 +505,7 @@ is to ... @@ -504,7 +505,7 @@ is to show an example that works both in Typed Racket and in our system but show an example that works both in Typed Racket and in our system but it does not in TypeScript and Flow. In the case that this were the it does not in TypeScript and Flow. In the case that this were the correct interpretation of the remark of the reviewer,we added a correct interpretation of the remark of the reviewer,we added a comment in p28l???-??? comment in p28 \end{answer} \end{answer} ... @@ -569,7 +570,7 @@ type preservation). We rewrote the sentence to be more clear. ... @@ -569,7 +570,7 @@ type preservation). We rewrote the sentence to be more clear. =\Domain\setminus\semantic{\empt}=\Domain$. So =\Domain\setminus\semantic{\empt}=\Domain$. So $\semantic{\empt}$ is empty and undef is not in (the $\semantic{\empt}$ is empty and undef is not in (the interpretation of) \any. We added an explanation (see: interpretation of) \any. We added an explanation (see: p17l???-???). In short \texttt{Undef} is a special singleton type p17 after the definition of Types). In short \texttt{Undef} is a special singleton type whose interpretation contains only the whose interpretation contains only the constant \texttt{undef} which is not in $\Domain$. constant \texttt{undef} which is not in $\Domain$. \end{answer} \end{answer} ... @@ -662,7 +663,7 @@ the new contributions. ... @@ -662,7 +663,7 @@ the new contributions. of refined types appearing in arbitrary places, which is very similar of refined types appearing in arbitrary places, which is very similar to the first contribution of this work. to the first contribution of this work. \begin{answer} \begin{answer} Done (page 31??) Done (page 31 center) \end{answer} \end{answer} An alternative approach followed by refinement type systems is to An alternative approach followed by refinement type systems is to ANF-transform the programs. A discussion is missing on how these two ANF-transform the programs. A discussion is missing on how these two ... @@ -671,7 +672,7 @@ the new contributions. ... @@ -671,7 +672,7 @@ the new contributions. while the two alternatives used by refinement types preserve while the two alternatives used by refinement types preserve decidability. decidability. \begin{answer} \begin{answer} Done (page 31??) Done (page 31 center) \end{answer} \end{answer} \item \item ... @@ -682,7 +683,7 @@ the new contributions. ... @@ -682,7 +683,7 @@ the new contributions. also presents a set theoretic interpretation), thus a comparison is also presents a set theoretic interpretation), thus a comparison is missing. missing. \begin{answer} \begin{answer} Done (page 31??) Done (page 31 bottom) \end{answer} \end{answer} \item \item In 3.3 it is mentioned that we are not aware of any study in this In 3.3 it is mentioned that we are not aware of any study in this ... @@ -787,7 +788,7 @@ the new contributions. ... @@ -787,7 +788,7 @@ the new contributions. mentions $n_o$ which does not appear in the theorem statement. mentions $n_o$ which does not appear in the theorem statement. \begin{answer} \begin{answer} We changed the notation of the judgments so that it now explicitly We changed the notation of the judgments so that it now explicitly mentions the ${n_o}$ (see p15l??-??) mentions the ${n_o}$ (see p15) \end{answer} \end{answer} \item Section \item Section ... @@ -947,7 +948,7 @@ failed and that after a couple of months were fixed and magically ... @@ -947,7 +948,7 @@ failed and that after a couple of months were fixed and magically worked in one or the other. worked in one or the other. We significantly extended the part in Section 5 where we explain this, We significantly extended the part in Section 5 where we explain this, by enriching it with the comments above. See p32l???-???. by enriching it with the comments above. See p32 third quarter. \end{answer} \end{answer} ... @@ -1068,7 +1069,7 @@ should be sound. In general, if you know that $x \in A$ and $(A \land ... @@ -1068,7 +1069,7 @@ should be sound. In general, if you know that$x \in A$and$(A \land \not= \emptyset$, then you certainly can't conclude that$x \in \neg B$. \not= \emptyset$, then you certainly can't conclude that $x \in \neg B$. \begin{answer} \begin{answer} We added an explanation and given a reference for a thorough We added an explanation and given a reference for a thorough discussion (see p10l??-??) discussion (see p10 center) \end{answer} \end{answer} \item \item ... ...