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

\usepackage[]{amsmath}

\usepackage[]{amssymb}

\usepackage[T3,OT1]{fontenc}

\DeclareTextSymbol\textcrlambda{T3}{172}

\DeclareTextSymbolDefault\textcrlambda{T3}

\usepackage[]{ucs}

\usepackage[utf8x]{inputenc}

\usepackage[]{rotating}

\usepackage[]{tikz}

\usetikzlibrary{matrix,arrows}

\title{A fresh look at programming with names and binders}

\author{Nicolas Pouillard and François Pottier}

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

\date{Gallium Seminar, May 2010}

\beamertemplatenavigationsymbolsempty

\useoutertheme{default}

\useinnertheme[shadow=true]{rounded}

\usecolortheme{orchid}

\defbeamertemplate*{footline}{}
{
  \leavevmode%
  \hbox{%
    \begin{beamercolorbox}[wd=\paperwidth,ht=2.25ex,dp=1.125ex,right]{}%
      \insertframenumber{}\hspace*{2ex}
    \end{beamercolorbox}}%
  \vskip0pt%
}


\setbeamersize{text margin left=0.30cm}

\setbeamersize{text margin right=0.30cm}


\providecommand\mathbbm{\mathbb}
\DeclareUnicodeCharacter{737}{\textsuperscript{l}}
\DeclareUnicodeCharacter{8718}{\ensuremath{\blacksquare}}
\DeclareUnicodeCharacter{8759}{::}
\DeclareUnicodeCharacter{9669}{\ensuremath{\triangleleft}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
\DeclareUnicodeCharacter{10214}{\ensuremath{\llbracket}}
\DeclareUnicodeCharacter{10215}{\ensuremath{\rrbracket}}

\DeclareUnicodeCharacter{231}{\c{c}}                            % ç
\DeclareUnicodeCharacter{411}{\textcrlambda}                    % ƛ
\DeclareUnicodeCharacter{945}{\ensuremath{\alpha}}              % α
\DeclareUnicodeCharacter{946}{\ensuremath{\beta}}               % β
\DeclareUnicodeCharacter{947}{\ensuremath{\gamma}}              % γ
\DeclareUnicodeCharacter{948}{\ensuremath{\delta}}              % δ
\DeclareUnicodeCharacter{949}{\ensuremath{\epsilon}}            % ε
\DeclareUnicodeCharacter{953}{\ensuremath{\iota}}               % ι
\DeclareUnicodeCharacter{954}{\ensuremath{\kappa}}              % κ
\DeclareUnicodeCharacter{955}{\ensuremath{\lambda}}             % λ
\DeclareUnicodeCharacter{957}{\ensuremath{\nu}}                 % ν
\DeclareUnicodeCharacter{959}{\ensuremath{o}}                   % ο
\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}              % σ
\DeclareUnicodeCharacter{964}{\ensuremath{\tau}}                % τ
\DeclareUnicodeCharacter{969}{\ensuremath{\omega}}              % ω
\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}              % Γ
\DeclareUnicodeCharacter{916}{\ensuremath{\Delta}}              % Δ
\DeclareUnicodeCharacter{183}{\ensuremath{\cdot}}               % ·
\DeclareUnicodeCharacter{8605}{\ensuremath{\leadsto}}           % ↝
\DeclareUnicodeCharacter{8614}{\ensuremath{\mapsto}}            % ↦
\DeclareUnicodeCharacter{8636}{\ensuremath{\leftharpoonup}}     % ↼
\DeclareUnicodeCharacter{8658}{\ensuremath{\Rightarrow}}        % ⇒
\DeclareUnicodeCharacter{10230}{\ensuremath{\longrightarrow}}   % ⟶
\DeclareUnicodeCharacter{9733}{\ensuremath{\star}}              % ★
\DeclareUnicodeCharacter{9659}{\ensuremath{\vartriangleright}}  % ▻
%\DeclareUnicodeCharacter{9669}{\ensuremath{\vartriangleleft}}  % ◅

\newcommand\defeq{\stackrel{\text{def}}{=}}
\DeclareUnicodeCharacter{8797}{\ensuremath{\defeq}}             % ≝
\newcommand\textLambda{\ensuremath{\Lambda}}

\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}
\vfill

\begin{center}
{\Huge \bfseries What do we need to program with names and binders?}
\end{center}

\vfill
\end{frame}

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

\vfill

\visible<+->{A type for names}

\begin{block}{}
\texttt{Name\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set}
\end{block}

\visible<+->{An equality test for names}

