# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1278879482 -3600
# Node ID b38f8d5e0b093ff5f3aa1ef7115f4e932b811788
# Parent  e2be455093a17de7b7890834247bbe9c40579d8b
slides

diff -r e2be455093a1 -r b38f8d5e0b09 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Sun Jul 11 00:58:54 2010 +0100
+++ b/Slides/Slides2.thy	Sun Jul 11 21:18:02 2010 +0100
@@ -44,7 +44,7 @@
   terms involving binders (e.g.~lambda calculus, variable convention)\medskip
   
   \item<2-> \ldots mainly used to find errors in my own 
-  (published) paper proofs and in that of others \alert{\bf ;o)}
+  (published) paper proofs and in those of others \alert{\bf ;o)}
   \end{itemize}
 
   \end{frame}}
@@ -57,7 +57,7 @@
   \begin{frame}<1-3>[c]
   \frametitle{Nominal Theory}
   
-  by Pitts; at its core are:\bigskip
+  \ldots by Pitts; at its core are:\bigskip
 
   \begin{itemize}
   \item sorted atoms and 
@@ -137,6 +137,8 @@
   \item<2-> $\text{[]}\,\act\, x = x$
   \item<2-> $(\pi_1 @  \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$
   \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$
+  \item<2-> if $\pi_1$, $\pi_2$ have dif$\!$f.~type, then
+    $\pi_1 \act (\pi_2 \act x) = \pi_2 \act (\pi_1 \act x)$
   \end{itemize}
   \end{itemize}
 
@@ -161,7 +163,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-5>
+  \begin{frame}<1-4>
   \frametitle{A Better Way}
 *}
 datatype atom = Atom string nat
@@ -169,27 +171,27 @@
 text_raw {*
   \mbox{}\bigskip
   \begin{itemize}
-  \item<3-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
+  \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
 
      \begin{itemize}
      \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)
      \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
      \end{itemize}\medskip
      
-  \item<4-> \alert{What about {\bf swappings}?}
+  \item<3-> \alert{What about {\bf swappings}?}
      \small
      \[
      \begin{array}{l@ {\hspace{1mm}}l}
      (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
         & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
           \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
-        & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
-          \only<5->{\text{\alert{\bf id}}}
+        & \text{else}\;\only<3>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
+          \only<4->{\text{\alert{\bf id}}}
      \end{array}
      \]
   \end{itemize}
 
-  \only<3>{
+  \only<2>{
   \begin{textblock}{7}(4,11)
   @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   \end{textblock}}
@@ -270,7 +272,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1-2>
-  \frametitle{Solution}
+  \frametitle{Our Solution}
 
 
   \begin{itemize}
@@ -408,12 +410,12 @@
 
   \begin{itemize}
   \item the formalised version of the nominal theory is now much nicer to 
-  work with (sorts are occasionally explicit, \alert{@{text "\<forall>\<pi>. P"}})\medskip
+  work with (sorts are occasionally explicit, \alert{$\forall \pi. P$})\medskip
 
   \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip
 
-  \item crucial insight: allow sort-disrespecting swappings%
-  \onslide<2->{ just define them as the identity}%
+  \item the crucial insight: allow sort-disrespecting swappings%
+  \onslide<2->{ \ldots just define them as the identity}\\%
   \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
 
   \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}
diff -r e2be455093a1 -r b38f8d5e0b09 Slides/Slides3.thy
--- a/Slides/Slides3.thy	Sun Jul 11 00:58:54 2010 +0100
+++ b/Slides/Slides3.thy	Sun Jul 11 21:18:02 2010 +0100
@@ -9,24 +9,54 @@
 
 (*>*)
 
+text_raw {*
+  \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Quiz}
+  
+  Assuming that \smath{a} and \smath{b} are distinct variables,\\
+  is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7} 
+  that make the following pairs \alert{$\alpha$-equivalent}?
+
+  \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
+  \begin{itemize}
+  \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_1)\;}
+
+  \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_3)\;}
+
+  \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_5)\;}
+
+  \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 
+        \smath{\lambda a.\lambda a. (a\,M_7)\;}
+  \end{itemize}
+  \end{tabular}
+
+  If there is one solution for a pair, can you describe all its solutions?
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
-  \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1>[t]
   \frametitle{%
   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
   \\
-  \huge Nominal 2\\[-2mm] 
-  \large Or, How to Reason Conveniently with\\[-5mm]
-  \large General Bindings in Isabelle/HOL\\[5mm]
+  \huge Nominal Unification\\[-2mm] 
+  \Large Hitting a Sweet Spot\\[5mm]
   \end{tabular}}
   \begin{center}
   Christian Urban
   \end{center}
   \begin{center}
-  joint work with {\bf Cezary Kaliszyk}\\[0mm] 
+  \small initial work with Andy Pitts and Jamie Gabbay\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%