50 \begin{frame}<1->[c] |
46 \begin{frame}<1->[c] |
51 \frametitle{} |
47 \frametitle{} |
52 |
48 |
53 \mbox{}\\[2mm] |
49 \mbox{}\\[2mm] |
54 \begin{itemize} |
50 \begin{itemize} |
55 \item my background is in |
51 \item my background is in: |
56 \begin{itemize} |
52 \begin{itemize} |
57 \item \normalsize programming languages and theorem provers |
53 \item \normalsize programming languages and |
58 \item \normalsize develop Nominal Isabelle |
54 \item \normalsize theorem provers |
59 \end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip |
55 \end{itemize}\medskip |
60 |
56 |
61 \item<1->to formalise and mechanically check proofs from |
57 \item \normalsize develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{} |
62 programming language research, TCS \textcolor{gray}{and OS}\bigskip |
58 \end{itemize} |
63 |
59 |
64 \item<2->we found out that the variable convention can lead to |
|
65 faulty proofs\ldots |
|
66 \end{itemize} |
|
67 |
|
68 \onslide<2->{ |
|
69 \begin{center} |
60 \begin{center} |
70 \begin{block}{} |
61 \begin{block}{} |
71 \color{gray} |
62 \color{gray} |
72 \footnotesize |
63 \footnotesize |
73 {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] |
64 {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] |
74 If $M_1,\ldots,M_n$ occur in a certain mathematical context |
65 If $M_1,\ldots,M_n$ occur in a certain mathematical context |
75 (e.g. definition, proof), then in these terms all bound variables |
66 (e.g. definition, proof), then in these terms all bound variables |
76 are chosen to be different from the free variables.\hfill Henk Barendregt |
67 are chosen to be different from the free variables.\hfill ---Henk Barendregt |
77 \end{block} |
68 \end{block} |
78 \end{center}} |
69 \end{center}\pause |
79 |
70 |
80 |
71 \mbox{}\\[-19mm]\mbox{} |
81 \only<1->{ |
72 |
82 \begin{textblock}{6}(10.9,3.5) |
73 \begin{itemize} |
83 \includegraphics[scale=0.23]{isabelle1.png} |
74 \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning |
84 \end{textblock}} |
75 about LF (and fixed it in three ways) |
85 |
76 \end{itemize} |
86 |
77 |
87 |
78 \end{frame}} |
88 \end{frame}} |
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
80 *} |
90 *} |
|
91 |
|
92 |
|
93 |
81 |
94 |
82 |
95 text_raw {* |
83 text_raw {* |
96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
97 \mode<presentation>{ |
85 \mode<presentation>{ |
98 \begin{frame}[c] |
86 \begin{frame}[c] |
99 \frametitle{} |
87 \frametitle{} |
100 |
88 |
101 \begin{tabular}{c@ {\hspace{2mm}}c} |
89 \begin{itemize} |
102 \\[6mm] |
90 \item found also fixable errors in my Ph.D.-thesis about cut-elimination |
103 \begin{tabular}{c} |
|
104 \includegraphics[scale=0.11]{harper.jpg}\\[-2mm] |
|
105 {\footnotesize Bob Harper}\\[-2.5mm] |
|
106 {\footnotesize (CMU)} |
|
107 \end{tabular} |
|
108 \begin{tabular}{c} |
|
109 \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] |
|
110 {\footnotesize Frank Pfenning}\\[-2.5mm] |
|
111 {\footnotesize (CMU)} |
|
112 \end{tabular} & |
|
113 |
|
114 \begin{tabular}{p{6cm}} |
|
115 \raggedright |
|
116 \color{gray}{published a proof on LF in\\ {\bf ACM Transactions on Computational Logic}, 2005, |
|
117 $\sim$31pp} |
|
118 \end{tabular}\\ |
|
119 |
|
120 \pause |
|
121 \\[0mm] |
|
122 |
|
123 \begin{tabular}{c} |
|
124 \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] |
|
125 {\footnotesize Andrew Appel}\\[-2.5mm] |
|
126 {\footnotesize (Princeton)} |
|
127 \end{tabular} & |
|
128 |
|
129 \begin{tabular}{p{6cm}} |
|
130 \raggedright |
|
131 \color{gray}{relied on their proof in a\\ {\bf security} critical application\\ (proof-carrying code)} |
|
132 \end{tabular} |
|
133 \end{tabular} |
|
134 |
|
135 |
|
136 |
|
137 \end{frame}} |
|
138 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
139 *} |
|
140 |
|
141 |
|
142 |
|
143 text {* |
|
144 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex] |
|
145 \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, |
|
146 draw=black!50, top color=white, bottom color=black!20] |
|
147 \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, |
|
148 draw=red!70, top color=white, bottom color=red!50!black!20] |
|
149 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
150 \mode<presentation>{ |
|
151 \begin{frame}<2->[squeeze] |
|
152 \frametitle{} |
|
153 |
|
154 \begin{columns} |
|
155 |
|
156 \begin{column}{0.8\textwidth} |
|
157 \begin{textblock}{0}(1,2) |
|
158 |
|
159 \begin{tikzpicture} |
|
160 \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm] |
|
161 { \&[-10mm] |
|
162 \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \& |
|
163 \node (proof1) [node1] {\large Proof}; \& |
|
164 \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\ |
|
165 |
|
166 \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
167 \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \& |
|
168 \onslide<4->{\node (proof2) [node1] {\large Proof};} \& |
|
169 \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
170 |
|
171 \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
172 \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
173 \onslide<5->{\node (proof3) [node1] {\large Proof};} \& |
|
174 \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\ |
|
175 |
|
176 \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
177 \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
178 \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \& |
|
179 \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
180 }; |
|
181 |
|
182 \draw[->,black!50,line width=2mm] (proof1) -- (def1); |
|
183 \draw[->,black!50,line width=2mm] (proof1) -- (alg1); |
|
184 |
|
185 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);} |
|
186 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);} |
|
187 |
|
188 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);} |
|
189 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);} |
|
190 |
|
191 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);} |
|
192 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);} |
|
193 |
|
194 \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} |
|
195 \end{tikzpicture} |
|
196 |
|
197 \end{textblock} |
|
198 \end{column} |
|
199 \end{columns} |
|
200 |
|
201 |
|
202 \begin{textblock}{3}(12,3.6) |
|
203 \onslide<4->{ |
|
204 \begin{tikzpicture} |
|
205 \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; |
|
206 \end{tikzpicture}} |
|
207 \end{textblock} |
|
208 |
|
209 \end{frame}} |
|
210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
211 |
|
212 *} |
|
213 |
|
214 |
|
215 text_raw {* |
|
216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
217 \mode<presentation>{ |
|
218 \begin{frame}[c] |
|
219 \frametitle{} |
|
220 |
|
221 \begin{itemize} |
|
222 \item I also found fixable errors in my Ph.D.-thesis about cut-elimination |
|
223 (examined by Henk Barendregt and Andy Pitts)\bigskip |
91 (examined by Henk Barendregt and Andy Pitts)\bigskip |
224 \item found flaws in a proof about a classic OS scheduling algorithm |
92 |
225 --- helped us to implement\\ it correctly and ef$\!$ficiently\\ |
93 \item formalised a classic OS scheduling algorithm (priority inversion |
226 {\small\textcolor{gray}{(the existing literature ``proved'' |
94 protocol) |
227 correct an incorrect algorithm; used in the Mars Pathfinder mission)}} |
95 \begin{itemize} |
228 \end{itemize}\bigskip\bigskip\pause |
96 \item original algorithm was incorrect even being proved correct (with `pencil-and-paper') |
229 |
97 \item helped us to implement this algorithm correctly and efficiently\\ |
230 |
98 \end{itemize}\bigskip\pause |
231 {\bf Conclusion:}\smallskip |
99 |
232 |
100 \item used Isabelle to prove properties about access controls and OSes |
233 Pencil-and-paper proofs in TCS are not foolproof, |
101 \end{itemize} |
234 not even expertproof. |
|
235 |
|
236 \end{frame}} |
|
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
238 *} |
|
239 |
|
240 |
|
241 text_raw {* |
|
242 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
243 \mode<presentation>{ |
|
244 \begin{frame}[t] |
|
245 |
|
246 \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{} |
|
247 \begin{center} |
|
248 \begin{block}{} |
|
249 \color{gray} |
|
250 \small |
|
251 ``I still remember having to grade hundreds of exams where the |
|
252 students started out by assuming what had to be proved, or filled |
|
253 page after page with gibberish in the hope that, somewhere in the |
|
254 mess, they might accidentally have said something |
|
255 correct. \ldots{}innumerable examples of ``parrot proofs'' --- |
|
256 NP-completeness reductions done in the wrong direction, arguments |
|
257 that look more like LSD trips than coherent chains of logic \ldots{}'' |
|
258 \end{block} |
|
259 \end{center}\pause |
|
260 |
|
261 \begin{tabular}{@ {}c@ {}} |
|
262 Tobias Nipkow calls this the ``London Underground Phenomenon'': |
|
263 \end{tabular} |
|
264 |
|
265 \begin{center} |
|
266 \begin{tabular}{ccc} |
|
267 students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs |
|
268 \end{tabular} |
|
269 \end{center} |
|
270 |
102 |
271 \end{frame}} |
103 \end{frame}} |
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
273 *} |
105 *} |
274 |
106 |
325 |
157 |
326 \begin{textblock}{6}(10.2,2.8) |
158 \begin{textblock}{6}(10.2,2.8) |
327 \footnotesize Isabelle: |
159 \footnotesize Isabelle: |
328 \end{textblock} |
160 \end{textblock} |
329 |
161 |
330 \begin{textblock}{6}(7,12) |
162 \end{frame}} |
331 \footnotesize\textcolor{gray}{students have seen them and can be motivated about them} |
163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
332 \end{textblock} |
164 *} |
333 |
165 |
334 \end{frame}} |
166 text_raw {* |
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
167 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
336 *} |
168 \mode<presentation>{ |
337 |
169 \begin{frame}<1-5>[t] |
338 text_raw {* |
|
339 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
340 \mode<presentation>{ |
|
341 \begin{frame}<1->[t] |
|
342 |
170 |
343 \mbox{}\\[-2mm] |
171 \mbox{}\\[-2mm] |
344 |
172 |
345 \small |
173 \small |
346 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
174 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} |
347 \bl{nullable ($\varnothing$)} & \bl{$=$} & \bl{false} &\\ |
175 \bl{$nullable(\varnothing)$} & \bl{$=$} & \bl{false} &\\ |
348 \bl{nullable ([])} & \bl{$=$} & \bl{true} &\\ |
176 \bl{$nullable([])$} & \bl{$=$} & \bl{true} &\\ |
349 \bl{nullable (c)} & \bl{$=$} & \bl{false} &\\ |
177 \bl{$nullable(c)$} & \bl{$=$} & \bl{false} &\\ |
350 \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ |
178 \bl{$nullable(r_1 + r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \vee nullable(r_2)$} & \\ |
351 \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\ |
179 \bl{$nullable(r_1 \cdot r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} & \\ |
352 \bl{nullable (r$^*$)} & \bl{$=$} & \bl{true} & \\ |
180 \bl{$nullable(r^*)$} & \bl{$=$} & \bl{true} & \\ |
353 \end{tabular}\medskip\pause |
181 \end{tabular}\medskip\pause |
354 |
182 |
355 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
183 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} |
356 \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\ |
184 \bl{$der\,c\,(\varnothing)$} & \bl{$=$} & \bl{$\varnothing$} & \\ |
357 \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\ |
185 \bl{$der\,c\,([])$} & \bl{$=$} & \bl{$\varnothing$} & \\ |
358 \bl{der c (d)} & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\ |
186 \bl{$der\,c\,(d)$} & \bl{$=$} & \bl{if $c = d$ then $[]$ else $\varnothing$} & \\ |
359 \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ |
187 \bl{$der\,c\,(r_1 + r_2)$} & \bl{$=$} & \bl{$der\,c\,r_1 + der\,c\,r_2$} & \\ |
360 \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\ |
188 \bl{$der\,c\,(r_1 \cdot r_2)$} & \bl{$=$} & \bl{if $nullable(r_1)$}\\ |
361 & & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ |
189 & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ |
362 \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ (r$^*$)} &\smallskip\\\pause |
190 & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\ |
363 |
191 \bl{$der\,c\,(r^*)$} & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause |
364 \bl{derivative [] r} & \bl{$=$} & \bl{r} & \\ |
192 |
365 \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\ |
193 \bl{$deriv\,[]\,r$} & \bl{$=$} & \bl{$r$} & \\ |
|
194 \bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\ |
366 \end{tabular}\medskip |
195 \end{tabular}\medskip |
367 |
196 |
368 \bl{matches r s $=$ nullable (derivative s r)} |
197 \bl{$match\,r\,s = nullable (deriv\,s\,r)$} |
369 |
198 |
370 \end{frame}} |
199 \only<4>{ |
371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
200 \begin{textblock}{10.5}(2,5) |
372 *} |
201 \begin{tikzpicture} |
373 |
202 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
374 text_raw {* |
203 {\normalsize\color{darkgray} |
375 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
204 \begin{minipage}{10.5cm} |
376 \mode<presentation>{ |
205 \begin{center} |
377 \begin{frame}[c] |
206 a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip |
378 \frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education} |
207 \end{center} |
379 |
208 |
380 \begin{itemize} |
209 \begin{center} |
381 \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip |
210 b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$} |
382 \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited |
211 \end{center} |
383 for a first-order version''\medskip\bigskip\bigskip\pause |
212 |
384 \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined'' |
213 where |
385 \bigskip |
214 \begin{center} |
386 |
215 \bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$} |
387 \begin{quote}\small |
216 \end{center}\medskip\pause |
388 ``Unfortunately, regular expression derivatives have been lost in the |
217 |
389 sands of time, and few computer scientists are aware of them.'' |
218 \begin{center} |
390 \end{quote} |
219 c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$} |
391 \end{itemize} |
220 \end{center} |
392 |
221 \end{minipage}}; |
393 |
222 \end{tikzpicture} |
394 \end{frame}} |
223 \end{textblock}} |
395 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
224 |
396 |
225 |
397 *} |
226 \end{frame}} |
|
227 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
228 *} |
|
229 |
|
230 text_raw {* |
|
231 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
232 \mode<presentation>{ |
|
233 \begin{frame}[t] |
|
234 \frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} |
|
235 |
|
236 \mbox{}\\[-13mm] |
|
237 |
|
238 \begin{tikzpicture}[y=.2cm, x=.3cm] |
|
239 %axis |
|
240 \draw (0,0) -- coordinate (x axis mid) (30,0); |
|
241 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
242 %ticks |
|
243 \foreach \x in {0,5,...,30} |
|
244 \draw (\x,1pt) -- (\x,-3pt) |
|
245 node[anchor=north] {\x}; |
|
246 \foreach \y in {0,5,...,30} |
|
247 \draw (1pt,\y) -- (-3pt,\y) |
|
248 node[anchor=east] {\y}; |
|
249 %labels |
|
250 \node[below=0.6cm] at (x axis mid) {\bl{a}s}; |
|
251 \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; |
|
252 |
|
253 %plots |
|
254 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
255 file {re-python.data}; |
|
256 \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] |
|
257 file {re-ruby.data}; |
|
258 |
|
259 %legend |
|
260 \begin{scope}[shift={(4,20)}] |
|
261 \draw[color=blue] (0,0) -- |
|
262 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
263 node[right]{\small Python}; |
|
264 \draw[yshift=-\baselineskip, color=brown] (0,0) -- |
|
265 plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
266 node[right]{\small Ruby}; |
|
267 \end{scope} |
|
268 \end{tikzpicture} |
|
269 |
|
270 \end{frame}} |
|
271 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
272 *} |
|
273 |
|
274 text_raw {* |
|
275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
276 \mode<presentation>{ |
|
277 \begin{frame}[t] |
|
278 \frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} |
|
279 |
|
280 \mbox{}\\[-13mm] |
|
281 |
|
282 \begin{tabular}{@ {\hspace{-5mm}}l} |
|
283 \begin{tikzpicture}[y=.2cm, x=.01cm] |
|
284 %axis |
|
285 \draw (0,0) -- coordinate (x axis mid) (1000,0); |
|
286 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
287 %ticks |
|
288 \foreach \x in {0,200,...,1000} |
|
289 \draw (\x,1pt) -- (\x,-3pt) |
|
290 node[anchor=north] {\x}; |
|
291 \foreach \y in {0,5,...,30} |
|
292 \draw (1pt,\y) -- (-3pt,\y) |
|
293 node[anchor=east] {\y}; |
|
294 %labels |
|
295 \node[below=0.6cm] at (x axis mid) {\bl{a}s}; |
|
296 \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; |
|
297 |
|
298 %plots |
|
299 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
300 file {re-python.data}; |
|
301 \draw[color=green] plot[mark=square*, mark options={fill=white} ] |
|
302 file {re2c.data}; |
|
303 \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] |
|
304 file {re-ruby.data}; |
|
305 |
|
306 %legend |
|
307 \begin{scope}[shift={(100,20)}] |
|
308 \draw[color=blue] (0,0) -- |
|
309 plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
310 node[right]{\small Python}; |
|
311 \draw[yshift=-13, color=brown] (0,0) -- |
|
312 plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
313 node[right]{\small Ruby}; |
|
314 \draw[yshift=13, color=green] (0,0) -- |
|
315 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
316 node[right]{\small nullable + der}; |
|
317 \end{scope} |
|
318 \end{tikzpicture} |
|
319 \end{tabular} |
|
320 |
|
321 \end{frame}} |
|
322 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
323 *} |
|
324 |
|
325 text_raw{* |
|
326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
327 \mode<presentation>{ |
|
328 \begin{frame}[t] |
|
329 \frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} |
|
330 |
|
331 \mbox{}\\[-9mm] |
|
332 |
|
333 \begin{tabular}{@ {\hspace{-5mm}}l} |
|
334 \begin{tikzpicture}[y=.2cm, x=.0008cm] |
|
335 %axis |
|
336 \draw (0,0) -- coordinate (x axis mid) (12000,0); |
|
337 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
338 %ticks |
|
339 \foreach \x in {0,2000,...,12000} |
|
340 \draw (\x,1pt) -- (\x,-3pt) |
|
341 node[anchor=north] {\x}; |
|
342 \foreach \y in {0,5,...,30} |
|
343 \draw (1pt,\y) -- (-3pt,\y) |
|
344 node[anchor=east] {\y}; |
|
345 %labels |
|
346 \node[below=0.6cm] at (x axis mid) {\bl{a}s}; |
|
347 \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; |
|
348 |
|
349 %plots |
|
350 \draw[color=green] plot[mark=square*, mark options={fill=white} ] |
|
351 file {re2b.data}; |
|
352 \draw[color=black] plot[mark=square*, mark options={fill=white} ] |
|
353 file {re3.data}; |
|
354 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
355 file {re-python.data}; |
|
356 \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] |
|
357 file {re-ruby.data}; |
|
358 |
|
359 %legend |
|
360 \begin{scope}[shift={(2000,20)}] |
|
361 \draw[color=blue] (0,0) -- |
|
362 plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
363 node[right]{\small Python}; |
|
364 \draw[yshift=-13, color=brown] (0,0) -- |
|
365 plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
366 node[right]{\small Ruby}; |
|
367 \draw[yshift=13, color=green] (0,0) -- |
|
368 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
369 node[right]{\small nullable + der}; |
|
370 \draw[yshift=26, color=black] (0,0) -- |
|
371 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) |
|
372 node[right]{\small nullable + der + simplification}; |
|
373 \end{scope} |
|
374 \end{tikzpicture} |
|
375 \end{tabular} |
|
376 |
|
377 \end{frame}} |
|
378 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
379 *} |
|
380 |
398 |
381 |
399 text_raw {* |
382 text_raw {* |
400 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
383 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
401 \mode<presentation>{ |
384 \mode<presentation>{ |
402 \begin{frame}[t] |
385 \begin{frame}[t] |
1145 |
1128 |
1146 \only<1->{% |
1129 \only<1->{% |
1147 \textcolor{blue}{% |
1130 \textcolor{blue}{% |
1148 \begin{center} |
1131 \begin{center} |
1149 \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}} |
1132 \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}} |
1150 der c $\varnothing$ & $\dn$ & $\varnothing$\\ |
1133 $der\,c\,\varnothing$ & $\dn$ & $\varnothing$\\ |
1151 der c [] & $\dn$ & $\varnothing$\\ |
1134 $der\,c\,[]$ & $\dn$ & $\varnothing$\\ |
1152 der c d & $\dn$ & if c $=$ d then [] else $\varnothing$\\ |
1135 $der\,c\,d$ & $\dn$ & if $c = d$ then $[]$ else $\varnothing$\\ |
1153 der c ($r_1 + r_2$) & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\ |
1136 $der\,c\,(r_1 + r_2)$ & $\dn$ & $der\,c\,r_1 + der\,c\,r_2$\\ |
1154 der c ($r^*$) & $\dn$ & (der c $r$) $\cdot$ ($r^*$)\\ |
1137 $der\,c\,(r^*)$ & $\dn$ & $(der\,c\,r) \cdot r^*$\\ |
1155 der c ($r_1 \cdot r_2$) & $\dn$ & ((der c $r_1$) $\cdot$ $r_2$) +\\ |
1138 $der\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\ |
1156 & & \hspace{-3mm}(if nullable $r_1$ then der c $r_2$ else $\varnothing$)\\ |
1139 & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ |
|
1140 & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\ |
1157 \end{tabular} |
1141 \end{tabular} |
1158 \end{center}}} |
1142 \end{center}}} |
1159 |
1143 |
1160 \only<2->{ |
1144 \only<2->{ |
1161 \begin{textblock}{13}(1.5,5.7) |
1145 \begin{textblock}{14.1}(1.5,5.7) |
1162 \begin{block}{} |
1146 \begin{block}{} |
1163 \begin{quote} |
1147 \begin{quote} |
1164 \begin{minipage}{13cm}\raggedright |
1148 \begin{minipage}{14.1cm}\raggedright\rm |
1165 derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip |
1149 derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip |
1166 \begin{center} |
1150 \begin{center} |
1167 \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(\text{ders}~x~r) = {\cal{L}}(\text{ders}~y~r) |
1151 \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(deriv~x~r) = {\cal{L}}(deriv~y~r) |
1168 \Longleftrightarrow x \approx_{{\cal{L}}(r)} y}} |
1152 \Longleftrightarrow x \approx_{{\cal{L}}(r)} y}} |
1169 \only<3>{\mbox{\hspace{-22mm}}\smath{\text{ders}~x~r = \text{ders}~y~r |
1153 \only<3>{\mbox{\hspace{-22mm}}\smath{deriv~x~r = deriv~y~r |
1170 \Longrightarrow x \approx_{{\cal{L}}(r)} y}} |
1154 \Longrightarrow x \approx_{{\cal{L}}(r)} y}} |
1171 \end{center}\bigskip |
1155 \end{center}\bigskip |
1172 \ |
1156 \ |
1173 \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI |
1157 \smath{\text{finite}(deriv~A~r)}, but only modulo ACI |
1174 |
1158 |
1175 \begin{center} |
1159 \begin{center} |
1176 \begin{tabular}{@ {\hspace{-10mm}}rcl} |
1160 \begin{tabular}{@ {\hspace{-10mm}}rcl} |
1177 \smath{(r_1 + r_2) + r_3} & \smath{\equiv} & \smath{r_1 + (r_2 + r_3)}\\ |
1161 \smath{(r_1 + r_2) + r_3} & \smath{\equiv} & \smath{r_1 + (r_2 + r_3)}\\ |
1178 \smath{r_1 + r_2} & \smath{\equiv} & \smath{r_2 + r_1}\\ |
1162 \smath{r_1 + r_2} & \smath{\equiv} & \smath{r_2 + r_1}\\ |
1308 |
1295 |
1309 \end{frame}} |
1296 \end{frame}} |
1310 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1311 *} |
1298 *} |
1312 |
1299 |
1313 text_raw {* |
|
1314 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1315 \mode<presentation>{ |
|
1316 \begin{frame}[c] |
|
1317 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
1318 |
|
1319 \begin{center} |
|
1320 \huge\bf\textcolor{gray}{in Nuprl} |
|
1321 \end{center} |
|
1322 |
|
1323 \begin{itemize} |
|
1324 \item Constable, Jackson, Naumov, Uribe\medskip |
|
1325 \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode) |
|
1326 \end{itemize} |
|
1327 |
|
1328 \end{frame}} |
|
1329 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1330 |
|
1331 *} |
|
1332 |
|
1333 text_raw {* |
|
1334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1335 \mode<presentation>{ |
|
1336 \begin{frame}[c] |
|
1337 \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} |
|
1338 |
|
1339 \begin{center} |
|
1340 \huge\bf\textcolor{gray}{in Coq} |
|
1341 \end{center} |
|
1342 |
|
1343 \begin{itemize} |
|
1344 \item Filli\^atre, Briais, Braibant and others |
|
1345 \item multi-year effort; a number of results in automata theory, e.g.\medskip |
|
1346 \begin{itemize} |
|
1347 \item Kleene's thm.~by Filli\^atre (\alert{``rather big''}) |
|
1348 \item automata theory by Briais (5400 loc) |
|
1349 \item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc) |
|
1350 \item Mirkin's partial derivative automaton construction (10600 loc) |
|
1351 \end{itemize} |
|
1352 \end{itemize} |
|
1353 |
|
1354 \end{frame}} |
|
1355 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1356 *} |
|
1357 |
|
1358 |
1300 |
1359 text_raw {* |
1301 text_raw {* |
1360 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1361 \mode<presentation>{ |
1303 \mode<presentation>{ |
1362 \begin{frame}[c] |
1304 \begin{frame}[c] |
1363 \frametitle{\LARGE Conclusion} |
1305 \frametitle{\LARGE Conclusion} |
1364 |
1306 |
1365 \begin{itemize} |
1307 \begin{itemize} |
1366 \item we have never seen a proof of Myhill-Nerode based on |
1308 \item we have never seen a proof of Myhill-Nerode based on |
1367 regular expressions only\smallskip\pause |
1309 regular expressions\smallskip\pause |
1368 |
1310 |
1369 \item great source of examples (inductions)\smallskip\pause |
1311 \item great source of examples (inductions)\smallskip\pause |
1370 |
1312 |
1371 \item no need to fight the theorem prover:\\ |
1313 \item no need to fight the theorem prover:\\ |
1372 \begin{itemize} |
1314 \begin{itemize} |
1373 \item first direction (790 loc)\\ |
1315 \item first direction (790 loc)\\ |
1374 \item second direction (400 / 390 loc) |
1316 \item second direction (400 / 390 loc) |
1375 \end{itemize} |
1317 \end{itemize} |
1376 |
1318 |
1377 \item I am not saying automata are bad; just formal proofs about |
1319 \item I am not saying automata are bad; just proofs about |
1378 them are quite dif$\!$ficult\pause\bigskip\medskip |
1320 them are quite difficult in theorem provers\bigskip |
1379 |
1321 |
|
1322 \item \small our journal paper has just been accepted in JAR (see webpage) |
|
1323 \end{itemize} |
|
1324 |
|
1325 \end{frame}} |
|
1326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1327 *} |
|
1328 |
|
1329 text_raw {* |
|
1330 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1331 \mode<presentation>{ |
|
1332 \begin{frame}[c] |
|
1333 \frametitle{\LARGE Future Work} |
|
1334 |
|
1335 \begin{itemize} |
|
1336 \item regular expression sub-matching with derivatives (Martin Sulzmann PPDP'12)\bigskip |
1380 \item parsing with derivatives of grammars\\ (Matt Might ICFP'11) |
1337 \item parsing with derivatives of grammars\\ (Matt Might ICFP'11) |
1381 \end{itemize} |
1338 \end{itemize} |
1382 |
1339 |
1383 \end{frame}} |
1340 \end{frame}} |
1384 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1341 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1385 *} |
1342 *} |
1386 |
1343 |
1387 text_raw {* |
1344 text_raw {* |
1388 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1345 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1389 \mode<presentation>{ |
1346 \mode<presentation>{ |
1390 \begin{frame}[c] |
|
1391 \frametitle{\LARGE An Apology} |
|
1392 |
|
1393 \begin{itemize} |
|
1394 \item This should all of course be done co-inductively |
|
1395 \end{itemize} |
|
1396 |
|
1397 \footnotesize |
|
1398 \begin{tabular}{@ {\hspace{4mm}}l} |
|
1399 From: Jasmin Christian Blanchette\\ |
|
1400 To: isabelle-dev@mailbroy.informatik.tu-muenchen.de\\ |
|
1401 Subject: [isabelle-dev] NEWS\\ |
|
1402 Date: \alert{\bf Tue, 28 Aug 2012} 17:40:55 +0200\\ |
|
1403 \\ |
|
1404 * {\bf HOL/Codatatype}: New (co)datatype package with support for mixed,\\ |
|
1405 nested recursion and interesting non-free datatypes.\\ |
|
1406 \\ |
|
1407 * HOL/Ordinals\_and\_Cardinals: Theories of ordinals and cardinals\\ |
|
1408 (supersedes the AFP entry of the same name).\\[2mm] |
|
1409 Kudos to Andrei and Dmitriy!\\ |
|
1410 \\ |
|
1411 Jasmin\\[-1mm] |
|
1412 ------------------------------------\\ |
|
1413 isabelle-dev mailing list\\ |
|
1414 isabelle-dev@in.tum.de\\ |
|
1415 \end{tabular} |
|
1416 |
|
1417 \end{frame}} |
|
1418 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1419 *} |
|
1420 |
|
1421 |
|
1422 text_raw {* |
|
1423 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1424 \mode<presentation>{ |
|
1425 \begin{frame}[b] |
1347 \begin{frame}[b] |
1426 \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}} |
1348 \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much\\ for listening!\\[5mm]Questions?}} |
1427 |
1349 |
1428 \end{frame}} |
1350 \end{frame}} |
1429 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1351 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1430 *} |
1352 *} |
1431 |
1353 |