\begin{block}{}
\texttt{\makebox[1.22ex][c]{{\char `\_}}≟Name\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool}
\end{block}

\visible<+->{A generator of fresh names}

\begin{block}{}
\texttt{fresh\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name}
\end{block}

\visible<+->{Alternatively$:$ An initial fresh name}

\begin{block}{}
\texttt{init\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name}
\end{block}

\visible<+->{And$:$ How to pick a new one}

\begin{block}{}
\texttt{next\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name}
\end{block}

\vfill
\end{frame}

\begin{frame}<1,2>[label=dataTm]
\frametitle{Data type for the untyped lambda calculus}

\vfill

\begin{block}{}
\only<1>{\texttt{data\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{1em}}V\mbox{\hspace{2em}}Name{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{1em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}Tm\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{1em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2em}}Name\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{1em}}Let\mbox{\hspace{1em}}Name\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}Tm{\newline}}}\only<2>{\texttt{data\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{0.50em}}V\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}Let\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}}}\only<3>{\texttt{data\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{0.50em}}V\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name{\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}\mbox{\hspace{0.50em}}Let\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name{\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm{\newline}}}\only<4>{\texttt{data\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{4em}}V\mbox{\hspace{2em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{4em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\(}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{1em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta ${\char `\.}\mbox{\hspace{1em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}} \mbox{\hspace{1em}}{\char `\(}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{1em}}{\char `\(}Tm\mbox{\hspace{0.50em}}$ \beta ${\char `\)}{\newline}\mbox{\hspace{0.50em}}{\char `\|}\mbox{\hspace{1em}}$ \exists $\mbox{\hspace{0.50em}}$ \beta ${\char `\.}\mbox{\hspace{1em}}Let\mbox{\hspace{1em}}{\char `\(}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{1em}}{\char `\(}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}Tm\mbox{\hspace{0.50em}}$ \beta ${\char `\)}{\newline}}}\only<5>{\texttt{data\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{0.50em}}V\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}Let\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}}}\only<6>{\texttt{data\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{0.50em}}V\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}u\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \beta $\}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{0.50em}}Let\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \beta $\}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}u\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\newline}}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries \only<1>{Nothing more!}\only<2->{Something less?}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \texttt{{\char `\(}$ \lambda $\mbox{\hspace{0.50em}}x{\char `\.}\mbox{\hspace{0.50em}}e{\char `\)}\mbox{\hspace{0.50em}}x}}
\end{center}

\begin{center}
{\Huge \bfseries can we compare the two '\texttt{x}'s?}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Comparison is World Homogeneous}
\end{center}

\begin{center}
{\Large \texttt{\makebox[1.22ex][c]{{\char `\_}}≟Name\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Names inhabit worlds}
\end{center}

\begin{itemize}
\item

{\LARGE \texttt{World\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Set}}

\item

{\LARGE \texttt{Name\mbox{\hspace{1.50em}}{\char `\:}\mbox{\hspace{0.50em}}World\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Set}}

\item

{\LARGE \texttt{$ \emptyset $\mbox{\hspace{3em}}{\char `\:}\mbox{\hspace{0.50em}}World}}
\end{itemize}

\begin{block}{Example$:$}
{\LARGE \texttt{$ \alpha $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}World{\newline}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha ${\newline}}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\huge \texttt{$ \neg $name$ \emptyset $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \emptyset $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \bot $}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge $ \left(\text{\texttt{$ \lambda $\mbox{\hspace{0.50em}}}}\text{\texttt{x}}\text{\alert{$ _{\beta} $}}\text{\texttt{{\char `\.}\mbox{\hspace{0.50em}}}}{e}\text{\alert{$ _{\beta} $}}\right)\;\text{\texttt{x}}\text{\alert{$ _{\alpha} $}} $}
\end{center}

\begin{center}
\visible<2,3>{{\Huge $ \left(\text{\texttt{$ \lambda $\mbox{\hspace{0.50em}}}}\text{\texttt{x}}\text{\alert{$ _{\beta} $}}\text{\texttt{{\char `\.}\mbox{\hspace{0.50em}}}}\text{\texttt{y}}\text{\alert{$ _{\beta} $}}\right)\;\text{\texttt{y}}\text{\alert{$ _{\alpha} $}} $}}
\end{center}

\begin{center}
{\Huge \bfseries \visible<3>{We need links between worlds!}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{A type for binders}

\vfill

\begin{center}
{\Huge \ttfamily \texttt{Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set}}
\end{center}

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

α outer world / β inner world

\item

A more precise type for a Name β

\item

\texttt{nameOfBinder\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \beta $}

\item

Using $ \text{\texttt{Binder}} $, name shadowing is permitted
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

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

\vfill
\end{frame}

\againframe<2,5>{dataTm}

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

\vfill

\begin{block}{}
\invisible<1>{\texttt{size\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}ℕ{\newline}}}\texttt{size\mbox{\hspace{0.50em}}{\char `\(}V\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}{\char `\)}\mbox{\hspace{4em}}{\char `\=}\mbox{\hspace{0.50em}}1{\newline}size\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{$ \cdotp $}\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}1\mbox{\hspace{0.50em}}{\char `\+}\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}size\mbox{\hspace{0.50em}}{\char `\(}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{0.50em}}t{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}1\mbox{\hspace{0.50em}}{\char `\+}\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t{\newline}size\mbox{\hspace{0.50em}}{\char `\(}Let\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}1\mbox{\hspace{0.50em}}{\char `\+}\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}\mbox{\hspace{0.50em}}size\mbox{\hspace{0.50em}}u{\newline}}
\end{block}

{\pause}

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

Polymorphic recursion at work!

\item

No freshning!

\item

