\documentclass[t,red,compress]{beamer}

\usepackage[utf8]{inputenc}

\title{Not So Fresh ML}

\author{Nicolas Pouillard and François Pottier}

\institute{\texttt{\{Nicolas.Pouillard,Francois.Pottier\}@inria.fr}}

\date{CANS Seminar, 2009}

\beamertemplatenavigationsymbolsempty

\useoutertheme{default}

\useinnertheme[shadow=true]{rounded}

\usecolortheme{orchid}


        \defbeamertemplate*{footline}{infolines theme without institution}
        {
          \leavevmode%
          \hbox{%
            \begin{beamercolorbox}[wd=.34\paperwidth,ht=2.25ex,dp=1.125ex,center]{author in head/foot}%
              \usebeamerfont{author in head/foot}
              \insertshortauthor
            \end{beamercolorbox}%
            \begin{beamercolorbox}[wd=.36\paperwidth,ht=2.25ex,dp=1.125ex,center]{title in head/foot}%
              \usebeamerfont{title in head/foot}
              \insertshorttitle
            \end{beamercolorbox}%
            \begin{beamercolorbox}[wd=.30\paperwidth,ht=2.25ex,dp=1.125ex,right]{date  in head/foot}%
              \usebeamerfont{date in head/foot}
              \insertshortdate{}\hspace*{2em}
              \insertframenumber{}\hspace*{2ex}
            \end{beamercolorbox}}%
          \vskip0pt%
        }
  

\setbeamersize{text margin left=0.30cm}

\setbeamersize{text margin right=0.30cm}

\usepackage[]{amsmath}
\begin{document}
\maketitle

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Towards safer and more expressive languages for meta-programming}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Program representation should stay well-typed and \alert{well-scoped}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{Pursuing the work on \textsc{FreshML}}

\vfill

\begin{itemize}
\item

Inspired from \textsc{FreshML}

\item

pure \textsc{FreshML} for its safety

\item

C$ \alpha $ml for its expressiveness
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries A taste of \textsc{FreshML}/C$ \alpha $ml}
\end{center}

\vfill
\end{frame}

\begin{frame}<1>[label=dataTerm]
\frametitle{Data type for explicitly typed lambda calculus}

\vfill

\begin{block}{}
\only<1>{data\mbox{\hspace{0.50em}}Term{\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}Atom{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}Term{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}\textless{}\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \times $\mbox{\hspace{0.50em}}neutral\mbox{\hspace{0.50em}}Ty\mbox{\hspace{0.50em}}$ \times $\mbox{\hspace{0.50em}}inner\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}\textgreater{}{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}\textless{}\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \times $\mbox{\hspace{0.50em}}outer\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \times $\mbox{\hspace{0.50em}}inner\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}\textgreater{}{\newline}}\only<2>{data\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}outer{\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}outer){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}outer)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}outer){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $inner.\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}inner)\mbox{\hspace{0.50em}}Ty\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}inner){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $inner.\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}inner)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}outer)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}inner){\newline}}\only<3>{data\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}Ty\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \beta $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \beta $){\newline}}\only<4>{data\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}Ty\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \beta $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \beta $){\newline}}\only<5>{data\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}$ \alpha $\textless{}$ \lambda $$ \beta $$ \rightarrow $\mbox{\hspace{0.50em}}(Ty,\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \beta $)\textgreater{}{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}$ \alpha $\textless{}$ \lambda $$ \beta $$ \rightarrow $\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \alpha $,\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \beta $)\textgreater{}{\newline}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Capture avoiding substitution}

\vfill

\begin{block}{}
subst\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}(Atom,\mbox{\hspace{0.50em}}Term)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term{\newline}subst\mbox{\hspace{0.50em}}(a,\mbox{\hspace{0.50em}}v)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}go{\newline}\mbox{\hspace{1em}}where{\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}b)\mbox{\hspace{3.50em}}$ {=} $\mbox{\hspace{0.50em}}if\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}then\mbox{\hspace{0.50em}}v\mbox{\hspace{0.50em}}else\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}b{\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{2.50em}}$ {=} $\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}t)\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}(Lam\textless{}b,ty,t\textgreater{})\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}Lam\textless{}b,\mbox{\hspace{0.50em}}ty,\mbox{\hspace{0.50em}}go\mbox{\hspace{0.50em}}t\textgreater{}{\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}(Let\textless{}b,t,u\textgreater{})\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}Let\textless{}b,\mbox{\hspace{0.50em}}go\mbox{\hspace{0.50em}}t,\mbox{\hspace{0.50em}}go\mbox{\hspace{0.50em}}u\textgreater{}{\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Computing the size of a term}

