
% -- Types of Terms -------------------------------------------------------------------------------
\begin{figure}
\boxfig{
\begin{center}
\fbox{ $\tyJudge {\Gamma} {\Sigma} {t} {\tau} {\sigma}$ }
\end{center}

\[
	\ruleAL	{TyUnit}
		{ \tyJudgeGS {()} {()} {\bot} }
\]

\[	\ruleAL	{TyVar}
		{\tyJudge
			{\Gamma, \ x : \tau} 
			{\Sigma} 
			{x} 
			{\tau} 
			{\bot}}
	\quad\quad\quad
	\ruleAL	{TyLoc}
		{\tyJudge
			{\Gamma}
			{\Sigma, \ l : \tau } 
			{l \ \:}
			{\tau}
			{\bot}}
\]

\[	\ruleIL	{TyAbsT}
		{\tyJudge
			{\Gamma, \ a : \kappa \: }
			{\Sigma}
			{t_2}
			{\tau_2}
			{\bot}}
		{\tyJudgeGS
			{\teLAM{a}{\kappa}{t_2}}
			{\tyForall{a}{\kappa}{\tau_2}}
			{\bot}}
\]

\[	\ruleIL	{TyAbs}
		{ \tyJudge	
			{\Gamma, \ x : \tau_1 \: }
			{\Sigma}
			{t}
			{\tau_2}
			{\sigma} 
		}
		{ \tyJudgeGS
			{\teLam{x}{\tau_1}{t}}
			{\tau_1 \toa{\sigma} \tau_2}
			{\bot} 
		}
\]

\[	\ruleIL	{TyAppT}
		{  \tyJudgeGS 
			{t_1} 
			{\tyForall{a}
			{\kappa_{11}}
			{\varphi_{12}}}
			{\sigma_1} 
		   \qq
		   \kiJudgeGS
			{\varphi_2}
			{\kappa_{11}} 
		}
		{ \tyJudgeGS
			{t_1 \ \varphi_2}
			{\varphi_{12}[\varphi_2/a]}
			{\sigma_1} 
		}
\]

\[	\ruleIL	{TyApp}	
		{ \tyJudgeGS
			{t_1}
			{\tau_{11} \toa{\sigma} \tau_{12}}
			{\sigma_1} 
		  \qq
	  	  \tyJudgeGS
			{t_2}
			{\tau_{11}}
			{\sigma_2} 
		}
		{ \tyJudgeGS
			{t_1 \ t_2}
			{\tau_{12}}
			{\sigma_1 \lor \sigma_2 \lor \sigma}
		}
\]

\[	\ruleIL	{TyLetR}
		{ \begin{array}{lll}
		  &&
			\ov{\kiJudgeGS
				{\delta_i}
				{\kappa_i}}^{\ i}
		  \\
			\ov{\delta_i} \ \trm{well formed}
		  & 
			{r \notin \ifv(\tau)}
		  & 
		        \tyJudge	
				{\Gamma, \ r : \%, \ \ov{w_i : \kappa_i}}
				{\Sigma}
				{t}
				{\tau}
				{\sigma} 
		  \end{array}
		}
		{ \tyJudgeGS
			{\teLetR{r}{\ov{w_i = \delta_i}}{t}} 
			{\tau} 
			{\sigma \setminus {(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}}
		}
\]

\[	\ruleIL	{TyWithR}
		{ \un{\rho},~ \ov{\Delta_i} \in \Sigma
		  \qq 
		  \tyJudgeGS
			{t}
			{\tau}
			{\sigma}
		}
		{ \tyJudgeGS
			{\teWithR{\un{\rho}}{\ov{\Delta_i}}{t}}
			{\tau}
			{\sigma \setminus {(\iRead~ \un{\rho} \lor \iWrite~ \un{\rho} \lor \iAlloc~ \un{\rho})}}
		}
\]

\[	\ruleIL	{TyAlloc}
		{ \begin{array}{ll}
  	  		& 
	  		\ov{\tyJudgeGS
				{t}
				{\tau_i	[\varphi/r~ \ov{\varphi'/a}]}
				{\sigma_i}}^{\: i \gets 0..n} 
	  	  \\
         		\kiJudgeGS
				{\varphi}
				{\%} 
	  	  &
	  		K :: \forall(r : \%). \forall(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)
	  	 \end{array}
		}
		{ 
		  \tyJudgeGS
			{K~ \varphi~ \ov{\varphi'}~ \ov{t}}
			{T~ \varphi~ \ov{\varphi'}}
			{\sigma_0 \lor \sigma_1 ... \lor \sigma_n \lor \iAlloc~ \varphi}
		}
\]

\[	\ruleIL	{TyCase}
		{ \tyJudgeGS
			{t}
			{T \ \varphi \ \ov{\varphi'}}
			{\sigma}
		  \quad
		  \ov{\tyJudgeGS	
			{p_i \to t_i}
			{T \ \varphi \ \ov{\varphi'} \to \tau}
			{\sigma_i'}}^{\: i\; \gets\; 0..n}
		}	
		{ \tyJudgeGS
			{ \kcase \ t \ \kof \ \ov{p \to t}}
			{\tau}
			{\sigma \lor \iRead \ \varphi 
				\lor \sigma_0' \lor \sigma_1' ... \lor \sigma_n'}
		}
\]

\[	\ruleIL	{TyUpdate}
		{ \begin{array}{ll}
		  	\kiJudgeGS
				{\delta}
				{\iMutable \ \varphi}
		  &	\tyJudgeGS
				{t'}
				{\tau_i[\varphi/r~ \ov{\varphi'/a}]}{\sigma'} 
		  \\	\tyJudgeGS
				{t}
				{T \ \varphi \ \ov{\varphi'}}
				{\sigma}
		  &	K :: \forall(r : \%)(\ov{a : \kappa}). \ov{\tau} \to T \ r \ \ov{a} 
			 	\in \trm{ctorTypes}(T)
		  \end{array}
		}
		{ \tyJudgeGS
			{\iupdate_{K,i} \ \varphi \ \ov{\varphi'} \ \delta \ t \ t'}
			{()}
			{\sigma \lor \sigma' \lor \iWrite \ \varphi}
		}
\]

\[	\ruleIL	{TySuspend}	
		{ \tyJudgeGS
			{t_1}
			{\tau_{11} \toa{\sigma} \tau_{12}}
			{\sigma_1}
		  \quad
		  \tyJudgeGS
			{t_2}
			{\tau_{11}}
			{\sigma_2}
		  \quad
		  \kiJudgeGS
			{\delta}
			{\iPure \ \sigma} 
		}
		{
		  \tyJudgeGS
			{\isuspend \ \tau_{11} \ \tau_{12} \ \sigma \ \delta \ t_1 \ t_2}
			{\tau_{12}}
			{\sigma_1 \lor \sigma_2}
		}
\]

\[
	\ruleIL	{TyMaskPure}
		{ \tyJudgeGS
			{t}
			{\tau}
			{\sigma}
		  \quad
		   \kiJudgeGS
			{\delta}
			{\iPure \ \sigma'}
		}
		{ \tyJudgeGS
			{\kmask \ \delta \ \kin \ t}{\tau}{\sigma \setminus \sigma' } 
		}
\]


} % boxfig
\smallskip
\caption{Types of Terms}
\label{fig:TypesOfTerms}
\end{figure}















