First version of new language section

language2.tex

+In this section
+
+\subsection{Types}
+
+
+\subsection{Syntax}
+
+
+\subsection{Dynamic semantics}
+
+uses type schemes?
+
+\subsection{Static semantics}
+
+
+\subsection{Algorithmic system}
+
+3 ingredients:
+
+\begin{enumerate}
+\item type of functions -> type schemes
+
+\item elimination rules (app, proj,if) ->operations on types and how to compute them
+
+\item Compute the environments for occurrence typing. Algorith to compute $\Gamma\vdash\Gamma$
+\end{enumerate}
+
+Next we can give the algorithmic typing rules
+
+\subsubsection{Type schemes}
+
+
+change the definition of typeof to take into account type-schemes for lambda abstractions
+
+\subsubsection{Operators on types}
+
+\paragraph{Declarative version}
+
+\paragraph{Algorithmic version}
+
+
+\subsubsection{Type envs for occurrence typing}
+
+
+
+\subsection{Algorithmic typing rules}
+