--- a/Slides/SlidesB.thy Sun Oct 13 23:09:21 2013 +0200
+++ b/Slides/SlidesB.thy Mon Oct 14 11:23:18 2013 +0200
@@ -27,7 +27,7 @@
\begin{center}
Christian Urban\\[1mm]
- King's College London\\[-6mm]\mbox{}
+ King's College London\\[-4mm]\mbox{}
\end{center}
\begin{center}
@@ -54,8 +54,27 @@
\begin{frame}<1->[c]
\frametitle{}
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-2mm}}c@ {}}
+ \includegraphics[scale=0.36]{phd-2.jpg}\,
+ \includegraphics[scale=0.36]{phd-1.jpg}\\
+ \hfill\textcolor{gray}{\small dinner after my PhD examination}
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{}
+
\begin{itemize}
- \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
+ \item \normalsize Aim: develop Nominal Isabelle for reasoning formally about
+ programming languages\\[-10mm]\mbox{}
\end{itemize}
\begin{center}
@@ -76,7 +95,7 @@
about LF (and fixed it in three ways)
\item found also fixable errors in my Ph.D.-thesis about cut-elimination
(examined by Henk Barendregt and Andy Pitts)
- \item found the variable convention can in principle be used for proving false
+ \item found that the variable convention can in principle be used for proving false
\end{itemize}
\end{frame}}
@@ -127,18 +146,18 @@
\item a general theory about atoms and permutations\medskip
\begin{itemize}
\item sorted atoms and
- \item sort-respecting permutations
+ \item sort-respecting permutations\bigskip
\end{itemize}
\item support and freshness
\begin{center}
\begin{tabular}{l}
- \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\
+ \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm]
\smath{a \fresh x \dn a \notin \textit{supp}(x)}
\end{tabular}
\end{center}\bigskip\pause
- \item allow users to reason about alpha-equivalence classes like about
+ \item allow users to reason about alpha-equivalence classes as if they were
syntax trees
%
%\item $\alpha$-equivalence
@@ -194,8 +213,8 @@
\begin{textblock}{9}(2.8,12.5)
\only<7>{
\begin{tikzpicture}
- \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn)
- {The ``new types'' are the reason why there is no Nominal Coq.};
+ \draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn)
+ {The ``new types mechanism'' is the reason why there is no Nominal Coq.};
\end{tikzpicture}}
\end{textblock}
@@ -210,10 +229,10 @@
\frametitle{HOL vs.~Nominal}
\begin{itemize}
- \item Nominal logic by Pitts are incompatible
+ \item Nominal logic by Pitts is incompatible
with choice principles\medskip
- \item HOL includes Hilbert's epsilon\pause\bigskip
+ \item but HOL includes Hilbert's epsilon\pause\bigskip
\item The solution: Do not require that everything has finite support\medskip
@@ -254,15 +273,15 @@
\onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
\onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
- \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+ %%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
\end{tikzpicture}
\end{center}
\begin{textblock}{9.5}(6,3.5)
\begin{itemize}
- \item<1-> defined fv and $\alpha$
- \item<2-> built quotient / new type
- \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots)
+ \item<1-> define fv and $\alpha$
+ \item<2-> build quotient / new type
+ \item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots)
\item<4-> derive a {\bf stronger} cases lemma
\item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
\begin{center}
@@ -284,15 +303,15 @@
\frametitle{Nominal Isabelle}
\begin{itemize}
- \item Users can define lambda-terms as:
+ \item Users can for example define lambda-terms as:
\end{itemize}
*}
atom_decl name text_raw {*\medskip\isanewline *}
nominal_datatype lam =
- Var "name"
- | App "lam" "lam"
- | Lam x::"name" t::"lam" binds x in t ("Lam _. _")
+ Var name
+ | App lam lam
+ | Lam x::name t::lam binds x in t ("Lam _. _")
text_raw {*
@@ -335,7 +354,7 @@
\end{center}
\item It requires us in the lambda-case to show the property \smath{P} for
- all binders \smath{x}.\smallskip\\
+ all binders \smath{x}.\medskip\\
(This nearly always requires renamings and they can be
tricky to automate.)
@@ -664,7 +683,7 @@
\end{tikzpicture}}
\end{textblock}
- \begin{textblock}{9.2}(3.6,9)
+ \begin{textblock}{9.2}(3.6,9.2)
\only<6,7>{
\begin{tikzpicture}[remember picture]
\draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)