\vfill

\begin{block}{}
size\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Int{\newline}size\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}\_)\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}1{\newline}size\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{2em}}$ {=} $\mbox{\hspace{0.50em}}1\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}size\mbox{\hspace{0.50em}}(Lam\textless{}\_,\_,t\textgreater{})\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}3\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t{\newline}size\mbox{\hspace{0.50em}}(Let\textless{}\_,t,u\textgreater{})\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}3\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries \textsc{FreshML} considered \visible<2>{\alert{too fresh}}!}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{More efficient programs}

\vfill

\begin{block}{Freshening is useless while$:$}
\begin{itemize}[<+->]
\item

Computing the size of a term

\item

Computing free variables

\item

Typing some languages

\item

Counting occurrences of some variable

\item

Substituting closed terms for variables

\item

Deciding $ \alpha $-equivalence

\item

...
\end{itemize}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{To freshen or not to freshen?}

\vfill

\begin{itemize}[<+->]
\item

While \textsc{FreshML} implicitly freshen

\item

This system allows both non-freshening and freshening openings

\item

However we will only the non-freshening part
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries World-index types for atoms}

\vfill

\visible<2>{let\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}in\mbox{\hspace{0.50em}}x}
\end{center}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Let's classify atoms by a world they live in}

\vfill

\begin{block}{The type of atoms is now indexed by a world}
type\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $
\end{block}

\begin{block}{Equality is homogeneous and prevents mixing worlds}
$ \text{{\char `\(}$ \equiv ${\char `\)}}_{\text{Atom}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool
\end{block}

\vfill
\end{frame}

\againframe<1,2,3>{dataTerm}

\begin{frame}[<+->]
\frametitle{Worlds are closely related to each other}

\vfill

\begin{block}{The type of (oriented) links between worlds}
type\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $
\end{block}

\begin{block}{Links holds the set of atoms as a frontier}
$ \alpha\stackrel{{\scriptscriptstyle \left(\notin{S}\right)}}{\vartriangleright}\beta $
\end{block}

\begin{block}{}
\begin{center}
\alert{Links are supposed to be invisible/inferred!}
\end{center}
\end{block}

\vfill
\end{frame}

\againframe<3,4>{dataTerm}

\begin{frame}[<+->]
\frametitle{Link operations}

\vfill

\begin{block}{Identity link}
$ \text{id}_{\text{Link}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $
\end{block}

\begin{block}{Link composition}
$ \text{{\char `\(}$ \circ ${\char `\)}}_{\text{Link}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma $.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \gamma $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \alpha $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \alpha $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \gamma $)
\end{block}

\begin{block}{Atomic link}
$ \text{atomic}_{\text{Link}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \alpha $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)
\end{block}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Casts to walk through links}

\vfill

\begin{block}{Atomic casts}
$ \text{cast}_{\text{Atom}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $)
\end{block}

\begin{block}{Generalized casts}
$ \text{cast}_{\text{f}} $\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}f.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}(f\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}f\mbox{\hspace{0.50em}}$ \alpha $)
\end{block}

\begin{block}{}
\begin{center}
\alert{Cast implies proof obligations or dynamic checks!}
\end{center}
\end{block}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Atom abstraction as existential quantification}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{Hiding the real world but keeping a link}

\vfill

\begin{block}{}
data\mbox{\hspace{0.50em}}$ \alpha $\textless{}f\textgreater{}\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Abs\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}(f\mbox{\hspace{0.50em}}$ \beta $)
\end{block}

\vfill
\end{frame}

\againframe<4,5>{dataTerm}

\begin{frame}[<+->]
\frametitle{Making an abstraction}

\vfill

\begin{block}{}
Abs\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}f.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}f\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\textless{}f\textgreater{}
\end{block}

\begin{block}{}
Lam\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $
\end{block}

\begin{block}{}
mkLam\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha ${\newline}mkLam\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}(atomic\mbox{\hspace{0.50em}}x)\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t
\end{block}

\begin{block}{}
mkConst\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}mkLam\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}(mkLam\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}x))
\end{block}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Opening an abstraction does not freshen it}

\vfill

\begin{block}{}
\mbox{\hspace{0.50em}}let\mbox{\hspace{0.50em}}(Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}in\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}
\end{block}

