Commit 456def46 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

small typos

parent 13b291ea
......@@ -387,7 +387,7 @@ Appendix~\ref{sec:proofs_algorithmic_without_ts} for the formal
definition). Then we have:
\begin{theorem}[Completeness]
For every type environment $\Gamma$ and positive expression $e$, if
$\Gamma\vdash e: t$, then there exists $t'$ such that $\Gamma\vdashA
$\Gamma\vdash e: t$, then there exist $n_o$ and $t'$ such that $\Gamma\vdashA
e: t'$.
\end{theorem}
We can also use the algorithmic system $\vdashAts$ defined for the proof
......
......@@ -82,10 +82,10 @@ intuitively, $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a well-typed
value if for all $i{\in} I$ the hypothesis that $x$ is of type $s_i$
implies that the body $e$ has type $t_i$, that is to say, it is well
typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to
t_i$ for all $i\in I$. Every value is associated to a type: the type of $c$ is $\basic c$; the type of
t_i$ for all $i\in I$. Every value is associated to a most specific type: the type of $c$ is $\basic c$; the type of
$\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,
the type of a pair of values is the product of the types of the
values.
values. We write $v\in t$ if $t$ is a subtype of the most specific type of $v$ (see Appendix~\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).
......@@ -100,9 +100,7 @@ The dynamic semantics is defined as a classic left-to-right call-by-value reduct
\tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\[-1.3mm]
\end{array}
\]
The semantics of type-cases uses the relation $v\in t$ that we
informally defined in the previous section. We delay its formal
definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for negated arrow types). Contextual reductions are
Contextual reductions are
defined by the following evaluation contexts:\\[1mm]
\centerline{\(
%\[
......
......@@ -234,7 +234,8 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
}
@article{Bierman10,
author = {Bierman, Gavin M. and Gordon, Andrew D. and Hriundefinedcu, Cundefinedtundefinedlin and Langworthy, David},
author = {Bierman, Gavin M. and Gordon, Andrew D. and
Cătălin Hriţcu and Langworthy, David},
title = {Semantic Subtyping with an SMT Solver},
year = {2010},
issue_date = {September 2010},
......
......@@ -883,7 +883,7 @@ It allows us to have a stronger (but still partial) completeness theorem.
The proofs for the algorithmic type system presented in \ref{sec:algorules} can be derived
from the proofs of this section (see section \ref{sec:proofs_algorithmic_without_ts}).
\subsubsection{Type schemes}
\subsubsection{Type schemes}\label{app:typeschemes}
We introduce the new syntactic category of \emph{types schemes} which are the terms~$\ts$ inductively produced by the following grammar.
\[
......
......@@ -45,7 +45,7 @@ the subtyping rule presented in \cite{THF10} is unable to deduce that
$(\texttt{number}\times(\texttt{number}\cup\texttt{bool}))\cup
(\texttt{bool}\times (\texttt{number}\cup\texttt{bool}))$ is a subtype of
(and actually equal to) $((\texttt{number}\cup\texttt{bool})\times\texttt{number})\cup
((\texttt{number}\cup\texttt{bool})\times\texttt{bool})$ (and likewise for other type constructors). For record
((\texttt{number}\cup\texttt{bool})\times\texttt{bool})$ (and likewise for other type constructors combined with union types). For record
types, we also type precisely the deletion of labels, which, as far as
we know no other system can do. On the other hand, the propagation of
logical properties defined in \cite{THF10} is a powerful tool, that
......
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