
\section{Lambda 5}

\begin{figure}[h]

$$
\inferrule* [Left=use]
{ }
{ \Gamma , M : A @ w \vdash M : A @ w}
$$

$$
\inferrule* [Left=impI]
{ \Gamma , x : A \vdash M : B}
{ \Gamma \vdash \lambda x . M : A \supset B}
\hspace {4em}
\inferrule* [Left=impE]
  { \Gamma \vdash M_1 : A \supset B \\ \Gamma \vdash M_2 : A }
  { \Gamma \vdash M_1 M_2 : B}
$$

$$
\inferrule* [Left=\textsc{atI}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{hold} M : A \, at \, \textsc w @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{atE}]
{\Gamma \vdash M : A \, at \, \textsc w' @ \textsc w \\ 
  \Gamma, A @ \textsc w' \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{leta} M \,in\, N : B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ $ \Box $ I}]
{\Gamma , \omega \hspace{0.5em} world \vdash M : A  @ \omega}
{\Gamma \vdash \textbf{box} M : \Box A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Box $ E}]
{\Gamma \vdash M : \Box A @ \textsc w}
{\Gamma \vdash \textbf{unbox} M : A @ \textsc w}
$$


$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{here} M : \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash M : \Diamond A @ \textsc w' \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{letd} \omega , x = M  \,in\, N : B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ get }]
{A \textbf{mobile} \\
 \Gamma \vdash M : A @ \textsc w'}
{\Gamma \vdash \textbf{get} [w'] M : A @ \textsc w}
$$

\end{figure}