\begin{block}{}
$ \Gamma $\mbox{\hspace{0.50em}}$ \vdash $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}$ \alpha $\textless{}f\textgreater{}\mbox{\hspace{0.50em}}where\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \in $\mbox{\hspace{0.50em}}$ \Gamma $
\end{block}

\begin{block}{}
$ \Gamma $,$ \beta $,lnk$:$$ \beta $$ \vartriangleright $$ \alpha $,x$:$Atom\mbox{\hspace{0.50em}}$ \beta $,y$:$f\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \vdash $\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}$ \tau $\mbox{\hspace{0.50em}}where\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}\#\mbox{\hspace{0.50em}}$ \tau $
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Safety Properties}

\vfill

\begin{itemize}[<+->]
\item

Well-typed programs do not get stuck

\item

$ \alpha $-equivalence is preserved by casts

\item

Casts may dynamically fail or be proven successful

\item

$ \alpha $-equivalence is defined structurally on types
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\frametitle{Example commuting abstraction with pairs}

\vfill

\begin{block}{}
commute\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}$ \alpha $\textless{}$ \lambda $$ \beta $$ \rightarrow $\mbox{\hspace{0.50em}}(Term\mbox{\hspace{0.50em}}$ \beta $,\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \beta $)\textgreater{}{\newline}\mbox{\hspace{9em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \alpha $\textless{}Term\textgreater{},\mbox{\hspace{0.50em}}$ \alpha $\textless{}Term\textgreater{}){\newline}commute\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$ {=} ${\newline}\mbox{\hspace{1em}}let\mbox{\hspace{0.50em}}(Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}(y,z))\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}t{\newline}\mbox{\hspace{1em}}in\mbox{\hspace{0.50em}}(Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y,\mbox{\hspace{0.50em}}Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}z){\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Name capture does not type-check}

\vfill

\begin{block}{}
wrong\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}$ \alpha $\textless{}Term\textgreater{}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\textless{}Term\textgreater{}{\newline}wrong\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}$ {=} ${\newline}\mbox{\hspace{1em}}let\mbox{\hspace{0.50em}}(Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}t{\newline}\mbox{\hspace{1em}}in\mbox{\hspace{0.50em}}Abs\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}u{\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Computing the size of a term}

\vfill

\begin{block}{}
size\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Int{\newline}size\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}\_)\mbox{\hspace{3.50em}}$ {=} $\mbox{\hspace{0.50em}}1{\newline}size\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{2.50em}}$ {=} $\mbox{\hspace{0.50em}}1\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}size\mbox{\hspace{0.50em}}(Lam\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}t)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}3\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t{\newline}size\mbox{\hspace{0.50em}}(Let\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}3\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}+\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}
\end{block}

\begin{block}{}
\begin{center}
\alert{Polymorphic recursion!}
\end{center}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Computing free variables}

\vfill

\begin{block}{}
\only<1>{remove\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}{[}Atom{]}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}{[}Atom{]}{\newline}remove\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}{[}{]}\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}{[}{]}{\newline}remove\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(b$:$bs){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}bs{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}otherwise\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}bs{\newline}}\only<2>{remove\mbox{\hspace{0.50em}}$:$$:${\newline}\mbox{\hspace{1.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}{[}Atom\mbox{\hspace{0.50em}}$ \beta ${]}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}{[}Atom\mbox{\hspace{0.50em}}$ \alpha ${]}{\newline}remove\mbox{\hspace{0.50em}}\_\mbox{\hspace{1.50em}}\_\mbox{\hspace{0.50em}}{[}{]}\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}{[}{]}{\newline}remove\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(b$:$bs){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}bs{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}otherwise\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}cast\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}bs{\newline}}
\end{block}

\begin{block}{}
\only<1>{fv\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}{[}Atom{]}{\newline}fv\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}a)\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}{[}a{]}{\newline}fv\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{2em}}$ {=} $\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}++\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}u{\newline}fv\mbox{\hspace{0.50em}}(Lam\textless{}a,\_,t\textgreater{})\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(fv\mbox{\hspace{0.50em}}t){\newline}fv\mbox{\hspace{0.50em}}(Let\textless{}a,t,u\textgreater{})\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}++\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(fv\mbox{\hspace{0.50em}}u){\newline}}\only<2>{fv\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{1em}}{[}Atom\mbox{\hspace{0.50em}}$ \alpha ${]}{\newline}fv\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}a)\mbox{\hspace{4.50em}}$ {=} $\mbox{\hspace{0.50em}}{[}a{]}{\newline}fv\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{3.50em}}$ {=} $\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}++\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}u{\newline}fv\mbox{\hspace{0.50em}}(Lam\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}t)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(fv\mbox{\hspace{0.50em}}t){\newline}fv\mbox{\hspace{0.50em}}(Let\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}++\mbox{\hspace{0.50em}}remove\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(fv\mbox{\hspace{0.50em}}u){\newline}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Looking up an environment}

