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

written outline, moved language2.tex to language.tex

parent 8c389e40
......@@ -388,7 +388,9 @@ an approximation thereof.
\mick{The paragraph above is not up to date.}
\beppe{Is it ok now?}
Finally, a nested check may help refining not only the types but also the type assumptions on some expressions. For instance, when typing the positive branch $e$ of
Finally, a nested check may help refining not only the types but also
the type assumptions on some expressions. For instance, when typing
the positive branch $e$ of
\begin{equation}\label{pair}
\ifty{(x,y)}{(\pair{(\Int\vee\Bool)}\Int)}{e}{...}
\end{equation}
......@@ -404,7 +406,21 @@ retyping the expression without that assumption (see rule
\Rule{Env\Aa} in Section~\ref{sec:algorules}).
\subsubsection*{Outline} Our presentation proceeds as follows
\subsubsection*{Outline} In Section~\ref{sec:language} we formalize the
ideas presented in this introduction: we define the types, the
expressions and their dynamic semantics and a type system that
implements occurrence typing together with the algorithms to decided
whether an expression is well typed in the
system. Section~\ref{sec:extensions} extends our formalism to record
types and presents two applications of our analysis: the inference of
arrow types for functions and a static analysis to reduce the number
of casts inserted by a compiler of a gradually-typed
language. Practical aspects are presented in
Section~\ref{sec:practical}. Section~\ref{sec:related} presents
related work and a discussion of future work concludes the
presentation.
For space reasons several technical definitions and all the proofs are omitted from this presentation and can be found in the appendix available online.
For space reasons several technical definitions and all the proofs are
omitted from this presentation and can be found in the appendix
available online.
......@@ -205,7 +205,7 @@
\section{Language}
\label{sec:language}
\input{language2}
\input{language}
%{\color{gray}
%\section{OLD LANGUAGE}
......@@ -225,6 +225,7 @@
%\input{polymorphism}
\section{Related work}
\label{sec:related}
\input{related}
\section{Future work and conclusion}
......
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