\subsubsection{Proof terms}

\subsubsection{Syntax for proof terms}
$$
N ::= x | \lambda x N | N_1 N_2 | \Lambda x N | N \cdot x | [ E ]_K 
$$
$$
E ::= \{ K \} N | x \ll N . E
$$


\subsubsection{Inference rules for proof terms}


$$
\inferrule
{ }
{ \Gamma , x : A \vdash x : A }
$$

$$
\inferrule
{ \Gamma , x : A \vdash t : B}
{ \Gamma \vdash \lambda x t : A \supset B}
\hspace {4em}
\inferrule
  { \Gamma \vdash t_0 : A \supset B \\ \Gamma \vdash t_1 : A }
  { \Gamma \vdash t_0 t_1 : B}
$$

$$
\inferrule
{ \Gamma \vdash t : A}
{\Gamma \vdash \Lambda x t : \forall x A}
\hspace {4em}
\inferrule
{ \Gamma \vdash t : \forall x A}
{ \Gamma \vdash t \cdot \alpha : A[x \leftarrow \alpha]}
$$

$$\inferrule
{ \Gamma \vdash t : \textsc{aff} (K, A)}
{ \Gamma \vdash [t]_K :\langle K \rangle A}
$$

$$
\inferrule
{ \Gamma \vdash t : \textsc{true} (A)}
{ \Gamma \vdash \{K\} t : \textsc{aff} (K, A) }
\hspace {4em}
\inferrule
{ \Gamma \vdash t_0 : \textsc{true} (\langle K \rangle A) \\ \Gamma, x : A \vdash t_1 : \textsc{aff} (K,B)}
{ \Gamma \vdash x \ll t_0 . t_1 : \textsc{aff} (K, B) }
$$

% \paragraph{Why a new kind of judgment?} local completness :
%% $$ \inferrule{\textsl{D}}{\Gamma \vdash A \supset B} \Rightarrow \inferrule* [Left=\textsc{impI}] { \inferrule   {}{\Gamma, A \vdash B }    } { \Gamma \vdash A \supset B} $$