\vfill

\begin{block}{}
data\mbox{\hspace{0.50em}}Env\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}Empty{\newline}\mbox{\hspace{5.50em}}\textbar{}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Snoc\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Env\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}(Atom\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}Ty{\newline}
\end{block}

\begin{block}{}
lookupEnv\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Env\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Ty{\newline}lookupEnv\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(Snoc\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}ty){\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}b\mbox{\hspace{2em}}$ {=} $\mbox{\hspace{0.50em}}ty{\newline}\mbox{\hspace{1em}}\textbar{}\mbox{\hspace{0.50em}}otherwise\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}lookupEnv\mbox{\hspace{0.50em}}(cast\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a)\mbox{\hspace{0.50em}}env{\newline}lookupEnv\mbox{\hspace{0.50em}}\_\mbox{\hspace{0.50em}}Empty\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}error\mbox{\hspace{0.50em}}"unbound\mbox{\hspace{0.50em}}value"{\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Typing a term}

\vfill

\begin{block}{}
typing\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Env\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Ty{\newline}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}v){\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}lookupEnv\mbox{\hspace{0.50em}}v\mbox{\hspace{0.50em}}env{\newline}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}(Lam\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}ty\mbox{\hspace{0.50em}}t){\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}ty\mbox{\hspace{0.50em}}`TyArrow`\mbox{\hspace{0.50em}}typing\mbox{\hspace{0.50em}}(Snoc\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}ty)\mbox{\hspace{0.50em}}t{\newline}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}(Let\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}typing\mbox{\hspace{0.50em}}(Snoc\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}(typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}t))\mbox{\hspace{0.50em}}u{\newline}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}case\mbox{\hspace{0.50em}}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}of{\newline}\mbox{\hspace{3em}}from\mbox{\hspace{0.50em}}`TyArrow`\mbox{\hspace{0.50em}}to\mbox{\hspace{0.50em}}\textbar{}\mbox{\hspace{0.50em}}from\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}typing\mbox{\hspace{0.50em}}env\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}to{\newline}\mbox{\hspace{3em}}\_\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}error\mbox{\hspace{0.50em}}"ill\mbox{\hspace{0.50em}}typed"{\newline}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Challenges and future work}

\vfill

\begin{itemize}[<+->]
\item

Deeper formalization and proofs

\item

$ \alpha $-equivalence for inside-out abstractions

\item

Better understanding of heterogeneous comparison

\item

Integrating complex binding structures

\item

Properties implied by world polymorphism
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\frametitle{Conclusion}

\vfill

\begin{itemize}[<+->]
\item

Explicit scopes using world indices

\item

Non-freshening opening

\item

Atom abstraction as existential quantification

\item

Expressivness close to a manual model with names
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Questions?}
\end{center}

\vfill
\end{frame}

\appendix

\againframe{dataTerm}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Polymorphic values represent closed terms}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries A more direct presentation of atom sorts}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Generalizing C$ \alpha $ml data structures}
\end{center}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Picking fresh atoms}

\vfill

\begin{block}{}
fresh\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}in\mbox{\hspace{0.50em}}t\visible<3>{\texttt{\mbox{\hspace{5.50em}}where\mbox{\hspace{0.50em}}x}\#$ \left(\text{\texttt{t}}\Downarrow\right) $}
\end{block}

\begin{itemize}[<+->]
\item

The atom can be used in the world you like

\item

Same proof obligation as in pure \textsc{FreshML}
\end{itemize}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Picking fresh atoms (second version)}

\vfill

\begin{block}{}
fresh\mbox{\hspace{0.50em}}x,lnkExp,lnkImp\mbox{\hspace{0.50em}}in\mbox{\hspace{0.50em}}t
\end{block}

\begin{block}{}
$ \Gamma $,$ \beta $,lnkExp$:$$ \beta $$ \vartriangleright $$ \alpha $,lnkImp$:$$ \alpha $$ \vartriangleright $$ \beta $,x$:$Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \vdash $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}$ \tau ${\newline}\mbox{\hspace{1.50em}}where\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \in $\mbox{\hspace{0.50em}}$ \Gamma $,\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}\#\mbox{\hspace{0.50em}}$ \tau $
\end{block}