No shifting!
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{block}{}
\texttt{exportBinder\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{1em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}y\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \beta ${\char `\)}{\newline}\mbox{\hspace{8em}}$ \rightarrow $\mbox{\hspace{0.50em}}Maybe\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}}
\end{block}

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

Compares $ \text{y} $ and $ \text{\texttt{nameOfBinder}}\;\text{x} $

\item

Performs a type refinement on success

\item

Partial!

\item

Injective!
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries What about moving names the other way around? \visible<2>{\alert{No!}}}
\end{center}

\vfill
\end{frame}

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

\vfill

\begin{block}{}
\visible<2,3,4,5>{\alt<2,3>{\texttt{rm\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}Name{\newline}rm\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\[}{\char `\]}\mbox{\hspace{9.50em}}{\char `\=}\mbox{\hspace{0.50em}}{\char `\[}{\char `\]}{\newline}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{1em}}{\char `\(}y\mbox{\hspace{0.50em}}∷\mbox{\hspace{0.50em}}ys{\char `\)}\mbox{\hspace{1em}}with\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}≟Name\mbox{\hspace{0.50em}}y{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{6.50em}}{\char `\|}\mbox{\hspace{0.50em}}false\mbox{\hspace{2em}}{\char `\=}\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}∷\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}ys{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{6.50em}}{\char `\|}\mbox{\hspace{0.50em}}true\mbox{\hspace{2.50em}}{\char `\=}\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}ys{\newline}}}{\texttt{rm\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}rm\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\[}{\char `\]}\mbox{\hspace{9.50em}}{\char `\=}\mbox{\hspace{0.50em}}{\char `\[}{\char `\]}{\newline}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{1em}}{\char `\(}y\mbox{\hspace{0.50em}}∷\mbox{\hspace{0.50em}}ys{\char `\)}\mbox{\hspace{1em}}with\mbox{\hspace{0.50em}}exportBinder\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{6.50em}}{\char `\|}\mbox{\hspace{0.50em}}just\mbox{\hspace{0.50em}}y\mbox{\hspace{1.50em}}{\char `\=}\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}∷\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}ys{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{6.50em}}{\char `\|}\mbox{\hspace{0.50em}}nothing\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}ys{\newline}}}}
\end{block}

\begin{block}{}
\visible<1,2,3,4,5>{\alt<1,2>{\texttt{fv\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}Name{\newline}}}{\texttt{fv\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}}}\texttt{fv\mbox{\hspace{0.50em}}{\char `\(}V\mbox{\hspace{0.50em}}x{\char `\)}\mbox{\hspace{4em}}{\char `\=}\mbox{\hspace{0.50em}}{\char `\[}\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}{\char `\]}{\newline}fv\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{$ \cdotp $}\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}{\char `\+}\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}u{\newline}fv\mbox{\hspace{0.50em}}{\char `\(}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}{\char `\(}fv\mbox{\hspace{0.50em}}t{\char `\)}{\newline}fv\mbox{\hspace{0.50em}}{\char `\(}Let\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}fv\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}{\char `\+}\mbox{\hspace{0.50em}}rm\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}{\char `\(}fv\mbox{\hspace{0.50em}}u{\char `\)}{\newline}}}
\end{block}

\begin{center}
\alert{{\Huge \bfseries \visible<5>{\texttt{fv} enjoys a free theorem!}}}
\end{center}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{Importing names}

\vfill

\begin{block}{}
\texttt{\makebox[1.22ex][c]{{\char `\_}}$ \subseteq $\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{4.50em}}{\char `\:}\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}World{\newline}$ \subseteq ${\char `\-}refl\mbox{\hspace{3em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \alpha ${\newline}$ \subseteq ${\char `\-}trans\mbox{\hspace{2.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \gamma $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \gamma ${\newline}import$ \subseteq $\mbox{\hspace{2.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \beta ${\newline}$ \emptyset ${\char `\-}bottom{\char `\-}$ \subseteq $\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \emptyset $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \alpha ${\newline}}
\end{block}

\begin{visibleenv}<2,3>
\begin{center}

\begin{tikzpicture}
    \matrix (m) [matrix of math nodes, row sep=2em, column sep=2em, text height=1.5ex, text depth=0.25ex, ampersand replacement=\&]
    { α \& \& γ \\
        \& \&   \\
      β \& \& δ \\ };
    \path[-]
    (m-1-3) edge node[above] {\texttt{Binder}} (m-1-1);
    \path[-]
    (m-1-1) edge node[left] {\begin{turn}{ -90}$⊆$\end{turn}} (m-3-1);
    \path[-][dashed]
    (m-1-3) edge node[right] {\begin{turn}{ -90}$⊆$\end{turn}} (m-3-3);
    \path[-][dashed]
    (m-3-3) edge node[below=3pt] {\texttt{Binder}} (m-3-1);
\end{tikzpicture}

\end{center}
\end{visibleenv}

{\pause}

\begin{block}{}
\texttt{\makebox[1.22ex][c]{{\char `\_}}Binder{\char `\-}commute{\char `\-}$ \subseteq $\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{1em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{11em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \lambda $\mbox{\hspace{0.50em}}$ \delta $\mbox{\hspace{2em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \gamma $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \delta $\mbox{\hspace{0.50em}}$ \times $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \delta $}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Strong binders}

\vfill

\begin{block}{}
\texttt{BINDER\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}World{\newline}weaken\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}BINDER\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}dropName\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}BINDER\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \subseteq $\mbox{\hspace{0.50em}}$ \beta ${\newline}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Generating names}

\vfill

