12 

    12 text_raw {*

    13 text_raw {*

    13   \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}

    14   \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}

    14   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    15   \mode<presentation>{

    16   \begin{frame}<1>[c]

    17   \frametitle{Quiz}

    18   

    19   Assuming that \smath{a} and \smath{b} are distinct variables,\\

    20   is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7} 

    21   that make the following pairs \alert{$\alpha$-equivalent}?

    22 

    23   \begin{tabular}{@ {\hspace{14mm}}p{12cm}}

    24   \begin{itemize}

    25   \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 

    26         \smath{\lambda b.\lambda a. (a\,M_1)\;}

    27 

    28   \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and 

    29         \smath{\lambda b.\lambda a. (a\,M_3)\;}

    30 

    31   \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and 

    32         \smath{\lambda b.\lambda a. (a\,M_5)\;}

    33 

    34   \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 

    35         \smath{\lambda a.\lambda a. (a\,M_7)\;}

    36   \end{itemize}

    37   \end{tabular}

    38 

    39   If there is one solution for a pair, can you describe all its solutions?

    40 

    41   \end{frame}}

    42   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    43 *}

    44 

    45 text_raw {*

    21   \huge Nominal 2\\[-2mm] 

    52   \huge Nominal Unification\\[-2mm] 

    22   \large Or, How to Reason Conveniently with\\[-5mm]

    53   \Large Hitting a Sweet Spot\\[5mm]

    23   \large General Bindings in Isabelle/HOL\\[5mm]

    29   joint work with {\bf Cezary Kaliszyk}\\[0mm] 

    59   \small initial work with Andy Pitts and Jamie Gabbay\\[0mm]