+\begin{frame}
+ \frametitle{Proposal (1)}
+ \begin{block}{Notation}
+ Implementation in Typed Racket\\
+ %macro language that compiles in racket BEFORE type checking
+ \texttt{$\llbracket$e$\rrbracket$}- Elaboration function on $e$\\
+ \end{block}
+ \pause%
+ \begin{block}{Curry example}
+ \begin{tabular}{rl}
+ \texttt{$\llbracket$ (curry ($\lambda$ (x y) x)) $\rrbracket$}
+ & \texttt{= (curry\_2 ($\lambda$ (x y) x))}\\
+ \pause%
+ \texttt{$\llbracket$ (curry ($\lambda$ (x y z) x)) $\rrbracket$}
+ & \texttt{= (curry\_3 ($\lambda$ (x y z) x))}\\
+ \end{tabular}
+ \end{block}
+\end{frame}