\begin{block}{}
\texttt{Fresh\mbox{\hspace{3.50em}}{\char `\:}\mbox{\hspace{0.50em}}World\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Set{\newline}Fresh\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{2.50em}}{\char `\=}\mbox{\hspace{0.50em}}$ \exists $\mbox{\hspace{0.50em}}$ \lambda $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}BINDER\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}fresh$ \emptyset $\mbox{\hspace{3em}}{\char `\:}\mbox{\hspace{0.50em}}Fresh\mbox{\hspace{0.50em}}$ \emptyset ${\newline}nextBINDER\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}BINDER\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\newline}\mbox{\hspace{12.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Fresh\mbox{\hspace{0.50em}}$ \beta ${\newline}}
\end{block}

\vfill
\end{frame}

\begin{frame}
\frametitle{Safety Properties}

\vfill

Well-typed programs...

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

... do not get stuck

\item

... preserve α-equivalence

\item

... do not break name abstraction

\item

... do not mix names with different scopes
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries How it works?}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{Nominal implementation}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ \text{\texttt{World}} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ \text{\texttt{Pred}}\;\text{ℕ} $}}\\
\text{\visible<2->{$ \text{\texttt{Name}}\;\beta $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ \text{\{ a $:$ ℕ \textbar{} }\text{a}\;\text{$ \in $}\;\beta\text{ \}} $}}\\
\text{\visible<3->{$ \text{\texttt{Binder}}\;\alpha\;\beta $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ \text{\{ a $:$ ℕ \textbar{} $ \beta $ $ \equiv $ \{a\} $ \cup $ $ \alpha $ \}} $}}\\
\text{\visible<4->{$ \text{\texttt{BINDER}}\;\alpha\;\beta $}} & \text{\visible<4->{$ \text{≝} $}} & \text{\visible<4->{$ \text{\{ a $:$ ℕ \textbar{} $ \beta $ $ \equiv $ \{a\} $ \cup $ $ \alpha $ $ \wedge $ a \textgreater{} $ \alpha $ \}} $}}\\
\text{\visible<5->{$ \alpha\;\text{$ \subseteq $}\;\beta $}} & \text{\visible<5->{$ \text{≝} $}} & \text{\visible<5->{$ \text{$ \forall $ a, }\text{a}\;\text{$ \in $}\;\alpha\;\text{$ \Rightarrow $}\;\text{a}\;\text{$ \in $}\;\beta $}}\\
\text{\visible<6->{$ \text{\_}\text{≟}_{\text{\texttt{Name}}}\text{\_} $}} & \text{\visible<6->{$ \text{≝} $}} & \text{\visible<6->{$ \text{\_}\text{≟}_{\text{ℕ}}\text{\_} $}}\\
\text{\visible<7->{$ \text{\texttt{exportBinder}}\;\text{a}\;\text{b} $}} & \text{\visible<7->{$ \text{≝} $}} & \text{\visible<7->{$ \text{if }\text{a}\;\text{≟}_{\text{ℕ}}\;\text{b}\text{ then }\text{\texttt{nothing}}\text{ else }\text{\texttt{just}}\;\text{b} $}}\\
\text{\visible<8->{$ \text{\texttt{nextBINDER}}\;\text{a}\;\text{b} $}} & \text{\visible<8->{$ \text{≝} $}} & \text{\visible<8->{$ \text{b}\;\text{⊔}\;(\text{a} + 1) $}}
\end{array} \]

\begin{visibleenv}<9>
$ \text{\texttt{import$ \subseteq $}} $, $ \text{\texttt{nameOfBinder}} $, $ \text{\texttt{weaken}} $,
       $ \text{\texttt{dropName}} $, $ \text{\texttt{Binder{\char `\-}commute{\char `\-}$ \subseteq $}} $, $ \text{\texttt{$ \subseteq ${\char `\-}trans}} $,
       $ \text{\texttt{$ \subseteq ${\char `\-}refl}} $ are computation free.
\end{visibleenv}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Why is this safe?}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{Logical relations recap}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ {f}\;\text{(}\tau\;\text{$ \rightarrow $}\;\sigma\text{)}\;{g} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ \text{$ \forall $}\;{v}\;{w}\text{, }{v}\;\text{(}\tau\text{)}\;{w}\;\text{$ \Rightarrow $}\;{f}\;{v}\;\text{(}\sigma\text{)}\;{g}\;{w} $}}\\
\text{\visible<2->{$ \text{(}{x}\text{₁}\text{, }{y}\text{₁}\text{)}\;\text{(}\tau\;\text{$ \times $}\;\sigma\text{)}\;\text{(}{x}\text{₂}\text{, }{y}\text{₂}\text{)} $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ {x}\text{₁}\;\text{(}\tau\text{)}\;{x}\text{₂}\;\text{$ \wedge $}\;{y}\text{₁}\;\text{(}\sigma\text{)}\;{y}\text{₂} $}}\\
\text{\visible<3->{$ {i}\text{₁}\;\text{(}\text{ℕ}\text{)}\;{i}\text{₂} $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ {i}\text{₁}\;\text{$ \equiv $}\;{i}\text{₂} $}}
\end{array} \]

\vfill
\end{frame}

\begin{frame}
\frametitle{Worlds as atom bijections}

\vfill

\begin{description}[<+->]
\item[Shadowing extension]

a₁ ((b₁,b₂) ⊞ $ \alpha $) a₂ holds if and only if either

\begin{itemize}
\item

a₁ $ \equiv $ b₁ $ \wedge $ a₂ $ \equiv $ b₂ or,

\item

a₁ ≢ b₁ $ \wedge $ a₂ ≢ b₂ $ \wedge $ a₁ ($ \alpha $) a₂
\end{itemize}

\item[Fresh extension]

(b₁,b₂)$ \alpha $ is

\begin{itemize}
\item

defined only if $ \text{b₁}\;\text{\textgreater{}}\;\text{\texttt{dom}}\left(\alpha\right) $ and $ \text{b₂}\;\text{\textgreater{}}\;\text{\texttt{codom}}\left(\alpha\right) $

\item

equal to \{(b₁,b₂)\} $ \cup $ $ \alpha $ when defined
\end{itemize}
\end{description}

\vfill
\end{frame}

\begin{frame}
\frametitle{Nominal logical relations}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ \text{a}\text{₁}\;\text{(}\text{\texttt{Name}}\;\beta\text{)}\;\text{a}\text{₂} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ \text{a}\text{₁}\;\text{(}\beta\text{)}\;\text{a}\text{₂} $}}\\
\text{\visible<2->{$ \text{a}\text{₁}\;\text{(}\text{\texttt{Binder}}\;\alpha\;\beta\text{)}\;\text{a}\text{₂} $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ \beta\;\text{$ \equiv $}\;\text{(}\text{a}\text{₁}\text{,}\text{a}\text{₂}\text{) ⊞ }\alpha $}}\\
\text{\visible<3->{$ \text{a}\text{₁}\;\text{(}\text{\texttt{BINDER}}\;\alpha\;\beta\text{)}\;\text{a}\text{₂} $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ \beta\;\text{$ \equiv $}\;\text{(a₁,a₂) $ \alpha $} $}}\\
\text{\visible<4->{$ \text{\texttt{{\char `\(}{\char `\)}}}\;\text{(}\alpha\;\text{$ \subseteq $}\;\beta\text{)}\;\text{\texttt{{\char `\(}{\char `\)}}} $}} & \text{\visible<4->{$ \text{≝} $}} & \text{\visible<4->{$ \alpha\;\text{$ \subseteq $}\;\beta $}}
\end{array} \]

\vfill
\end{frame}

\begin{frame}
\frametitle{Soundness theorem for nominal logical relations}

\vfill

\begin{theorem}
Every primitive operation $ {p} $ of type
                 τ is related to itself at type τ
\end{theorem}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries Come on, De Bruijn indices are much simpler}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{De Bruijn implementation (types)}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ \text{\texttt{World}} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ \text{ℕ} $}}\\
\text{\visible<2->{$ \text{\texttt{Name}}\;\beta $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ \text{\texttt{Fin}}\;\beta\text{ $ \Leftrightarrow $ }\left[0\text{,}\beta\right) $}}\\
\text{\visible<3->{$ \text{\texttt{Binder}}\;\alpha\;\beta $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ \beta\;\text{$ \equiv $}\;(\alpha + 1) $}}\\
\text{\visible<4->{$ \text{\texttt{BINDER}} $}} & \text{\visible<4->{$ \text{≝} $}} & \text{\visible<4->{$ \text{\texttt{Binder}} $}}\\
\text{\visible<5->{$ \alpha\;\text{$ \subseteq $}\;\beta $}} & \text{\visible<5->{$ \text{≝} $}} & \text{\visible<5->{$ \text{\{ k $:$ ℕ \textbar{} $ \beta $ $ \equiv $ $ \alpha $ + k \}} $}}
\end{array} \]

\vfill
\end{frame}

\begin{frame}
\frametitle{De Bruijn implementation (primitives)}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ \text{\_}\text{≟}_{\text{\texttt{Name}}}\text{\_} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ \text{\_}\text{≟}_{\text{ℕ}}\text{\_} $}}\\
\text{\visible<2->{$ \text{exportBinder}\;\text{\texttt{{\char `\(}{\char `\)}}}\;0 $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ \text{\texttt{nothing}} $}}\\
\text{\visible<3->{$ \text{exportBinder}\;\text{\texttt{{\char `\(}{\char `\)}}}\;\left(\text{\texttt{suc}}\;{i}\right) $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ \text{\texttt{just}}\;{i} $}}\\
\text{\visible<4->{$ \text{\texttt{import$ \subseteq $}}\;{k}\;{i} $}} & \text{\visible<4->{$ \text{≝} $}} & \text{\visible<4->{$ ({k} + {i}) $}}\\
\text{\visible<5->{$ \text{\texttt{$ \subseteq ${\char `\-}trans}}\;{k}\;{k}\text{'} $}} & \text{\visible<5->{$ \text{≝} $}} & \text{\visible<5->{$ ({k} + {k}\text{'}) $}}\\
\text{\visible<6->{$ \text{\texttt{nameOfBinder}}\;\text{\texttt{{\char `\(}{\char `\)}}} $}} & \text{\visible<6->{$ \text{≝} $}} & \text{\visible<6->{$ 0 $}}\\
\text{\visible<7->{$ \text{\texttt{dropName}}\;\text{\texttt{{\char `\(}{\char `\)}}} $}} & \text{\visible<7->{$ \text{≝} $}} & \text{\visible<7->{$ 1 $}}\\
\text{\visible<8->{$ \text{\texttt{$ \subseteq ${\char `\-}refl}} $}} & \text{\visible<8->{$ \text{≝} $}} & \text{\visible<8->{$ 0 $}}
\end{array} \]

\begin{visibleenv}<9>
$ \text{\texttt{nextBINDER}} $, $ \text{\texttt{weaken}} $,
       and $ \text{\texttt{Binder{\char `\-}commute{\char `\-}$ \subseteq $}} $ are computation free.
\end{visibleenv}

\vfill
\end{frame}

\begin{frame}[<+->]
\frametitle{(well-scoped) De Bruijn indices advantages}

\vfill

{\Large \bfseries Canonical representation}

{\pause}

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

α-equivalence made simple!

\item

Structural induction!
\end{itemize}

\visible<4,5,6>{{\Large \bfseries Guaranteed well-formness}}

{\pause}

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

The $ \text{\texttt{Fin}}\;{n} $ technique is well known for that

\item

Every variable has to be smaller than $ {n} $
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

\begin{center}
{\Huge \bfseries It is trivially safe, right? \visible<2>{\alert{No!}}}
\end{center}

\vfill
\end{frame}

\begin{frame}
\frametitle{De Bruijn indices canonicity$:$ precisely}

\vfill

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

Bound and fresh names uniquely chosen.

\item

Free names are freely chosen, though!

\item

Consequence$:$ α-equivalence is not so simple!

\item

α-equivalences are not automatically preserved!
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\frametitle{Worlds as bijections again}

\vfill

\begin{description}[<+->]
\item[Shifting]

$ \alpha\uparrow\text{ ≝ \{(0,0)\} $ \cup $ \{(i₁+1,i₂+1) \textbar{} (i₁,i₂) $ \in $ $ \alpha $\}} $

\item[Iterated shifting]

We write $ \alpha\uparrow^{{k}} $ for the result of
                   shifting the world α $ {k} $ times
\end{description}

\vfill
\end{frame}

\begin{frame}
\frametitle{De Bruijn logical relations}

\vfill

\[ \begin{array}{rcl}
\text{\visible<1->{$ {i}\text{₁}\;\text{(}\text{\texttt{Name}}\;\beta\text{)}\;{i}\text{₂} $}} & \text{\visible<1->{$ \text{≝} $}} & \text{\visible<1->{$ {i}\text{₁}\;\text{(}\beta\text{)}\;{i}\text{₂} $}}\\
\text{\visible<2->{$ \text{\texttt{{\char `\(}{\char `\)}}}\;\text{(}\text{\texttt{Binder}}\;\alpha\;\beta\text{)}\;\text{\texttt{{\char `\(}{\char `\)}}} $}} & \text{\visible<2->{$ \text{≝} $}} & \text{\visible<2->{$ \beta\;\text{$ \equiv $}\;\alpha\uparrow $}}\\
\text{\visible<3->{$ \text{\texttt{{\char `\(}{\char `\)}}}\;\text{(}\text{\texttt{BINDER}}\;\alpha\;\beta\text{)}\;\text{\texttt{{\char `\(}{\char `\)}}} $}} & \text{\visible<3->{$ \text{≝} $}} & \text{\visible<3->{$ \beta\;\text{$ \equiv $}\;\alpha\uparrow $}}\\
\text{\visible<4->{$ {k}\;\text{(}\alpha\;\text{$ \subseteq $}\;\beta\text{)}\;{k} $}} & \text{\visible<4->{$ \text{≝} $}} & \text{\visible<4->{$ \beta\;\text{$ \equiv $}\;\alpha\uparrow^{{k}} $}}
\end{array} \]

\vfill
\end{frame}

\begin{frame}
\frametitle{Soundness theorem for De Bruijn logical relations}

\vfill

\begin{theorem}
Every primitive operation $ {p} $ of type
                 τ is related to itself at type τ
\end{theorem}

\vfill
\end{frame}

\begin{frame}
\frametitle{Listings of some advanced examples}

\vfill

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

Deciding α-equivalence on types like $ \text{\texttt{Tm}} $

\item

Generic export through a binder

\item

Generic import through a world inclusion witness

\item

Normalisation by evaluation
\end{itemize}

\vfill
\end{frame}

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

\vfill

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

More powerful logical relations (relating to an abstract model)

\item

How to carry information on binders (types, specs...)

\item

More formalisation of the logical relations

\item

More advanced usages
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\frametitle{Conclusion}

\vfill

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

Explicit scopes using world indices

\item

Non-freshening opening

\item

Name abstraction as existential quantification

\item

Expressiveness close to a manual model with names

\item

Two concrete and safe implementations of the interface
\end{itemize}

\vfill
\end{frame}

\begin{frame}
\vfill

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

\vfill
\end{frame}

\appendix

\begin{frame}[label=bonus]
\frametitle{Bonus track}

\hyperlink{occurs}{\beamerbutton{\texttt{occurs}}}

\hyperlink{star}{\beamerbutton{\texttt{Star}}}

\hyperlink{env}{\beamerbutton{\texttt{★Binder}}}

\hyperlink{exportStar}{\beamerbutton{\texttt{export★Binder}}}

\hyperlink{fv'}{\beamerbutton{\texttt{fv{\char `\'}}}}

\hyperlink{pack}{\beamerbutton{Packaging}}

\hyperlink{app}{\beamerbutton{\texttt{app}}}

\hyperlink{context}{\beamerbutton{Contexts}}

\hyperlink{patt}{\beamerbutton{Patterns}}

\hyperlink{nameEqH}{\beamerbutton{\texttt{nameEqH}}}
\end{frame}

\againframe<1,2,3,4,5,6>{dataTm}

\begin{frame}[label=occurs]
\frametitle{Occurs check}

\begin{block}{}
\texttt{occurs\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool{\newline}occurs\mbox{\hspace{0.50em}}x₀\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}{\char `\(}$ \lambda $\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}x₀\mbox{\hspace{0.50em}}≟Name\mbox{\hspace{0.50em}}y{\char `\)}{\newline}\mbox{\hspace{1em}}where{\newline}\mbox{\hspace{2em}}OccEnv\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}World\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Set{\newline}\mbox{\hspace{2em}}OccEnv\mbox{\hspace{1em}}$ \alpha $\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool{\newline}\mbox{\hspace{2em}}extend\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}OccEnv\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}OccEnv\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{2em}}extend\mbox{\hspace{1em}}x\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}maybe\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}false\mbox{\hspace{0.50em}}{\char `\(}exportBinder\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y{\char `\)}{\newline}{\newline}\mbox{\hspace{2em}}occ\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}OccEnv\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool{\newline}\mbox{\hspace{2em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}V\mbox{\hspace{0.50em}}y{\char `\)}\mbox{\hspace{4em}}{\char `\=}\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}y{\newline}\mbox{\hspace{2em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}t\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{$ \cdotp $}\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$ \vee $\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}u{\newline}\mbox{\hspace{2em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}{\char `\(}extend\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}$ \Gamma ${\char `\)}\mbox{\hspace{0.50em}}t{\newline}\mbox{\hspace{2em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}Let\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}$ \vee $\mbox{\hspace{0.50em}}occ\mbox{\hspace{0.50em}}{\char `\(}extend\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}$ \Gamma ${\char `\)}\mbox{\hspace{0.50em}}u{\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=star]
\frametitle{Reflexive and transitive closure of a relation}

