... ... @@ -21,7 +21,8 @@ t_1\vee\neg t_2)$\textbf{Values} & v &::=& c\alt\lambda x.e\alt (v,v) \end{array} (no let here: can be added on a surface language later together with explicit type annotation$e:t$that are checked by bidirectional typing) \subsubsection{Type Tests for values} We define$\typof c = \basic{c}$,$\typof {\lambda x.e} = \Empty\to\Any$,$\typof{(v_1,v_2)}=\typof{v_1}\times\typof{v_2}$. Finally$v\in t$iff ... ... @@ -141,8 +142,8 @@ Variant with more compact derivations: For annotations we write$\{t_1,\ldots{,} t_n\}$for$\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}$and just$t$for$\{\ann\varnothing{t}\}$. So for instance we write$\lambda x{:}t.e$for$\lambda x{:}\{\ann\varnothing{t}\}.e$and$\letexp{x{:}\{t_1,\ldots{,} t_n\}}{e}{e}$instead of$\letexp{x{:}\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}}{e}{e}$x{:}t.e$ for $\lambda x{:}\{\ann\varnothing{t}\}.e$ while $\letexp{x{:}\{t_1,\ldots{,} t_n\}}{e}{e}$ stands for $\letexp{x{:}\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}}{e}{e}$ \subsubsection{Algorithmic typing rules} This system correspond to the variant with more compact derivations. \begin{mathpar} ... ... @@ -229,7 +230,9 @@ $t'\leq t$, and $\Gamma\vdashA e': t'$ \subsubsection{Preservation of the reductions} Write the reduction rule for let and then note that $e\reduces e'$ if and only if $\eras e \reduces \eras{e}$ (details to be checked, should we rather use $v$?) (details to be checked, should we rather use $v$? Probably we have $\eras e \reduces \eras{e}\Longrightarrow e\reduces^{0|1} e'$ and $e\reduces e'\Longrightarrow \eras e \reduces^+ \eras{e}$) \subsection{Normalization} ... ...