source: Deliverables/D1.1/Presentations/WP2-roberto.tex @ 656

Last change on this file since 656 was 656, checked in by amadio, 9 years ago

rob updated

File size: 37.1 KB
RevLine 
[626]1
2
3
4
5
6\documentclass{beamer}
7
8\usetheme{Frankfurt}
9%\logo{\includegraphics[height=1.0cm]{fetopen.png}}
10% smaller
11\logo{\includegraphics[height=0.6cm]{fetopen.png}}
12
13
14\usepackage[english]{babel}
15\usepackage{inputenc}
16
17
18
19                           
20%\documentclass[landscape]{seminar}
21
22% \usepackage[latin1]{inputenc}
23% \usepackage[frenchb]{babel}
24
25
26%TO HAVE AN ARTICLE STYLE
27%\documentclass[11pt]{article}
28%\usepackage{latexsym}
29%\usepackage{amsfonts}
30%\usepackage{a4wide}
31
32
33
34% TO HAVE COLOURS IN SLIDES, USAGE \Blu{}, \Red{}, \Green{}, \Purple{}
35\usepackage{epsfig}
36\usepackage{color}
37\usepackage{fancybox}
38\usepackage{color}
39\usepackage{alltt}
40\definecolor{c1114}{rgb}{1,0.2156862745098,0.75294117647059}
41\definecolor{c1112}{rgb}{1,0,0}
42\definecolor{c1121}{rgb}{0,0,0.54509803921569}
43\definecolor{c1123}{rgb}{0,0.5,0}
44\def\Green#1{\textcolor{c1123}{#1}}
45\def\Blu#1{\textcolor{c1121}{#1}}
46\def\Red#1{\textcolor{c1112}{#1}}
47\def\Purple#1{\textcolor{c1114}{#1}}
48\definecolor{c1082}{rgb}{0.,0.,0.}
49\definecolor{c1083}{rgb}{1,0,0}
50
51% TO NEUTRALIZE COLOURS
52%\newcommand{\Red}[1]{#1}
53%\newcommand{\Blu}[1]{#1}
54%\newcommand{\Green}[1]{#1}
55%\newcommand{\Purple}[1]{#1}
56
57%TO NEUTRALIZE SLIDE
58% replace {slide} by {slid} and insert
59%\newenvironment{slid}{}{}
60
61% ALSO REMOVE \newpage
62
63
64\newcommand{\eqdef}{=_{\text{def}}} 
65\newcommand{\concat}{\cdot}%%{\mathbin{+}}
66
67\newcommand{\Models}{\mid \! =}              % models
68\newcommand{\Int}{\mathit{int}} 
69\newcommand{\nat}{\mathit{nat}} 
70\newcommand{\String}{\mathit{string}} 
71\newcommand{\Ident}{\mathit{ident}} 
72\newcommand{\Block}{\mathit{block}} 
73\newcommand{\Signature}{\mathit{signature}} 
74 
75\newcommand{\pc}{\mathit{pc}} 
76\newcommand{\estack}{\mathit{estack}} 
77\newcommand{\Error}{\epsilon} 
78 
79%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
80%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81 
82% --------------------------------------------------------------------- %
83% Proof rule.                                                           %
84% --------------------------------------------------------------------- %
85 
86\newcommand{\staterule}[3]{%
87  $\begin{array}{@{}l}%
88   \mbox{#1}\\%
89   \begin{array}{c}
90   #2\\ 
91   \hline 
92   \raisebox{0ex}[2.5ex]{\strut}#3%
93   \end{array}
94  \end{array}$} 
95 
96\newcommand{\GAP}{2ex} 
97 
98\newcommand{\recall}[2]{%
99 $\begin{array}{c}
100 #1\\ 
101 \hline 
102 \raisebox{0ex}[2.5ex]{\strut}#2%
103 \end{array}$} 
104 
105\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
106\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
107\newcommand{\ratio}{.3} 
108 
109\newenvironment{display}[1]{\begin{tabbing} 
110  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
111  \noindent\hbra\\[-.5em] 
112  {\ }\textsc{#1}\\[-.8ex] 
113  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
114  }{\\[-.8ex]\hket 
115  \end{tabbing}} 
116 
117 
118\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
119\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
120\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
121    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
122 
123\newcommand{\entry}[2]{\>$#1$\>\>#2} 
124\newcommand{\clause}[2]{$#1$\>\>#2} 
125\newcommand{\category}[2]{\clause{#1::=}{#2}} 
126\newcommand{\subclause}[1]{\>\>\>#1} 
127\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
128 
129%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
130%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
131 
132% environments
133 
134%% \newtheorem{theorem}{Theorem}
135%% \newtheorem{fact}[theorem]{Fact}
136%% \newtheorem{definition}[theorem]{Definition}
137%% \newtheorem{lemma}[theorem]{Lemma}
138%% \newtheorem{corollary}[theorem]{Corollary}
139%% \newtheorem{proposition}[theorem]{Proposition}
140%% \newtheorem{example}[theorem]{Example}
141%% \newtheorem{exercise}[theorem]{Exercise}
142%% \newtheorem{remark}[theorem]{Remark}
143%% \newtheorem{proviso}[theorem]{Proviso}
144%%  \newtheorem{conjecture}[theorem]{Conjecture}
145
146% proofs 
147 
148%\newcommand{\Proof}{\noindent {\sc Proof}. }
149\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
150%\newcommand{\qed}{\hfill${\Box}$}
151\newcommand{\EndProof}{\qed}
152 
153% figure environment
154 
155\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures
156\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
157                                                        %environment for figures
158%       ************Macros for mathematical symbols*************
159% Style
160 
161\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
162\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
163\newcommand{\ra}{\rangle} 
164 
165\newcommand{\lf}{\lfloor} 
166\newcommand{\rf}{\rfloor} 
167\newcommand{\ul}[1]{\underline{#1}}     % to underline
168\newcommand{\ol}[1]{\overline{#1}}      % to overline
169\newcommand{\ok}{~ok}                   % well formed context
170 
171% Syntax
172 
173\newcommand{\Gives}{\vdash}             % in a type judgment
174\newcommand{\emptycxt}{\O}              % empty context
175\newcommand{\subs}[2]{[#1 / #2]} 
176\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]   
177\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
178
179\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list.
180 
181\newcommand{\impl}{\supset} 
182%\newcommand{\imp}{{\sc Imp}}            %imp language
183%\newcommand{\vm}{{\sc Vm}}              %virtual machine language
184\newcommand{\arrow}{\rightarrow}        % right thin arrow
185\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
186\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
187\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
188\newcommand{\pr}{\parallel}             % parallel ||
189\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
190\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
191\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
192\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
193\newcommand{\Alt}{ \mid\!\!\mid  } 
194\newcommand{\isum}{\oplus} 
195\newcommand{\dpar}{\mid\!\mid} 
196                                        % for the production of a grammar containing \mid
197\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
198                                        % to make a centered inference rule
199 
200% (Meta-)Logic
201 
202\newcommand{\bool}{{\sf bool}}          % boolean values
203\newcommand{\Or}{\vee}                  % disjunction
204\newcommand{\OR}{\bigvee}               % big disjunction
205\newcommand{\AND}{\wedge}               % conjunction
206\newcommand{\ANDD}{\bigwedge}           % big conjunction
207\newcommand{\Arrow}{\Rightarrow}        % right double arrow
208\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
209\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
210 
211% Semantics
212 
213\newcommand{\dl}{[\![}                  % semantic [[
214\newcommand{\dr}{]\!]}                  % semantic ]]
215\newcommand{\lam}{{\bf \lambda}}        % semantic lambda
216
217
218% The equivalences for this paper
219
220% the usual ones
221\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
222\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
223
224% the contextual conv sensitive
225\newcommand{\cbis}{\approx}        % convergence sensitive bis
226\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
227
228% the labelled conv sensitive
229\newcommand{\lcbis}{\approx^{\ell}} %
230\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
231\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
232
233
234
235
236\newcommand{\maytest}{=_{\Downarrow}}
237\newcommand{\musttest}{=_{\Downarrow_{S}}}
238
239
240 
241 
242% Sets
243 
244\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
245\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
246\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
247\newcommand{\union}{\cup}               % union
248\newcommand{\inter}{\cap}               % intersection
249\newcommand{\Union}{\bigcup}            % big union
250\newcommand{\Inter}{\bigcap}            % big intersection
251\newcommand{\cpl}[1]{#1^{c}}            % complement
252\newcommand{\card}{\sharp}              % cardinality
253\newcommand{\minus}{\backslash}         % set difference
254\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
255\newcommand{\comp}{\circ}               % functional composition
256\newcommand{\set}[1]{\{#1\}}            % set enumeration
257\newcommand{\pset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
258 
259% Domains
260 
261\newcommand{\two}{{\bf O}}              % Sierpinski space
262\newcommand{\join}{\vee}                % join
263\newcommand{\JOIN}{\bigvee}             % big join 
264\newcommand{\meet}{\wedge}              % meet
265\newcommand{\MEET}{\bigwedge}           % big meet
266\newcommand{\dcl}{\downarrow}           % down closure
267\newcommand{\ucl}{\uparrow}             % up closure
268\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
269%\newcommand{\diver}{\uparrow}           % diverging term
270\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
271\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
272\newcommand{\CConv}{\Downarrow_{C}}
273\newcommand{\diver}{\Uparrow}           % diverging map
274\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
275\newcommand{\ret}{\triangleleft}        % retract
276\newcommand{\nor}{\succeq}
277\newcommand{\prj}{\underline{\ret}}     % projection
278\newcommand{\parrow}{\rightharpoonup}   % partial function space
279\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
280\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
281\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
282%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
283\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
284\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
285                                        %extra space
286\newcommand{\per}[1]{\;#1 \;} 
287\newcommand{\wddagger}{\natural}  % weak suspension
288%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
289% Categories
290 
291\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
292 
293%               *******  Notation for the $\pi$-calculus *********
294% Syntax:
295 
296 
297\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
298\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
299\newcommand{\names}[1]{{\it n}(#1)}                     % names
300\newcommand{\true}{{\sf t}}                             % true
301\newcommand{\false}{{\sf f}}                            % false
302\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
303\newcommand{\pioo}{\pi_{1}^{r}} 
304\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
305\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
306\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
307\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
308\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
309\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
310\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
311\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
312\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
313\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
314\newcommand{\nil}{{\sf nil}} 
315\newcommand{\cons}{{\sf cons}} 
316\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
317\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
318\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
319\newcommand{\mand}{\mbox{ and }} 
320\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
321\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
322\newcommand{\w}[1]{{\it #1}}    %To write in math style
323\newcommand{\vcb}[1]{{\bf #1}} 
324\newcommand{\lc}{\langle\!|} 
325\newcommand{\rc}{|\!\rangle} 
326\newcommand{\obj}[1]{{\it obj}(#1)} 
327\newcommand{\move}[1]{{\sf move}(#1)} 
328\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
329\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
330\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
331\newcommand{\dpt}{\,:\,} 
332\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
333\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
334\newcommand{\vc}[1]{{\bf #1}} 
335\newcommand{\lnorm}{\lbrack\!\lbrack} 
336\newcommand{\rnorm}{\rbrack\!\rbrack} 
337\newcommand{\sem}[1]{\underline{#1}} 
338\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
339\newcommand{\lcro}{\langle\!|} 
340\newcommand{\rcro}{|\!\rangle} 
341\newcommand{\semi}[1]{\lcro #1\rcro} 
342\newcommand{\sell}{\,\ell\,} 
343\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
344 
345\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
346\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
347\newcommand{\welse}[1]{{\sf else}~#1} 
348
349%Pour la fleche double, il faut rajouter :
350%      \usepackage{mathtools}
351
352\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled actionlow %high
353
354%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
355
356%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
357
358%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
359
360%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
361                                %%%high
362
363\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
364                                %%%high
365
366
367%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
368\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
369
370%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
371\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
372
373
374 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
375\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
376\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
377
378
379\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high
380\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
381 
382\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}} 
383\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
384 
385 
386 
387\newcommand{\eval}{\Downarrow} 
388\newcommand{\Eval}[1]{\Downarrow^{#1}} 
389 
390 
391\newcommand{\Z}{{\bf Z}} 
392\newcommand{\Real}{\mathbb{R}^{+}} 
393\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
394\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
395\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
396\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
397\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
398\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
399\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
400\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
401\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
402\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
403\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
404\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
405\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
406\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
407 
408\newcommand{\hatt}[1]{#1^{+}} 
409\newcommand{\Of}{\mathbin{\w{of}}} 
410 
411\newcommand{\susp}{\downarrow} 
412\newcommand{\lsusp}{\Downarrow_L} 
413\newcommand{\wsusp}{\Downarrow} 
414\newcommand{\commits}{\searrow} 
415 
416 
417\newcommand{\spi}{S\pi} 
418 
419
420 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
421% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
422\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
423
424
425\newcommand{\tick}{{\sf tick}}          %tick action
426
427 
428 
429\newcommand{\sbis}{\equiv_L} 
430\newcommand{\emit}[2]{\ol{#1}#2} 
431%\newcommand{\present}[4]{#1(#2).#3,#4}
432\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
433
434\newcommand{\matchv}[4]{[#1 > #2]#3,#4}
435
436\newcommand{\new}[2]{\nu #1 \ #2} 
437\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
438\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
439 
440
441
442\newcommand{\tit}[1]{\begin{center} \Red{{\bf #1 }}\end{center}}
443\newcommand{\stit}[1]{\begin{center} #1 \end{center}}
444\newcommand{\chpt}[1]{\begin{center} \Red{{\huge #1 }}\end{center}}
445\newcommand{\bem}[1]{\Blu{{\em #1}}}
446\newcommand{\NB}{{\bf NB}~}
447\newcommand{\Refer}[1]{\Green{{\small {\bf Ref} \ #1}}}
448
449\newcommand{\tact}[2]{\ensuremath{\underset{#1}{\act{~#2~}}}}
450\newcommand{\tacteq}[2]{\ensuremath{\underset{#1}{\acteq{~#2~}}}}
451\newcommand{\twbis}{\approx^{t}}        % typed weak bis
452
453\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
454\newcommand{\thread}[1]{{\sf thread} \ #1}
455\newcommand{\store}[2]{(#1 \Leftarrow #2)}
456\newcommand{\gt}[1]{{\sf get}(#1)}
457\newcommand{\st}[2]{{\sf set}(#1,#2)}
458\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
459
460\newcommand{\Beh}{{\bf B}}
461\newcommand{\Ter}{{\bf 1}}
462
463\newcommand{\imp}{{\sf Imp}}            %imp language
464\newcommand{\vm}{{\sf Vm}}              %virtual machine language
465\newcommand{\mips}{{\sf Mips}}          %Mips language
466\newcommand{\eighty}{{\sf 8051}}
467\newcommand{\asm}{{\sf ASM}}
468\newcommand{\C}{{\sf C}}                % C language
469\newcommand{\gcc}{{\sf gcc}}            %gcc
470\newcommand{\Clight}{{\sf Clight}}        %C light language
471\newcommand{\Cminor}{{\sf Cminor}}
472\newcommand{\RTLAbs}{{\sf RTLAbs}}
473\newcommand{\RTL}{{\sf RTL}}
474\newcommand{\ERTL}{{\sf ERTL}}
475\newcommand{\LTL}{{\sf LTL}}
476\newcommand{\LIN}{{\sf LIN}}
477\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
478\newcommand{\ocaml}{{\sf ocaml}}
479\newcommand{\coq}{{\sf Coq}}
480\newcommand{\compcert}{{\sf CompCert}}
481\newcommand{\cerco}{{\sf CerCo}}
482\newcommand{\cil}{{\sf CIL}}
483\newcommand{\scade}{{\sf Scade}}
484\newcommand{\absint}{{\sf AbsInt}}
485\newcommand{\framac}{{\sf Frama-C}}
486\newcommand{\powerpc}{{\sf PowerPc}}
487\newcommand{\lustre}{{\sf Lustre}}
488\newcommand{\esterel}{{\sf Esterel}}
489\newcommand{\ml}{{\sf ML}}
490%\newcommand{\ocaml}{{\sf OCAML}}
491
492
493
494\author{Roberto M. Amadio}
495\institute{Universit\'e Paris Diderot}
496
[633]497\title{$\cerco$ Work Package 2: Untrusted Compiler Prototype (part 1)}
[626]498\date{March 11, 2011}
499
500\begin{document}
501
502\begin{frame}
503\maketitle
504\end{frame}
505
506
507
508
509\begin{frame}
510
511\frametitle{Goal and schedule of WP2}
512Implement a {\bf proof-of-concept prototype} of the cost annotating compiler.
513
514\begin{description}
515
516\item[Task 2.1] Architectural design ($\Arrow$ D2.1)
517
518\item[Task 2.2] Intermediate languages and data structures ($\Arrow$ D2.1)
519
520\item[Task 2.3] Implementation ($\Arrow$ D2.2)
521
522\item[Task 2.4] Integration validation and testing (terminates at T0+18, no deliverable)
523\end{description}
524
525\begin{description}
526
527\item[D2.1] Compiler design and Intermediate languages (T0+6).
528
529\item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12).
530
531\end{description}
[633]532{\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
[626]533second part will give more details on Task 2.2, discuss Task 2.3 (with demo),
534and  provide some perspectives on Task 2.4 and WP5.}
535
536\end{frame}
537
538
539\begin{frame}
540
[633]541\frametitle{People involved at UPD site}
[626]542
543
[633]544{\small
[626]545\begin{tabular}{|c|c|c|}
546
547\hline
548{\bf Name}           &{\bf Status} &{\bf Rough Allocated Time} \\\hline
[633]549Roberto \textsc{Amadio} &Professor &1 day/week \\
550Yann \textsc{R\'egis-Gianas} &Assistant Professor &1 day/week \\
551Nicolas \textsc{Ayache}      &Post-doc      &full time, 11 months \\
552Ronan \textsc{Saillard}      &Internship+PhD &full time, 8 months \\
553Kayvan \textsc{Memarian}     &Internship   &1.5 days/week, 4 months \\ \hline
554\end{tabular}}
[626]555
[633]556
557~\\~\\
558\Red{{\bf NB}} Internships are very important: dissemination, speed up development,
559explore side paths, preliminary training towards research (PhD),$\ldots$
560
[626]561\end{frame}
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576\begin{frame}
577
578\frametitle{Motivation}
579Resource analysis of programming models should, if we are serious about it,
580eventually have an impact on programming practice. Limiting factors include:
581
582\begin{itemize}
583
584\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
585
586\item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs.
587
588\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
589
590\end{itemize}
591
592\end{frame}
593
594
595\begin{frame}
596
[633]597\frametitle{$\cerco$ goals and approach}
[626]598
599\begin{itemize}
600
601\item Bound and certify the {\bf number of cycles} that it takes to run a
602given  piece of code on a given processor with a given compiler.
603
[633]604\item Target {\bf $\C$ programs}, and in particular the kind of $\C$ 
[626]605programs produced for embedded applications
[633]606(such as those generated by the $\scade$ compiler).
[626]607
608\item {\bf Reflect the cost information} obtained at the machine level
[633]609back into the $\C$ source code.
[626]610
611\item {\bf Extract synthetic bounds} by reasoning on
[633]612the annotated $\C$  programs (for which several general purpose tools now exist).
[626]613
614\end{itemize}
615
[633]616\Red{\NB} Technically, this can be seen as a refinement of ongoing work on {\bf compiler certification}   
617(see, e.g., $\compcert$ project).
[626]618
619\end{frame}
620
621
622
623\begin{frame}
624
625\frametitle{Current technology and our challenge}
626\begin{itemize}
627
628
629\item Compilation phases are heavily {\bf inspected and tested} 
630but not formally checked with a proof assistant.
631\[
[633]632\lustre \arrow \C \arrow \textsc{binary~ code}
[626]633\]
634\item Binary code must be {\bf annotated} with (uncertified)
635information on the number of iterations of loops.
636
637\item Tools such as \textsc{AbsInt} perform WCET analysis of
638{\bf sequences of instructions of binary code}.
639
640\end{itemize}
641
[633]642\noindent \Red{{\bf Our challenge}}
643Lift in a {\em certified way} whathever information we have on the execution
644cost of the binary code to an information on the $\C$ source code (a kind
[626]645of {\bf decompilation}).
646
647\end{frame}
648
649
650
651\begin{frame}
652
653\frametitle{A potential connection}
654Could use this work as a {\bf platform} to experiment with
[633]655\Blu{{\em implicit complexity programming languages}}.
[626]656
657{\small
658\begin{enumerate}
659
[633]660\item Write a program in your preferred implicit complexity programming language.
661\item Compile it to $\C$.
662\item $\cerco$ compiles $\C$ to machine code and provides precise and certified information on execution time of $\C$ code.
[626]663\item Use your implicit complexity analysis to produce automatically a synthetic bound on the resources used by the program.
[633]664\item If you want to push this further, try to lift the assertions about the $\C$ code to assertions on your source program.
[626]665\end{enumerate}}
[656]666\Red{\NB} Might be another case study for WP5.
[626]667\end{frame}
668
669
670
671
672\begin{frame}
673
674\frametitle{Is this really possible?}
675
676\begin{itemize}
677
678\item 
679What are the  annotations, and how are we going to actually
680prove that they are correct? \\
681$\Arrow$ We need a {\bf proof methodology}.~\\~\\
682
683\item 
684Is it possible to produce annotations of the source code
685that predict soundly and precisely the execution cost?\\
686$\Arrow$ We need to {\bf show that the approach scales}.
687
688\end{itemize}
689
690\end{frame}
691
692
693
694
695\begin{frame}
696
697\frametitle{Preliminary ideas}
698
699\begin{itemize}
700
701\item 
702A cost annotation is an {\bf instrumentation} of the source program
703that keeps track of the execution cost of the program.
704
705\item 
706The computed cost should be {\bf correct} and possibly {\bf precise} 
707relatively to the compiled code.
708
709\item 
710Starting from the annotated source program apply standard tools
[633]711to reason about $\C$ programs in order to {\bf extract synthetic bounds}.
[626]712
713\end{itemize}
714
715\end{frame}
716
717
718
719
720\begin{frame}
721
722\frametitle{A small size case study (direct approach 1/3)}
723
724{\footnotesize
725\[
726\begin{array}{ccccc}
727
728      &\cl{C}   &                          &\cl{C'}              \\
729
730\imp   &\arrow        &\vm                &\arrow       &\mips        \\
731
732\ \quad\downarrow \w{An}_{\imp}
733&
734&\ \quad\downarrow \w{An}_{\vm}
735&
736&\ \quad\downarrow \w{An}_{\mips} \\
737
738\imp   &             &\vm             & &\mips        \\
739
740\end{array}
741\]}
742\begin{itemize}
743
744\item $\imp$: an imperative language with while loops.
745
746\item $\vm$: a virtual machine with a stack.
747
748\item $\mips$: an assembly like language with registers and RAM memory.
749
750\item $\cl{C}$: relies on the stack to evaluate numerical expressions.
751
752\item $\cl{C'}$: statically allocates the base of the stack in the registers and the
753rest in RAM memory. This requires a `stack height' analysis of the $\vm$ code.
754
755\item $\w{An}_{\mips}$: counts the number of $\mips$ instructions executed.
756
757\end{itemize}
758
759\end{frame}
760
761
762\begin{frame}
763\frametitle{A small size case study (direct approach 2/3)}
764{\footnotesize
765\[
766\begin{array}{ccccc}
767
768      &\cl{C}   &                          &\cl{C'}              \\
769
770\imp   &\arrow        &\vm                &\arrow       &\mips        \\
771
772\ \quad\downarrow \w{An}_{\imp}
773&
774&\ \quad\downarrow \w{An}_{\vm}
775&
776&\ \quad\downarrow \w{An}_{\mips} \\
777
778\imp   &             &\vm             & &\mips        \\
779
780\end{array}
781\]}
782
783\begin{itemize}
784
785
786\item The annotation functions instrument the
787code so that it {\bf monitors its execution cost} by incrementing
788a (fresh) \w{cost} variable.
789
790\item In particular, the annotation function of the object code
791$\w{An}_{\mips}$ is a  {\bf compelling definition} of the execution cost.
792
793\end{itemize}
794\end{frame}
795
796
797\begin{frame}
798
799\frametitle{A small size case study (direct approach 3/3)}
800
801{\footnotesize
802\[
803\begin{array}{ccccc}
804
805      &\cl{C}   &                          &\cl{C'}              \\
806
807\imp   &\arrow        &\vm                &\arrow       &\mips        \\
808
809\ \quad\downarrow \w{An}_{\imp}
810&
811&\ \quad\downarrow \w{An}_{\vm}
812&
813&\ \quad\downarrow \w{An}_{\mips} \\
814
815\imp   &             &\vm             & &\mips        \\
816
817\end{array}
818\]}
819
820\begin{itemize}
821\item The annotation function at step $i$ is {\bf correct} with
822respect to the one at step $i+1$ of the compilation
823if
824
825{\small
826\[
[633]827\begin{array}{lc}
828\mbox{`Predicted' cost} &(\w{An}_{i}(S),s[0/\w{cost}])\eval s'[c/\w{cost}]\\\hline
829\mbox{`Real' cost}       &(\w{An}_{i+1}(\cl{C}_{i,i+1}(S)),s[0/\w{cost}]) \eval s'[d/\w{cost}] \quad d \leq c
830\end{array}
[626]831\]}
832
833\item Further it is {\bf precise} if \ $c\leq d+\kappa(S)$.
834
835\end{itemize}
836
837\end{frame}
838
839\begin{frame}
840
841\frametitle{Problems with the direct approach}
842K. \textsc{Memarian} formalized this in \textsc{Coq} 
843(500 lines of specification and 2400 lines of proofs).
844
845\begin{itemize}
846
847\item Proofs have to manipulate {\bf numerical values}.
848
849\item Proofs about the bounds are {\bf intertwined} 
850with those of functional correctness and get much larger
851(factor $7$ in the experiment).
852
853\item To be precise we need to explicit a lot of {\bf contextual information}
854which is at odd with proof compositionality.
855
856\end{itemize}
857
858\end{frame}
859
860
861\begin{frame}
862
863\frametitle{Second attempt: labelling approach (1/7)}
864{\footnotesize
865\[
866\begin{array}{ccccc}
867
868
869\imp      &                              &                          &                & \\
870
871\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
872
873\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
874
875\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
876&
877&\ \quad\downarrow \w{er}_{\vm}
878&
879&\ \quad\downarrow \w{er}_{\mips} \\ 
880
881\imp   &\arrow             &\vm             &\arrow &\mips        \\
882      &\cl{C}   &                          &\cl{C'}              \\
883\end{array}
884\]}
885
886\begin{description}
887
888\item[Labelled languages] All languages are enriched with \bem{labelled instructions} generating \bem{labelled transitions}.
889
890\item[Erasures] The \bem{erasure functions} are just functions that remove all labelling instructions.
891
892\end{description}
893
894\end{frame}
895
896
897
898\begin{frame}
899
900\frametitle{Labelling approach  (2/7)}
901{\footnotesize
902\[
903\begin{array}{ccccc}
904
905
906\imp      &                              &                          &                & \\
907
908\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
909
910\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
911
912\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
913&
914&\ \quad\downarrow \w{er}_{\vm}
915&
916&\ \quad\downarrow \w{er}_{\mips} \\ 
917
918\imp   &\arrow             &\vm             &\arrow &\mips        \\
919      &\cl{C}   &                          &\cl{C'}              \\
920\end{array}
921\]}
922
923\begin{description}
924
925
926
927\item[Extended compilation] The compilation functions are \bem{extended} to the labelled languages.
928
929\item[Commutation] Compilation and erasure functions \bem{commute}:
930\[
931\w{er}_{\vm} \comp \cl{C} = \cl{C} \comp \w{er}_{\imp} \qquad
932\w{er}_{\mips} \comp \cl{C'} = \cl{C'} \comp \w{er}_{\vm}
933\]
934
935\end{description}
936\end{frame}
937
938
939
940\begin{frame}
941
942\frametitle{Labelling approach (3/7)}
943{\footnotesize
944\[
945\begin{array}{ccccc}
946
947
948\imp      &                              &                          &                & \\
949
950\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
951
952\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
953
954\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
955&
956&\ \quad\downarrow \w{er}_{\vm}
957&
958&\ \quad\downarrow \w{er}_{\mips} \\ 
959
960\imp   &\arrow             &\vm             &\arrow &\mips        \\
961      &\cl{C}   &                          &\cl{C'}              \\
962\end{array}
963\]}
964
965{\small
966\begin{description}
967
968\item[Labelling] A \bem{labelling} of the source language is just a function $\cl{L}$ such that $\w{er}_{\imp}\comp \cl{L}=\w{id}_{\imp}$.
969
970\item[Instrumentation]
971Given a \bem{`cost function'} associating costs to labels,
972an \bem{instrumentation} of the source language is a
973function $\cl{I}_{\imp}$  replacing  labels with suitable increments
974of a fresh \bem{cost variable}.
975
976\item[Annotation]
977 An \bem{annotation} of the source language is defined as:
978\[
979\w{An}_{\imp} = \cl{I}_{\imp}\comp \cl{L}~.
980\]
981
982\end{description}}
983
984\end{frame}
985
986\begin{frame}
987
988\frametitle{Labelling approach (4/7)}
989{\footnotesize
990\[
991\begin{array}{ccccc}
992
993
994\imp      &                              &                          &                & \\
995
996\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
997
998\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
999
1000\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1001&
1002&\ \quad\downarrow \w{er}_{\vm}
1003&
1004&\ \quad\downarrow \w{er}_{\mips} \\ 
1005
1006\imp   &\arrow             &\vm             &\arrow &\mips        \\
1007      &\cl{C}   &                          &\cl{C'}              \\
1008\end{array}
1009\]}
1010
[633]1011\begin{description}
[626]1012
[633]1013\item[Simulation]
1014The simulation properties of the compilation functions are {\em lifted} to the labelled languages.
1015%With a proper design of the labelled languages this just means taking into account the rules that
1016%generate labelled transitions. 
1017Let $\lambda$ denote a sequence of labels. Then:% we have:
1018\end{description}
[626]1019\[
1020(S,s)\eval (s',\lambda)  \quad \Arrow \quad 
1021(\cl{C}(S),s) \eval (s',\lambda) \quad \Arrow \quad
1022(\cl{C'}(\cl{C}(S)),s) \eval (s',\lambda)
1023\]
1024
1025\end{frame}
1026
1027
1028\begin{frame}
1029
1030
1031\frametitle{Labelling approach (5/7)}
1032{\footnotesize
1033\[
1034\begin{array}{ccccc}
1035
1036
1037\imp      &                              &                          &                & \\
1038
1039\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1040
1041\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1042
1043\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1044&
1045&\ \quad\downarrow \w{er}_{\vm}
1046&
1047&\ \quad\downarrow \w{er}_{\mips} \\ 
1048
1049\imp   &\arrow             &\vm             &\arrow &\mips        \\
1050      &\cl{C}   &                          &\cl{C'}             
1051\end{array}
1052\]}
1053
[633]1054\begin{description}
1055
1056\item[Numerical vs. Symbolic cost] By {\bf diagram chasing} we derive:
[626]1057\[
1058\infer{(\w{An}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]}
[633]1059{(\cl{C'}(\cl{C}(\cl{L}(S))),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)}
[626]1060\]
[633]1061where $\delta$ is the numerical (additive) cost associated with $\lambda$.
[626]1062
[633]1063\end{description}
1064
[626]1065\end{frame}
1066
1067
1068
1069\begin{frame}
1070
1071\frametitle{Labelling approach (6/7)}
1072{\footnotesize
1073\[
1074\begin{array}{ccccc}
1075
1076
1077\imp      &                              &                          &                & \\
1078
1079\quad\uparrow {\cal I}_{\imp}      &\cl{C}   &        &\cl{C'}         &     \\
1080
1081\imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\
1082
1083\quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
1084&
1085&\ \quad\downarrow \w{er}_{\vm}
1086&
1087&\ \quad\downarrow \w{er}_{\mips} \\ 
1088
1089\imp   &\arrow             &\vm             &\arrow &\mips        \\
1090      &\cl{C}   &                          &\cl{C'}              \\
1091\end{array}
1092\]}
1093
[633]1094\begin{description}
1095
1096\item[When is the labelling $\cl{L}$ interesting?]
1097I.e., knowing that
[626]1098\[
1099\cl{C'}(\cl{C}(S)) = \w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(S)))
1100\]
[633]1101{\bf under which conditions} can we conclude that $\lambda$, {\em i.e.},
1102$\delta$, is a sound and  possibly precise description of the real execution cost?
1103\end{description}
[626]1104\end{frame}
1105
1106
1107\begin{frame}
1108
1109\frametitle{Labelling approach (7/7)}
[633]1110Conditions to be checked on the labelled binary code.
[626]1111
1112{\small
1113\begin{itemize}
1114
1115\item Assume a sound over-approximation of
1116the {\bf control flow} of the labelled object code
1117$(\cl{C'}(\cl{C}(L(S))$.
1118This is a directed, rooted graph where some nodes are labelled.
1119
1120\item The labelling is {\bf sound} if in the CFG
1121all nodes are reachable from a labelled node and
1122all loops go through a labelled node.
1123
1124\item In this case, the {\bf cost of a label} $\ell$ is the cost
1125of the most expensive path in the control flow graph starting
1126from a node labelled $\ell$
1127and, crossing unlabelled nodes, arriving at a labelled one
1128or an unlabelled one without
1129successors (call such paths {\bf simple}).
1130
1131\item A sound labelling is {\bf precise} if for all labels $\ell$ the
1132paths of the kind
1133described above starting from a node labelled $\ell$ have the same cost.
1134
1135
1136\end{itemize}}
1137
1138\end{frame}
1139
1140\begin{frame}
1141
1142\frametitle{Advantages of the labelling approach}
1143
1144\begin{itemize}
1145
1146\item  Costs are handled {\bf symbolically} 
1147as labels are propagated by the compiler.
1148
1149\item  Proofs of {\bf functional correctness stay simple} 
1150(just one additional case to cover the labels)
1151
1152\item  {\bf No need to explicit the contextual information}.
1153The numerical cost is computed only at the assembly language level
1154and then it is reflected back to the source.
1155
1156\end{itemize}
1157
1158\end{frame}
1159
1160
1161\begin{frame}
1162
[633]1163\frametitle{A larger experiment: a $\C$ to $\mips$ compiler}
[626]1164{\footnotesize
1165\[
1166\begin{array}{cccccccccc}
1167&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
1168                                              &&&&&&&&\downarrow \\
1169 \mips &\leftarrow &\LIN &\leftarrow  &\LTL &\leftarrow  &\ERTL  &\leftarrow &\RTL &\qquad \mbox{(back-end)}
1170\end{array}
1171\]
1172}
1173
1174{\small
1175\begin{itemize}
1176
1177\item Moderate optimisations: register allocation, dead-code elimination,$\ldots$ (a bit more efficient than {\tt gcc0}).
1178
1179\item Roughly, we implement the labelling approach on top of a compiler quite
[633]1180close to $\compcert$.
[626]1181
1182\item Around 10K lines of $\ocaml$ code. No proofs, just code inspection and test. We used the software  in a master level compilation course.
1183
1184\end{itemize}}
1185
1186\end{frame}
1187
1188
1189\begin{frame}
1190
1191\frametitle{Observed soundness and precision for the $C$ compiler}
1192As a rule of thumb,  we lose {\bf soundness} if we miss loops in the generated  code.
1193We lose {\bf precision} if we miss branching in the generated code.
1194
1195\begin{itemize}
1196
1197\item The first situation never arises in the considered compilation chain.
1198
[633]1199\item The second situation can be handled by some pre-processing of the $\C$ code
[626]1200(e.g., logical \bem{and} compiled as a conditional expression).
1201
1202\end{itemize}
1203
1204\end{frame}
1205
1206
1207
1208\begin{frame}
1209
1210\frametitle{What comes next}
1211This work was completed in the first 7 months of the project.
[633]1212The following 5 months have been spent:
[626]1213
1214
1215\begin{itemize}
[633]1216\item Enhancing and debugging the compiler.
[626]1217
1218\item Extending the formal proofs on the toy compiler.
1219
[633]1220\item Porting the compiler from $\mips$  to $\eighty$ (and teaching this).
[626]1221
[633]1222\item Integrating the {\sc Ocaml/Matita} description of $\eighty$.
[626]1223
1224\end{itemize}
1225
[633]1226This is covered  in the second part of the talk.
[626]1227
1228\end{frame}
1229
1230\end{document}
1231
1232
Note: See TracBrowser for help on using the repository browser.