\begin{figure}

\boxfig{
\begin{center}
\fbox{ $\kiJudge{\Gamma}{\Sigma}{\varphi}{\kappa}$ } \\
\end{center}

% -- Ambient Rules ------------------------------------------------------------
\[
	\ruleAL	{KiBot}
		{ \kiJudge
			{\Gamma}
			{\Sigma}
			{ \bot }
			{ \ ! }
		}
	\quad\quad\quad
	\ruleAL	{KiVar}
		{\kiJudge
			{\Gamma,~ a : \kappa}
			{\Sigma}
			{a}
			{\kappa}
		}
\]

\[	\ruleIL	{KiApp}
		{ \kiJudgeGS
			{ \varphi_1 }
			{ \kiPi{a}{\kappa_1}{\kappa_2} }
		  \quad
		  \kiJudgeGS
		  	{ \varphi_2 }
			{ \kappa_1 }
	 	}
		{ \kiJudgeGS
			{ \varphi_1 \ \varphi_2 }
			{ \kappa_2 [\varphi_2 / a] }
		}
\]

\[	\ruleIL	{KiAll}
		{ \ksJudgeGS
			{\kappa_1}
			{\omega_1}
		  \quad
		  \kiJudge
	  		{\Gamma, \ a : \kappa_1}
			{\Sigma}
			{\tau_2}
			{\kappa_2}
		}
		{ \kiJudge
			{\Gamma}
			{\Sigma}
			{ \tyForall{a}{\kappa_1}{\tau_2} }
			{ \kappa_2 }
		}
\]

\[	\ruleIL	{KiJoinEff}
		{ \kiJudgeGS
			{ \sigma_1 }
			{ \ ! }
		  \quad
		  \kiJudgeGS
		  	{ \sigma_2 }
			{ \ ! }
		}
		{ \kiJudgeGS
			{ \sigma_1 \lor \sigma_2 }
			{ \ ! }
		}
\]

\[
	\quad\quad\quad
	\ruleIL	{KiJoinPure}
		{ \kiJudgeGS
			{ \delta_1  }
			{ \iPure~ \sigma_1}
		  \quad
		  \kiJudgeGS
			{ \delta_2 }
			{ \iPure~ \sigma_2}
		}
		{ \kiJudgeGS
			{ \delta_1 \lor \delta_2 }
			{\iPure~ (\sigma_1 \lor \sigma_2)}
		}
\]
		


% -- Baked in constructors ----------------------------------------------------
\medskip
\begin{tabular}{llllll}
	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $(\to)$ 		& $::~ * \to * \to \ ! \to *$ 
\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\textrm{()}$ 	& $::~ *$ 
&	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iRead$ 	& $::~ \% \to \ !$ 
\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iInt$ 		& $::~ \% \to *$ 
&	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iWrite$ 	& $::~ \% \to \ !$ 
\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iList$ 	& $::~ \% \to * \to *$ 
&	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iAlloc$ 	& $::~ \% \to \ !$ 
\\[1ex]
	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iMkPureBot$~~	& $::~ \iPure \ \bot$	
\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iMkConst$ 	& $::~ \Pi (r : \%). \ \iConst \ r$ 
\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ &~ $\iMkMutable$~~	& $::~ \Pi (r : \%). \ \iMutable\ r$ 

\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ 	
		&~ $\iMkPurifyRead$~~~~~
		&  \mc{3}{$::~ \Pi (r : \%). \ \iConst \ r \rightarrow \ \iPure \ (\iRead \ r)$}

\\	$\Gamma \: \arrowvert \: \Sigma \judgea{K}$ 
		&~ $\iMkPurifyAlloc$~~~~~
		&  \mc{3}{$::~ \Pi (r : \%). \ \iConst \ r \rightarrow \ \iPure \ (\iAlloc \ r)$}
\end{tabular}
}
\smallskip
\caption{Kinds of Types}
\label{fig:kinds-of-types}
\end{figure}














