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

For every type environment $\Gamma$ and \emph{positive} expression $e$, if

$\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

of Theorem~\ref{th:algosound} to give a more precise characterization

of terms for which our algorithm is complete. The system $\vdashAts$

We can use the algorithmic system $\vdashAts$ defined for the proof

of Theorem~\ref{th:algosound} to give a far more precise characterization

of the terms for which our algorithm is complete. The system $\vdashAts$

copes with negated arrow types but it still is not

complete essentially for two reasons: $(i)$ the recursive nature of

rule \Rule{Path} and $(ii)$ the use of nested \Rule{PAppL} that yield

...

...

@@ -413,9 +413,9 @@ left-hand side of another negated arrow.

\begin{theorem}[Partial Completeness]

For every $\Gamma$, $e$, $t$, if $\Gamma\vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that $\Gamma\vdashA e: t'$ and $t'\leq t$.

\end{theorem}

\noindent This last result is only of theoretical interest since in

practice one will implement languages with positive

expressions only. This is why for our implementation we use the CDuce

\noindent This last result is only of theoretical interest since, in

practice, we expect to have only languages with positive

expressions. This is why for our implementation we use the CDuce

library in which type schemes are absent and functions are typed only

by intersections of positive arrows. We present the implementation in

Section~\ref{sec:practical} but before let us study some extensions.

Section~\ref{sec:practical}, but before we study some extensions.

@@ -84,8 +84,8 @@ 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 most specific type (mst): the mst of $c$ is $\basic c$; the mst 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 mst of a pair of values is the product of the mst of the

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).

the mst of a pair of values is the product of the mst's of the

values. We write $v\in t$ if the most specific type of $v$is a subtype of $t$(see Appendix~\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).

...

...

@@ -164,7 +164,7 @@ core and the use of subtyping, given by the following typing rules:\vspace{-1mm}

{}

\qquad\vspace{-3mm}

\end{mathpar}

These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice that we used a classic subsumption rule (i.e., \Rule{Subs}) to embed subtyping in the type system. Let us next focus on the unconventional aspects of our system, from the simplest to the hardest.

These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice subtyping is embedded in the system by the classic \Rule{Subs} subsumption rule. Next we focus on the unconventional aspects of our system, from the simplest to the hardest.

The first unconventional aspect is that, as explained in

Section~\ref{sec:challenges}, our type assumptions are about