\begin{figure}[ht]
% -- Symbol Classes
\boxfig{
\begin{tabbing}
MMMMM   \= Mx \= MMMMMMMM
MM 	\= M \= Mx \= MMMMMMM \kill
\textbf{Symbol Classes} \\
	   $a$, $r$, $e$, $w$ 	\> $\rightarrow$ 	\>  (type variables)  
	\> $T$			\> $\rightarrow$	\>  (data type constructors)
	\\
	   $x$, $y$		\> $\rightarrow$ 	\>  (value variables)  
	\> $K$			\> $\rightarrow$	\>  (data constructors)
	\\ $l$			\> $\rightarrow$	\>  (store locations)
	\> $\rho$		\> $\rightarrow$	\>  (region labels)
\end{tabbing}

% -- Superkinds
\begin{tabbing}
M 	\= Mx \= MMMMMMMMMMMMMMMMMMMMMMMMMMMM \= MMMMMMM \kill
\textbf{Super Kinds} \\
$\omega$ 
	\> $::=$	\> $\Box 
				~~|~~ \Diamond 
				~~|~~ \kappa \to \omega$
\end{tabbing}


% -- Kinds
\begin{tabbing}
M	\= Mx \= MMMMMMMMMMMMMMMMMMMMMM \= MMMMMMM \kill
\textbf{Kinds} \\
$\kappa$ 
	\> $::=$	\> $\kappa~ \varphi
				~~|~~ \Pi(a : \kappa_1).~ \kappa_2$ 
			\> (kinds)
	\\
	\> $~|$		\> $*  
				~~|~~ \%
				~~|~~ \ !$ 
			\> (atomic kinds) \\
	\> $~|$		\> $\iConst  
				~~|~~ \iMutable
				~~|~~ \iPure$
			\> (witness kind constructors)
\end{tabbing}


% -- Types
\begin{tabbing}
M 	\= MM \= MMMMMMMMMMMMMMMMMMMMMM \= MMMMMMM \kill
\textbf{Types} \\
$\varphi$, $\tau$, $\sigma$, $\delta$, $\Delta$ \\
	\> $::=$	\> $a  
				~~|~~ \forall (a : \kappa). \ \tau
				~~|~~ \varphi_1 \ \varphi_2$
			\> (types) 
	\\
	\> $\ |$	\> $(\to) 
				~~|~~ () 
				~~|~~ T$
			\> (data type constructors) 
	\\
	\> $\ |$	\> $\sigma_1 \lor \sigma_2 
				~~|~~ \bot
				~~|~~ \iRead 
				~~|~~ \iWrite
				~~|~~ \iAlloc$
			\> (effect type constructors) 
	\\
	\> $\ |$ 	\> $\iMkConst \ 
				| \ \iMkMutable \
				| \ \iMkPure$
			\> (witness type constructors)
	\\ 
	\> $~ |$	\> $\iMkPurifyRead 
				~~|~~ \iMkPurifyAlloc$
			\> ...
	\\
	\> $\ |$	\> $ \ \un{\rho} 
				~~|~~ \un{\rconst \ \varphi}
				~~|~~ \un{\rmutable \ \varphi}
				~~|~~ \un{\rpure \ \sigma}$
			\> (witness types) 
\end{tabbing}

% -- Terms
\begin{tabbing}
M 	\= MM \= MMMMMMMMMMMMMMMMMMMMMM \= MMMMMMM \kill
\textbf{Terms} \\
$t$ 	\> $::=$ 	\> $x ~~|~~ v
				~~|~~ t \ \varphi
				~~|~~ t_1 \ t_2$
\\
	\> $~ |$	\> $\teLetR{r}{\ov{w = \delta}}{t}$
			\> (region creation)
\\
	\> $~ |$	\> $\teWithR{\un{\rho}}{\ov{\Delta_i}}{t}$
			\> (evaluation in local region)
\\
	\> $~ |$	\> $K~ \ov{\varphi}~ \ov{t}$
			\> (alg. data allocation)
\\
	\> $~ |$	\> $\kcase \ t \ \kof \ \ov{K \ \ov{x : \tau} \to t' }$
			\> (case match)
\\
	\> $~ |$	\> $\iupdate_{K,i} \ \ov{\varphi} \ t_1 \ t_2$
			\> (destructive update of alg. data)
\\
	\> $~ |$	\> $\isuspend \ \ov{\varphi} \ t_1 \ t_2$
			\> (suspension of pure fn. application)
\\
	\> $~ |$	\> $\kmask \ \delta \ \kin \ t$
			\> (mask of pure effect)
\end{tabbing}

\begin{tabbing}
MMM 	\= MM \= MMMMMMMMMMMMMMMMMMMM \= MMMMMMM \kill
$v^\circ,u^\circ$ 
	\> $::=$	\> $v 
				~~|~~ \isuspend \ \ov{\varphi} \ v_1^\circ \ v_2^\circ$
			\> (weak values include suspensions)
\\
$v,~~ u$ \> $::=$	\> $l
				~~|~~ ()
				~~|~~ \Lambda (a : \kappa). \ t
				~~|~~ \lambda (x : \tau). \ t$
			\> (strong values cannot be reduced further)
\end{tabbing}


\begin{tabbing}
MMMMM	\= MMMMMMMMMMMM \= MMMMMMMMM \= MMMMMMMMMMMMMMMMMM \kill
\textbf{Derived Forms} 
\\
$\kappa_1 \to \kappa_2$			\> $\equalsdef~~ \Pi     (\_ : \kappa_1). \ \kappa_2$ 
\>
$\klet \ (x : \tau) = t_1 \ \kin \ t_2$ \> $\equalsdef~~ (\lambda (x : \tau). \ t_2) \ t_1$
\\
$\kappa \ \To \tau$			\> $\equalsdef~~ \forall (\_ : \kappa).   \ \tau$
\> $t_1 ~;~ t_2$			\> $\equalsdef~~ \klet~ (\_ : ()) = t_1 ~\kin~ t_2$
\\
\>				
\> $\kletregion \ r \ \kin \ t$		\> $\equalsdef~~ \kletregion \ r \ \kwith \ \emptyset \ \kin \ t$
\end{tabbing}

\begin{tabbing}
MM \= MMMMMMMMMMMMMMM \= M \= \kill
\textbf{Type Environment} \> \>
\textbf{Store Typing} \\
$\Gamma$	\> $::= \Gamma_1,~ \Gamma_2 
			~~|~~ a : \kappa 
			~~|~~ x : \tau$ 
		\>
$\Sigma$	\> $::= \Sigma_1,~ \Sigma_2
			~~|~~ l : \tau
			~~|~~ \un{\rho} 
			~~|~~ \un{\rconst~ \rho}
			~~|~~ \un{\rmutable~ \rho}$
\end{tabbing}

} % boxfig
\smallskip
\caption{Core Language}
\label{fig:core-language}
\end{figure}