\begin{block}{}
\texttt{Rel\mbox{\hspace{0.50em}}A\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}A\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}A\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Set}
\end{block}

\begin{block}{}
\texttt{data\mbox{\hspace{0.50em}}Star\mbox{\hspace{0.50em}}\{I\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\}\mbox{\hspace{0.50em}}{\char `\(}T\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}I{\char `\)}\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}I\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{1em}}$ \epsilon $\mbox{\hspace{2em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{i\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Star\mbox{\hspace{0.50em}}T\mbox{\hspace{0.50em}}i\mbox{\hspace{0.50em}}i{\newline}\mbox{\hspace{1em}}\makebox[1.22ex][c]{{\char `\_}}◅\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{i\mbox{\hspace{0.50em}}j\mbox{\hspace{0.50em}}k\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}T\mbox{\hspace{0.50em}}i\mbox{\hspace{0.50em}}j\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Star\mbox{\hspace{0.50em}}T\mbox{\hspace{0.50em}}j\mbox{\hspace{0.50em}}k\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Star\mbox{\hspace{0.50em}}T\mbox{\hspace{0.50em}}i\mbox{\hspace{0.50em}}k{\newline}}
\end{block}

\begin{block}{}
\texttt{Star⁻¹\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{I\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}I\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}I{\newline}Star⁻¹\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}flip\mbox{\hspace{0.50em}}$ \circ $\mbox{\hspace{0.50em}}Star\mbox{\hspace{0.50em}}$ \circ $\mbox{\hspace{0.50em}}flip{\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=env]
\frametitle{Environments as a chain of binders}

\begin{block}{}
\texttt{★Binder\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Rel\mbox{\hspace{0.50em}}World{\newline}★Binder\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}Star⁻¹\mbox{\hspace{0.50em}}Binder{\newline}}
\end{block}

\begin{block}{}
\texttt{\mbox{\hspace{1em}}$ \epsilon $\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}★Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \alpha ${\newline}\makebox[1.22ex][c]{{\char `\_}}◅\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}$ \Gamma $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}★Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}{\newline}\mbox{\hspace{7.50em}}$ \rightarrow $\mbox{\hspace{1em}}★Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=exportStar]
\frametitle{Exporting through a chain of binders}

