Commit 400077b7 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 4433f062 8814e56c
......@@ -252,7 +252,8 @@ type, but also we had to build the expression that causes the
divergence in quite an \emph{ad hoc} way which makes divergence even
more unlikely: setting an $n_o$ twice the depth of the syntax tree of
the outermost type case should be enough to capture all realistic
cases.
cases. For instance, all examples given in Section~\ref{sec:practical}
can be checked (or found to be ill-typed) with $n_o = 1$.
\fi
......
......@@ -382,8 +382,9 @@ 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 \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
during a test. On difference is that with refinement types, the
information can be
kept at the level of types types, since dependent types contain terms and can
introduce variables, while in our approach the mapping is kept in an
environment. Although tracking of types for structured expressions thus
seems thus an aspect commont to different approaches to occurrence types,
......
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