Commit 7d2aa75a authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typos

parent 113291fc
...@@ -26,24 +26,24 @@ the argument has type {\tt Number}, and when the output is {\tt false}, the ...@@ -26,24 +26,24 @@ the argument has type {\tt Number}, and when the output is {\tt false}, the
argument does not. Such information is used selectively argument does not. Such information is used selectively
in the ``then'' and ``else'' branches of a test. in the ``then'' and ``else'' branches of a test.
\rev{%%%% \rev{%%%%
Since \citet{THF10} focus they analysis on a particular set of pure Since \citet{THF10} focus their analysis on a particular set of pure
operations, their approach works also in the presence of side-effects. Although operations, the approach works also in the presence of side-effects. Although
the choices made by our and their approach seems diametrically opposed the choices made by our and their approach seem poles apart
(the Boolean output of few pure operations vs.\ any output of any (Boolean output of few pure operations vs.\ any output of every
expression), they share some similar techniques. For instance, our expression), they share some similar techniques. For instance, our
deduction system for $\vdashp$ plays a similar role as deduction system for $\vdashp$ plays a similar role as
the proof systems and \textsf{update} function of \citet[Figures 4, the proof systems and \textsf{update} function of \citet[Figures 4,
7 \& 9]{THF10}. In that framework, when one needs to type a variable 7 \& 9]{THF10}. In that framework, in order to type a variable
(judgemetn ``$\Gamma \vdash x:\tau$''), one has to be able to prove (judgement ``$\Gamma \vdash x:\tau$'') one needs to prove
that the logical formula $\tau_x$ holds (under the hypotheses of that the logical formula $\tau_x$ holds (under the hypotheses of
$\Gamma$). This atomic formula may not be directly available in $\Gamma$). This atomic formula may not be directly available in
$\Gamma$ but may $\Gamma$ but may
be proven by a combination of logical deduction rules (Figure~4), or be proven by a combination of logical deduction rules (Figure~4 of~\cite{THF10}), or
by recursively exploring a path leading to $x$ (Figure~7 and ~9) a by recursively exploring a path leading to $x$ (Figure~7 and ~9 of~\cite{THF10}) a
path being a sequence of \textbf{cdr} or \textbf{car} applications, path being a sequence of \textbf{cdr} or \textbf{car} applications,
much like our $f$ and $s$ components of paths. This idea is also much like our $f$ and $s$ components of paths. This idea is also
present in our $\vdashp$ with differences pertaining to our type present in our deduction system for $\vdashp$ with differences pertaining to our type
framework and design choices : type restrictions can be encoded using framework and design choices: type restrictions can be encoded using
set-theoretic intersections and negations (instead of meta-functions working on the set-theoretic intersections and negations (instead of meta-functions working on the
syntax of types) and our richer language of paths components. syntax of types) and our richer language of paths components.
}%%%%rev }%%%%rev
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment