9 |
9 |
10 (*>*) |
10 (*>*) |
11 |
11 |
12 |
12 |
13 text_raw {* |
13 text_raw {* |
14 \renewcommand{\slidecaption}{TU Munich, 28.~May 2010} |
14 \renewcommand{\slidecaption}{Edinburgh, 11.~July 2010} |
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
16 \mode<presentation>{ |
16 \mode<presentation>{ |
17 \begin{frame}<1>[t] |
17 \begin{frame}<1>[t] |
18 \frametitle{% |
18 \frametitle{% |
19 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
19 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
20 \\ |
20 \\ |
21 \huge Nominal 2\\[-2mm] |
21 \LARGE Proof Pearl:\\[-2mm] |
22 \large Or, How to Reason Conveniently with\\[-5mm] |
22 \LARGE A New Foundation for\\[-2mm] |
23 \large General Bindings in Isabelle\\[15mm] |
23 \LARGE Nominal Isabelle\\[12mm] |
24 \end{tabular}} |
24 \end{tabular}} |
25 \begin{center} |
25 \begin{center} |
26 joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] |
26 \small |
|
27 Brian Huf\!fman and {\bf Christian Urban}\\[0mm] |
27 \end{center} |
28 \end{center} |
28 \end{frame}} |
29 \end{frame}} |
29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
30 |
31 |
31 *} |
32 *} |
32 |
33 |
33 text_raw {* |
34 text_raw {* |
34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
35 \mode<presentation>{ |
36 \mode<presentation>{ |
36 \begin{frame}<1-2> |
37 \begin{frame}<1-2> |
37 \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} |
38 \frametitle{\begin{tabular}{c}Nominal Isabelle\end{tabular}} |
|
39 \mbox{}\\[-3mm] |
|
40 |
|
41 \begin{itemize} |
|
42 \item sorted atoms and sort-respecting permutations\medskip |
|
43 |
|
44 \onslide<2->{ |
|
45 \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip |
|
46 |
|
47 \begin{center} |
|
48 \begin{tabular}{c@ {\hspace{7mm}}c} |
|
49 $[]\;\act\;c \dn c$ & |
|
50 $(a\;b)\!::\!\pi\;\act\;c \dn$ |
|
51 $\begin{cases} |
|
52 b & \text{if}\; \pi \act c = a\\ |
|
53 a & \text{if}\; \pi \act c = b\\ |
|
54 \pi \act c & \text{otherwise} |
|
55 \end{cases}$ |
|
56 \end{tabular} |
|
57 \end{center}} |
|
58 \end{itemize} |
|
59 |
|
60 \end{frame}} |
|
61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
62 *} |
|
63 |
|
64 text_raw {* |
|
65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
66 \mode<presentation>{ |
|
67 \begin{frame}<1-2> |
|
68 \frametitle{\begin{tabular}{c}Nominal Theory\end{tabular}} |
38 \mbox{}\\[-3mm] |
69 \mbox{}\\[-3mm] |
39 |
70 |
40 \begin{itemize} |
71 \begin{itemize} |
41 \item sorted atoms and sort-respecting permutations\medskip |
72 \item sorted atoms and sort-respecting permutations\medskip |
42 |
73 |