\begin{block}{}
\texttt{export★Binder\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}\mbox{\hspace{1em}}$ \rightarrow $\mbox{\hspace{0.50em}}★Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{13em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Maybe\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}export★Binder\mbox{\hspace{1em}}$ \epsilon $\mbox{\hspace{4em}}y{\newline}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}just\mbox{\hspace{0.50em}}y{\newline}export★Binder\mbox{\hspace{1em}}{\char `\(}x\mbox{\hspace{0.50em}}◅\mbox{\hspace{0.50em}}$ \Gamma ${\char `\)}\mbox{\hspace{1em}}y{\newline}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}exportBinder\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}{\char `\>}{\char `\>}{\char `\=}\mbox{\hspace{0.50em}}export★Binder\mbox{\hspace{0.50em}}$ \Gamma ${\newline}\mbox{\hspace{1em}}where\mbox{\hspace{0.50em}}open\mbox{\hspace{0.50em}}MaybeMonad{\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=fv']
\frametitle{Free variables, continued...}

\begin{block}{}
\texttt{fv{\char `\'}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\mbox{\hspace{0.50em}}$ \alpha $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}★Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}List\mbox{\hspace{0.50em}}{\char `\(}Name\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}fv{\char `\'}\mbox{\hspace{1em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}V\mbox{\hspace{0.50em}}x{\char `\)}\mbox{\hspace{4em}}{\char `\=}\mbox{\hspace{0.50em}}List{\char `\.}fromMaybe\mbox{\hspace{0.50em}}{\char `\(}export★Binder\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}x{\char `\)}{\newline}fv{\char `\'}\mbox{\hspace{1em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}t\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{$ \cdotp $}\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}fv{\char `\'}\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}{\char `\+}\mbox{\hspace{0.50em}}fv{\char `\'}\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}u{\newline}fv{\char `\'}\mbox{\hspace{1em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t{\char `\)}\mbox{\hspace{3em}}{\char `\=}\mbox{\hspace{0.50em}}fv{\char `\'}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}◅\mbox{\hspace{0.50em}}$ \Gamma ${\char `\)}\mbox{\hspace{0.50em}}t{\newline}fv{\char `\'}\mbox{\hspace{1em}}$ \Gamma $\mbox{\hspace{1em}}{\char `\(}Let\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}u{\char `\)}\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}fv{\char `\'}\mbox{\hspace{0.50em}}$ \Gamma $\mbox{\hspace{0.50em}}t\mbox{\hspace{0.50em}}{\char `\+}{\char `\+}\mbox{\hspace{0.50em}}fv{\char `\'}\mbox{\hspace{0.50em}}{\char `\(}x\mbox{\hspace{0.50em}}◅\mbox{\hspace{0.50em}}$ \Gamma ${\char `\)}\mbox{\hspace{0.50em}}u{\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=pack]
\frametitle{Packaging up...}

\begin{itemize}
\item

\texttt{binderOf}

\item

\texttt{nameOf}

\item

\texttt{nextOf}

\item

\texttt{importWith}
\end{itemize}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=app]
\frametitle{Constructing terms}