\begin{itemize}[<+->]
\item

The fresh atom is in an existential world

\item

Links are provided to import and export things

\item

Proof obligations relied to casts
\end{itemize}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Freshening is still available}

\vfill

\begin{block}{}
\mbox{\hspace{0.50em}}let\mbox{\hspace{0.50em}}(Abs\mbox{\hspace{0.50em}}\_lnk\mbox{\hspace{0.50em}}(fresh\mbox{\hspace{0.50em}}x)\mbox{\hspace{0.50em}}y)\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}in\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}
\end{block}

\begin{block}{Freshening allows to use the same world}
$ \Gamma $\mbox{\hspace{0.50em}}$ \vdash $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}$ \alpha $\textless{}f\textgreater{}\mbox{\hspace{0.50em}}where\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \in $\mbox{\hspace{0.50em}}$ \Gamma $

$ \Gamma $,\_lnk$:$$ \alpha $$ \vartriangleright $$ \alpha $,x$:$Atom\mbox{\hspace{0.50em}}$ \alpha $,y$:$f\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \vdash $\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}$:$\mbox{\hspace{0.50em}}$ \tau $
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Precise control over scopes}

\vfill

\begin{block}{Having explicit world subsume$:$}
\begin{itemize}[<+->]
\item

C$ \alpha $ml inner/outer/neutral annotations

\item

C$ \alpha $ml pattern types/expression types distinction

\item

\textsc{FreshML}/C$ \alpha $ml atom sorts
\end{itemize}
\end{block}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Safe heterogeneous comparison!}
\end{center}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Safe heterogeneous comparison!}

\vfill

\begin{block}{}
atmEqH\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Atom\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \beta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool
\end{block}

\begin{block}{}
atmEqH\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}\textbar{}\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}$ \notin $\mbox{\hspace{0.50em}}lnk\mbox{\hspace{1em}}$ {=} $\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}cast\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}b{\newline}\mbox{\hspace{7.50em}}\textbar{}\mbox{\hspace{0.50em}}otherwise\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}False
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Substituting closed terms for variables}

\vfill

\begin{block}{}
substClosed\mbox{\hspace{0.50em}}$:$$:${\newline}\mbox{\hspace{2em}}$ \forall $\mbox{\hspace{0.50em}}$ \alpha $.\mbox{\hspace{0.50em}}Atm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}($ \forall $\mbox{\hspace{0.50em}}$ \beta $.\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \beta $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \alpha ${\newline}substClosed\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}v\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}go\mbox{\hspace{0.50em}}id{\newline}\mbox{\hspace{1em}}where{\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}$:$$:$\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}$ \delta $.\mbox{\hspace{0.50em}}($ \delta $\mbox{\hspace{0.50em}}$ \vartriangleright $\mbox{\hspace{0.50em}}$ \alpha $)\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \delta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Term\mbox{\hspace{0.50em}}$ \delta ${\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}(Var\mbox{\hspace{0.50em}}b)\mbox{\hspace{0.50em}}\textbar{}\mbox{\hspace{0.50em}}atmEqH\mbox{\hspace{0.50em}}a\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}$ {=} $\mbox{\hspace{0.50em}}v{\newline}\mbox{\hspace{9.50em}}\textbar{}\mbox{\hspace{0.50em}}otherwise\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}Var\mbox{\hspace{0.50em}}b{\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}(App\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}App\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}t)\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}(Lam\mbox{\hspace{0.50em}}lnk'\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}ty\mbox{\hspace{0.50em}}t){\newline}\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}Lam\mbox{\hspace{0.50em}}lnk'\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}ty\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}(lnk\mbox{\hspace{0.50em}}$ \circ $\mbox{\hspace{0.50em}}lnk')\mbox{\hspace{0.50em}}t){\newline}\mbox{\hspace{2em}}go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}(Let\mbox{\hspace{0.50em}}lnk'\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u){\newline}\mbox{\hspace{3em}}$ {=} $\mbox{\hspace{0.50em}}Let\mbox{\hspace{0.50em}}lnk'\mbox{\hspace{0.50em}}b\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}t)\mbox{\hspace{0.50em}}(go\mbox{\hspace{0.50em}}(lnk\mbox{\hspace{0.50em}}$ \circ $\mbox{\hspace{0.50em}}lnk')\mbox{\hspace{0.50em}}u)
\end{block}

\vfill
\end{frame}
\end{document}