%% /home/plescann/MIM-1/LOGIQUE/LAMBDA/transp.tex

%% Time-stamp: <modifié par Pierre Lescanne le 28 Nov 2001 à 10h47>

\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips

\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips

\slidesmag{5}
\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*


\title{\color{red}{\textit{Lambda-calcul simplement typé}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\rougeMa}[1]{\textcolor{red}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\fleche}{\rightarrow}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\eqa}{\mathop{\equiv_\alpha}}
\newcommand{\Y}{\mathsf{Y}}
\newcommand{\ali}{\newline\hspace*{20pt}}


\newcommand{\inferTwoLabel}[4]{
{#1} \quad 
 \bl{\begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{
 {#1} \quad
  \bl{\begin{array}{c}
  #2
  \end{array}}}

\newcommand{\inferLabel}[3]{
    {#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}

 \newcommand{\inferTwo}[3]{\bl{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}}

 \newcommand{\infer}[2]{\bl{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<<->>}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}

%%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
  \begin{center}                % mais ca peut t'interesser
    \large\bf
    \color{cyan}{\shadowbox{#1}}%
  \end{center}
  \markright{#1}
  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}

%------------------------------------------------------
\begin{slide}
  \maketitle \addtocounter{slide}{-1} \slidepagestyle{empty}


\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
\bleu{\Omega} et \bleu{\Y}  contiennent des termes qui s'appliquent à
eux-mêmes.  

Le \rouge{paradoxe du barbier} est:

\begin{quotation}
\VERT{Le barbier rase tous ceux qui ne se rasent pas eux-mêmes. \emph{Qui rase le
barbier} ?}
\end{quotation}

Pour éviter les paradoxes, on cherche à éviter de tels termes.

On va donc \rouge{typer} les termes.

C'est aussi bien pour la programmation. 
\end{slide}
%------------------------------------------------------
\begin{slide}
Le typage a donc deux objectifs:
\begin{itemize}
\item préserver la correction, \VERT{rien de mauvais ne peut arriver},
\item préserver la terminaison, \VERT{toutes les réductions se terminent}. 
\end{itemize}
\vspace*{8pt}
En $\lambda$-calcul la \rouge{terminaison} s'appelle la \rouge{normalisation forte}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les environnements} 

Il faut typer les variables libres, il faut donc faire des hypothèses
sur les types de ces variables.

D'où la notion d'\rouge{environnement}.

Un environnement est un ensemble d'association de types à des variables.

\bl{
\begin{displaymath}
  \label{eq:env}
  \Gamma \equiv x_1:\sigma_1,...,x_n:\sigma_n
\end{displaymath}}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les types} 
Un \rouge{jugement} est l'affirmation du type \bleu{\sigma} d'un terme
\bleu{M} sous un certain environnement \bleu{\Gamma}:
\bl{
\begin{displaymath}
  \label{eq:jug}
  \Gamma \vdash M:\sigma
\end{displaymath}}
Les types sont
\begin{itemize}
\item soit des variables \bleu{\alpha},
\item soit des types applications \bleu{\sigma \fleche \tau}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles} 
\[\leafLabel{\mbox{(Var)}}{\Gamma, x:\sigma \vdash x:\sigma}\]

\[\inferLabel{\mbox{(Abs)}}{\Gamma, x:\sigma \vdash
  M:\tau}{\Gamma\vdash \lambda x . M:\sigma\fleche\tau}\]

\[\inferTwoLabel{\mbox{(App)}}{\Gamma\vdash
  M:\sigma\fleche\tau}{\Gamma\vdash N:\sigma}{\Gamma\vdash M N :
  \tau}\]

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercices} 
Typez les termes 

\bleu{B\equiv \lambda x y z. x (y z)}, 

\bleu{I \equiv \lambda x. x},

\bleu{C\equiv \lambda x y z. x z y}, 

\bleu{K \equiv \lambda x y . x}, 

\bleu{S \equiv \lambda x y z . x z (y z)}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercices (suite)} 

\vspace*{20pt}

\begin{enumerate}
\item Typez \bleu{I I \equiv (\lambda x. x)(\lambda x. x)}.

  
\item 
  Typez \bleu{\textbf{2}\textbf{2} \equiv (\lambda f x. f(f x))
    (\lambda f x. f(f x))}.

\item A-t-on le même type pour \bleu{I} (resp. \bleu{\textbf{2}}) dans 
  chaque cas?
\end{enumerate}

\VERT{Conclusion :}  Le système de types simples n'est pas assez général.  Il
ne permet d'affecter un type unique à chaque terme.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.

\rouge{$\bullet$} Si \bleu{M \equiv y} alors \bleu{\Gamma} contient
\bleu{y:\tau} et \bleu{M[x:=N]\equiv M\equiv y} donc le résultat
qui   est \bleu{\Gamma\vdash y:\tau} est clair.

\rouge{$\bullet$} Si \bleu{M \equiv x} alors \bleu{\tau=\sigma} et \bleu{M[x:=N]\equiv
    N} et le résultat est l'une des hypothèses.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}

\rouge{Démonstration :}  Par induction sur \bleu{M}.

 \rouge{$\bullet$}  Si \bleu{M \equiv P~Q} alors par (App) pour un certain \bleu{\tau'}, on a
 \begin{itemize}
 \item \bleu{\Gamma, x:\sigma \vdash P:\tau'\rightarrow \tau} duquel
   on tire par induction \bleu{\Gamma\vdash P[x:=N]:\tau'\rightarrow
     \tau}
 \item et \bleu{\Gamma, x:\sigma \vdash Q:\tau'} duquel on tire par
   induction \bleu{\Gamma\vdash Q[x:=N]:\tau'}.
\end{itemize}
Donc par (App) \bleu{\Gamma\vdash
      (P~Q)[x:=N]:\tau} puisque \bleu{(P~Q)[x:=N]\equiv P[x:=N]~Q[x:=N]}.

\rouge{$\bullet$} Le cas \bleu{M \equiv \lambda x.P} est similaire.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Réduction du sujet} 
\rouge{Lemme} \VERT{Réduction du sujet}

La $\beta$-réduction préserve le type.

\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}

\rouge{Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x .M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x .M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\item \rouge{Les autres cas sont similaires.}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Commentaires}
\begin{itemize}
\item Si un terme est d'un certain type, \rouge{il n'en sortira pas} par
  $\beta$-réduction. 
\item Si un terme a une forme normale et s'il a un type, alors \rouge{sa
  forme normale a ce type}.
\end{itemize}
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'isomorphisme de Curry-Howard} 
\begin{small}
\begin{math}
\begin{array}{c | c}
\leafLabel{\mbox{\VERT{(Var)}}}{\Gamma,\rouge{ x:}~\sigma \vdash \rouge{x:}~\sigma} & \bl{\Gamma, p \vdash p}\\

\inferLabel{\mbox{\VERT{(Abs)}}}{\Gamma, \rouge{x:}~\sigma \vdash
 \rouge{M:}~\tau}{\Gamma\vdash \rouge{\lambda x . M:}~\sigma\fleche\tau} 
& \inferLabel{\VERT{\Ra I}}{\Gamma, p \vdash q}{\Gamma\vdash p\Ra q} \\

\inferTwoLabel{\mbox{\VERT{(App)}}}{\Gamma\vdash
 \rouge{M:}~\sigma\fleche\tau}{\Gamma\vdash \rouge{N:}~\sigma}{\Gamma\vdash \rouge{M N :}~
  \tau} & \inferTwoLabel{\VERT{\Ra E}}{\Gamma\vdash p\Ra q}{\Gamma\vdash
  p}{\Gamma\vdash q} \\
\end{array}
\end{math}
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'isomorphisme de Curry-Howard}
Dans \bleu{\Gamma\vdash \rouge{M:}~\sigma}, 
\begin{itemize}
\item  \rouge{M:} est une \rouge{annotation} qui est le \rouge{«terme de preuve»},

\item \bleu{\sigma} peut-être vu comme un \rouge{type} ou comme une \rouge{proposition}.
\end{itemize}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'isomorphisme de Curry-Howard}
On obtient le tableau de correspondance:

\vspace*{5pt}

\begin{Large}
\begin{center}
\begin{tabular}{c | c}
\VERT{types} & \VERT{propositions}\\
\VERT{termes} & \VERT{preuves}\\
\VERT{réduction} & \VERT{simplification des preuves}
\end{tabular}
\end{center}
\end{Large}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Normalisation forte}
\rouge{Définition :}   Un terme \bleu{M} est \VERT{fortement normalisable} si
toute suite de réductions \bleu{M \rabeta M_1 \rabeta ...\rabeta M_n
  ...} est finie.

\vspace{10pt}

\rouge{Théorème :} Si \bleu{\Gamma \vdash M: \tau} alors \bleu{M} est
\VERT{fortement normalisable}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
  
  \framebox{\parbox{9.5cm}{\rouge{Lemme:} Si \bleu{A}, \bleu{B} et
      \bleu{\vec{C}} \VERT{sont fortement normalisables} \ali et
      \bleu{A B \vec{C}} \VERT{n'est pas fortement normalisable} \ali
      alors il y a un \bleu{D} tel que
\begin{enumerate}
\item \bleu{A\rarabeta \lambda x. D}
\item \bleu{D[x:=B] \vec{C}} \VERT{n'est pas fortement normalisable}.
\end{enumerate}}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
  
  \framebox{\parbox{2cm}{\rouge{Démonstration:}}}

Puisque \bleu{A}, \bleu{B} et
      \bleu{\vec{C}} \VERT{sont fortement normalisables}, la réduction
      infinie qui part de \bleu{A B \vec{C}} est de la forme 
\bl{\[A B \vec{C}\rarabeta (\lambda x.D) B_1 \vec{C_1} \rabeta
D[x:=B_1]\vec{C_1} \rarabeta ...\]}

Mézalors les résultat vient immédiatement du fait que 
\bl{
\[D[x:=B] \vec{C} \rarabeta D[x:=B_1]\vec{C_1}.\]
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
  
  \framebox{\parbox{7cm}{\rouge{Lemme:} 
Si \bleu{P} est \VERT{typé}
\ali et si  \bleu{M} et \bleu{P} sont \VERT{fortement normalisables},
\ali alors \bleu{M[x:=P]} est \VERT{fortement normalisable}.
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
  
  \framebox{\parbox{2cm}{\rouge{Démonstration:}}}

Par induction sur le triplet \bleu{(type(P), h(M), taille(M))}, où
\begin{itemize}
\item où \bleu{type(P)} est la complexité du type de \bleu{P},
\item \bleu{h(M)} (ou hauteur) est la longueur de la plus longue
  réduction qui commence en~\bleu{M},
\item  \bleu{taille(M)} est la taille de \bleu{M}.
\end{itemize}

Les cas où \bleu{M} est une abstraction \bleu{\lambda y . N} ou de la
forme \bleu{y \vec{R}} sont faciles et laissés au lecteur.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{itemize}
  \item \rouge{$M = (\lambda y . L) Q \vec{R}$} 
 
Par induction, \bleu{L[x:=P]}, \bleu{Q[x:=P]} et \bleu{\vec{R}[x:=P]}
sont fortement normalisables.

Par le lemme précédent, il suffit de montrer que
\bleu{L[x:=P][y:=Q[x:=P]]\ \vec{R}[x:=P]} \rouge{$\equiv$} \bleu{D[x:=P]}
\ali où \bleu{D} \rouge{$\equiv$} \bleu{L[y:=Q]\ \vec{R}} est fortement
normalisable .

Or \bleu{h(D) < h(M)} donc par induction \bleu{M[x:=P]} est fortement
normalisable.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{itemize}
  \item \rouge{$M = x L \vec{Q}$} 

    \begin{small}
    Par induction, \bleu{L' \equiv L[x:=P]} et \bleu{\vec{Q'} \equiv
      \vec{Q}[x:=P]} sont fortement normalisables.


Par le lemme précédent, il suffit de montrer que si \bleu{P\rarabeta
  \lambda y. P_1} alors \bleu{M'} \rouge{$\equiv$}
\bleu{P_1[y:=L']\vec{Q'}} est fortement
normalisable.

Puisque \bleu{type(L')<type(P)}, on peut appliquer l'hypothèse de
récurrence et donc \bleu{P_1[y:=L']} est fortement
normalisable.

Et ainsi par induction 
\begin{itemize}
\item parce que \bl{ \(M' {\color{red}\equiv} (z
    \vec{Q'})[z:=P_1[y:=L']]\) } est fortement normalisable 
\item et que \bleu{type(P_1)<type(P)},
\end{itemize}
on conclut
que \bleu{M[x:=P]} est fortement normalisable.
\end{small}
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Normalisation forte (démonstration)} 
Le théorème est prouvé par induction structurelle sur le terme dont on
cherche à prouver la normalisation forte.

\begin{itemize}
\item \rouge{Le terme est une variable ou une abstraction} c'est clair.
\item \rouge{Le terme est une application } \bleu{P\ Q} \rouge{$\equiv$}
  \bleu{(z Q)[z:=P]} \ali alors c'est évident par le lemme précédent et par
    induction structurelle.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\end{document}