\begin{block}{}
\texttt{app\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \emptyset ${\newline}app\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{1em}}{\char `\(}binderOf\mbox{\hspace{0.50em}}x{\char `\)}\mbox{\hspace{0.50em}}{\char `\(}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{0.50em}}{\char `\(}binderOf\mbox{\hspace{0.50em}}y{\char `\)}{\newline}\mbox{\hspace{5em}}{\char `\(}V\mbox{\hspace{0.50em}}{\char `\(}importWith\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}{\char `\(}nameOf\mbox{\hspace{0.50em}}x{\char `\)}{\char `\)}\mbox{\hspace{0.50em}}\makebox[1.22ex][c]{$ \cdotp $}\mbox{\hspace{0.50em}}V\mbox{\hspace{0.50em}}{\char `\(}nameOf\mbox{\hspace{0.50em}}y{\char `\)}{\char `\)}{\char `\)}{\newline}\mbox{\hspace{1em}}where\mbox{\hspace{1em}}open\mbox{\hspace{0.50em}}FreshPack{\newline}\mbox{\hspace{4.50em}}x\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}fresh$ \emptyset ${\newline}\mbox{\hspace{4.50em}}y\mbox{\hspace{1em}}{\char `\=}\mbox{\hspace{0.50em}}nextOf\mbox{\hspace{0.50em}}x{\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=context]
\frametitle{Towards elaborate uses of worlds}

\begin{block}{}
\texttt{data\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}{\char `\(}$ \beta $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}World{\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{1em}}Hole\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \alpha ${\newline}\mbox{\hspace{1em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}₁\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\}\mbox{\hspace{0.50em}}{\char `\(}c\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{1em}}\makebox[1.22ex][c]{{\char `\_}}\makebox[1.22ex][c]{$ \cdotp $}₂\makebox[1.22ex][c]{{\char `\_}}\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}c\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{1em}}\makebox[1.22ex][c]{ƛ}\mbox{\hspace{2.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}$ \tau $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Ty{\char `\)}{\newline}\mbox{\hspace{9.50em}}{\char `\(}c\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\newline}\mbox{\hspace{1em}}Let₁\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}c\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\char `\)}{\newline}\mbox{\hspace{9.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\newline}\mbox{\hspace{1em}}Let₂\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\mbox{\hspace{0.50em}}\{$ \beta $\mbox{\hspace{0.50em}}$ \gamma $\}\mbox{\hspace{1em}}{\char `\(}x\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\char `\)}\mbox{\hspace{0.50em}}{\char `\(}t\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Tm\mbox{\hspace{0.50em}}$ \alpha ${\char `\)}{\newline}\mbox{\hspace{9.50em}}{\char `\(}c\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \gamma ${\char `\)}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}C\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma ${\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=patt]
\frametitle{Patterns types}

