Commit da6baca7 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typos

parent 2fb410b1
......@@ -472,12 +472,8 @@ presentation.
\fi
%
To ease the presentation all the proofs are
omitted from the main text and can be found in the appendix
\ifsubmission
joint to the submission as supplemental material.
\else
available online.
\fi
omitted from the main text and can be found in the appendix.
\iflongversion
\subsubsection*{Contributions}
......
......@@ -56,6 +56,7 @@
\withcommentsfalse
\newif\ifsubmission
\submissiontrue
\submissionfalse
\newif\iflongversion
\longversiontrue
%\longversionfalse
......
\rev{We present in this section preliminary results obtained by our
implementation. After giving some technical highlights, we focus on
demonstrating the behaviour of our typing algorithm on meaningful
demonstrating the behavior of our typing algorithm on meaningful
examples. We also provide an in-depth comparison with the fourteen
examples of \cite{THF10}}.
......@@ -22,12 +22,12 @@ Appendix~\ref{app:optimize}.
The implementation is rather crude and consists of 2000 lines of OCaml code,
including parsing, type-checking of programs, and pretty printing of
types. \rev{CDuce is used as a library to provide set-theoretic types and
semantic subtyping. The implementation faithfully transcribe in OCaml
semantic subtyping. The implementation faithfully transcribes in OCaml
the algorithmic system $\vdashA$ as well as all the type operations
defined in this work. One optimization that our implementation
features (with respect to the formal presentation) is the use of a
memoization environment in the code of the $\Refine {e,t}{\Gamma}$
function, that avoids unnecessary traversals of $e$.
function, which allows the inference to avoid unnecessary traversals of $e$.
}
\subsection{Experiments}
......@@ -45,10 +45,6 @@ annotations.
It should be noted that for all the examples we present, the
time for the type inference process is less than 5ms, hence we do not report
precise timings in the table. These and other examples can be tested in the
\ifsubmission
anonymized
\else
\fi
online toplevel available at
\url{https://occtyping.github.io/}%
\input{code_table}
......@@ -382,7 +378,7 @@ simple example:}
if x is String then concat x y else add x y
\end{alltt}
\rev{%%%
The definition above does not type-check in any system, and rightly
The definition above does not type-check in any available system, and rightly
does so since nothing ensures
that \code{x} and \code{y} will be either both strings (so
that \code{concat} does not fail) or both integers (so that \code{add}
......@@ -399,13 +395,13 @@ this function type-checks in our system (and, of course, in Typed
Racket as well) but the corresponding type-annontated version in JavaScript
}%%%rev
\begin{alltt}\color{darkblue}
function sum (x : [string,string]|[number,number]) \{
if (typeof x[0] === "string") \{
return x[0].concat(x[1]);
\} else \{
return x[0] + x[1];
function sum (x : [string,string]|[number,number]) \{
if (typeof x[0] === "string") \{
return x[0].concat(x[1]);
\} else \{
return x[0] + x[1];
\}
\}
\}
\end{alltt}
\rev{%%%%
is rejected both by Flow and TypeScript since their type analyses fail to detect the
......
......@@ -255,7 +255,7 @@ of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information
is not propagated to the outer context.
A similar approach is taken by \citet{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
appear in a logical formula (whereas previous work only allowed formulae
appear in a logical formula (whereas previous work only allowed formul\ae
on ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types.
......@@ -282,7 +282,7 @@ so that they share the same binding, something that a plain A-normalization
does not provide (and which, actually, must not provide, since in that
case the transformation may not preserve the reduction semantics).
Amongst the work on refinement types, some have studied the extensions
Among the work on refinement types, some have studied the extensions
of a refinement type-system with intersection types. For
instance, \cite{BHM14} studies a type system with refinement types,
polymorphism and full union and intersection (but no negation). While
......@@ -292,13 +292,13 @@ present, as well as the associated type-system is a $\lambda$-calculus
with pattern-matching, let bindings, and a refining test for equality
(as well as protocol-oriented constructs such as channel creation,
message passing, and expression forking). While on the surface their
types ressemble ours, they follow another direction. First, their
types resemble ours, they follow another direction. First, their
language is fully annotated (meaning that, for instance, polymorphic terms must
be intantiated explicitely and intersection types must also be given
be explicitly instantiated and intersection types must also be specified
through an annotation). Second, since the subtyping relation they
provide is syntactic, it cannot in general take into account the
distributivity of logical connectives with respect to type constructors. This
limitation is hovever not a problem since the main goal of their
limitation is however not a problem since the main goal of their
subtyping relation is to propagate a \emph{kinding} information that
they use to characterize the level of knowledge an attacker may have
about a particular value.
......
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