52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
53 \mode<presentation>{ |
53 \mode<presentation>{ |
54 \begin{frame}<1->[c] |
54 \begin{frame}<1->[c] |
55 \frametitle{} |
55 \frametitle{} |
56 |
56 |
57 \begin{itemize} |
57 \begin{center} |
58 \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{} |
58 \begin{tabular}{@ {\hspace{-2mm}}c@ {}} |
|
59 \includegraphics[scale=0.36]{phd-2.jpg}\, |
|
60 \includegraphics[scale=0.36]{phd-1.jpg}\\ |
|
61 \hfill\textcolor{gray}{\small dinner after my PhD examination} |
|
62 \end{tabular} |
|
63 \end{center} |
|
64 |
|
65 \end{frame}} |
|
66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
67 *} |
|
68 |
|
69 text_raw {* |
|
70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
71 \mode<presentation>{ |
|
72 \begin{frame}<1->[c] |
|
73 \frametitle{} |
|
74 |
|
75 \begin{itemize} |
|
76 \item \normalsize Aim: develop Nominal Isabelle for reasoning formally about |
|
77 programming languages\\[-10mm]\mbox{} |
59 \end{itemize} |
78 \end{itemize} |
60 |
79 |
61 \begin{center} |
80 \begin{center} |
62 \begin{block}{} |
81 \begin{block}{} |
63 \color{gray} |
82 \color{gray} |
74 \begin{itemize} |
93 \begin{itemize} |
75 \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning |
94 \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning |
76 about LF (and fixed it in three ways) |
95 about LF (and fixed it in three ways) |
77 \item found also fixable errors in my Ph.D.-thesis about cut-elimination |
96 \item found also fixable errors in my Ph.D.-thesis about cut-elimination |
78 (examined by Henk Barendregt and Andy Pitts) |
97 (examined by Henk Barendregt and Andy Pitts) |
79 \item found the variable convention can in principle be used for proving false |
98 \item found that the variable convention can in principle be used for proving false |
80 \end{itemize} |
99 \end{itemize} |
81 |
100 |
82 \end{frame}} |
101 \end{frame}} |
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
84 *} |
103 *} |
125 |
144 |
126 \begin{itemize} |
145 \begin{itemize} |
127 \item a general theory about atoms and permutations\medskip |
146 \item a general theory about atoms and permutations\medskip |
128 \begin{itemize} |
147 \begin{itemize} |
129 \item sorted atoms and |
148 \item sorted atoms and |
130 \item sort-respecting permutations |
149 \item sort-respecting permutations\bigskip |
131 \end{itemize} |
150 \end{itemize} |
132 |
151 |
133 \item support and freshness |
152 \item support and freshness |
134 \begin{center} |
153 \begin{center} |
135 \begin{tabular}{l} |
154 \begin{tabular}{l} |
136 \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\ |
155 \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm] |
137 \smath{a \fresh x \dn a \notin \textit{supp}(x)} |
156 \smath{a \fresh x \dn a \notin \textit{supp}(x)} |
138 \end{tabular} |
157 \end{tabular} |
139 \end{center}\bigskip\pause |
158 \end{center}\bigskip\pause |
140 |
159 |
141 \item allow users to reason about alpha-equivalence classes like about |
160 \item allow users to reason about alpha-equivalence classes as if they were |
142 syntax trees |
161 syntax trees |
143 % |
162 % |
144 %\item $\alpha$-equivalence |
163 %\item $\alpha$-equivalence |
145 %\begin{center} |
164 %\begin{center} |
146 %\begin{tabular}{l} |
165 %\begin{tabular}{l} |
192 \end{center} |
211 \end{center} |
193 |
212 |
194 \begin{textblock}{9}(2.8,12.5) |
213 \begin{textblock}{9}(2.8,12.5) |
195 \only<7>{ |
214 \only<7>{ |
196 \begin{tikzpicture} |
215 \begin{tikzpicture} |
197 \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn) |
216 \draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn) |
198 {The ``new types'' are the reason why there is no Nominal Coq.}; |
217 {The ``new types mechanism'' is the reason why there is no Nominal Coq.}; |
199 \end{tikzpicture}} |
218 \end{tikzpicture}} |
200 \end{textblock} |
219 \end{textblock} |
201 |
220 |
202 \end{frame}} |
221 \end{frame}} |
203 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
222 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
208 \mode<presentation>{ |
227 \mode<presentation>{ |
209 \begin{frame}<1-3>[c] |
228 \begin{frame}<1-3>[c] |
210 \frametitle{HOL vs.~Nominal} |
229 \frametitle{HOL vs.~Nominal} |
211 |
230 |
212 \begin{itemize} |
231 \begin{itemize} |
213 \item Nominal logic by Pitts are incompatible |
232 \item Nominal logic by Pitts is incompatible |
214 with choice principles\medskip |
233 with choice principles\medskip |
215 |
234 |
216 \item HOL includes Hilbert's epsilon\pause\bigskip |
235 \item but HOL includes Hilbert's epsilon\pause\bigskip |
217 |
236 |
218 \item The solution: Do not require that everything has finite support\medskip |
237 \item The solution: Do not require that everything has finite support\medskip |
219 |
238 |
220 \begin{center} |
239 \begin{center} |
221 \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x} |
240 \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x} |
252 \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};} |
271 \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};} |
253 |
272 |
254 \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);} |
273 \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);} |
255 \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};} |
274 \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};} |
256 |
275 |
257 \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);} |
276 %%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);} |
258 \end{tikzpicture} |
277 \end{tikzpicture} |
259 \end{center} |
278 \end{center} |
260 |
279 |
261 \begin{textblock}{9.5}(6,3.5) |
280 \begin{textblock}{9.5}(6,3.5) |
262 \begin{itemize} |
281 \begin{itemize} |
263 \item<1-> defined fv and $\alpha$ |
282 \item<1-> define fv and $\alpha$ |
264 \item<2-> built quotient / new type |
283 \item<2-> build quotient / new type |
265 \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) |
284 \item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) |
266 \item<4-> derive a {\bf stronger} cases lemma |
285 \item<4-> derive a {\bf stronger} cases lemma |
267 \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\ |
286 \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\ |
268 \begin{center} |
287 \begin{center} |
269 \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} |
288 \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} |
270 \end{center} |
289 \end{center} |
282 \mode<presentation>{ |
301 \mode<presentation>{ |
283 \begin{frame} |
302 \begin{frame} |
284 \frametitle{Nominal Isabelle} |
303 \frametitle{Nominal Isabelle} |
285 |
304 |
286 \begin{itemize} |
305 \begin{itemize} |
287 \item Users can define lambda-terms as: |
306 \item Users can for example define lambda-terms as: |
288 \end{itemize} |
307 \end{itemize} |
289 *} |
308 *} |
290 |
309 |
291 atom_decl name text_raw {*\medskip\isanewline *} |
310 atom_decl name text_raw {*\medskip\isanewline *} |
292 nominal_datatype lam = |
311 nominal_datatype lam = |
293 Var "name" |
312 Var name |
294 | App "lam" "lam" |
313 | App lam lam |
295 | Lam x::"name" t::"lam" binds x in t ("Lam _. _") |
314 | Lam x::name t::lam binds x in t ("Lam _. _") |
296 |
315 |
297 |
316 |
298 text_raw {* |
317 text_raw {* |
299 \mbox{}\bigskip |
318 \mbox{}\bigskip |
300 |
319 |
662 By the variable convention we conclude that \smath{x\not= y}. |
681 By the variable convention we conclude that \smath{x\not= y}. |
663 }; |
682 }; |
664 \end{tikzpicture}} |
683 \end{tikzpicture}} |
665 \end{textblock} |
684 \end{textblock} |
666 |
685 |
667 \begin{textblock}{9.2}(3.6,9) |
686 \begin{textblock}{9.2}(3.6,9.2) |
668 \only<6,7>{ |
687 \only<6,7>{ |
669 \begin{tikzpicture}[remember picture] |
688 \begin{tikzpicture}[remember picture] |
670 \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb) |
689 \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb) |
671 {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow |
690 {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow |
672 y\!\not\in\! \text{fv}(t)\!-\!\{x\} |
691 y\!\not\in\! \text{fv}(t)\!-\!\{x\} |