\begin{block}{}
\texttt{data\mbox{\hspace{0.50em}}Pa\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}Set\mbox{\hspace{0.50em}}where{\newline}\mbox{\hspace{1em}}PVar\mbox{\hspace{1.50em}}{\char `\:}\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Pa\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}\mbox{\hspace{1em}}PPair\mbox{\hspace{1em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \gamma $\}\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Pa\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \gamma $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Pa\mbox{\hspace{0.50em}}$ \gamma $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Pa\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta ${\newline}}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}

\begin{frame}[label=nameEqH]
\frametitle{Safe heterogeneous comparison!}

\begin{block}{}
\texttt{nameEqH\mbox{\hspace{0.50em}}{\char `\:}\mbox{\hspace{0.50em}}$ \forall $\{$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Name\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Binder\mbox{\hspace{0.50em}}$ \alpha $\mbox{\hspace{0.50em}}$ \beta $\mbox{\hspace{0.50em}}$ \rightarrow $\mbox{\hspace{0.50em}}Bool}
\end{block}

\begin{block}{}
\texttt{nameEqH\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}y\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}with\mbox{\hspace{0.50em}}exportBinder\mbox{\hspace{0.50em}}lnk\mbox{\hspace{0.50em}}y{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{8em}}{\char `\|}\mbox{\hspace{0.50em}}just\mbox{\hspace{0.50em}}y{\char `\'}\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}x\mbox{\hspace{0.50em}}$ \equiv $\mbox{\hspace{0.50em}}y{\char `\'}{\newline}{\char `\.}{\char `\.}{\char `\.}\mbox{\hspace{8em}}{\char `\|}\mbox{\hspace{0.50em}}nothing\mbox{\hspace{0.50em}}{\char `\=}\mbox{\hspace{0.50em}}false}
\end{block}

\hyperlink{bonus}{\beamerreturnbutton{Back}}
\end{frame}
\end{document}