source: Deliverables/D2.1/Revision/letter.tex @ 792

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

Deliverable D2.1 with addendum

File size: 21.7 KB
Line 
1
2\documentclass[11pt,epsf,a4wide]{article}
3\usepackage{../../style/cerco}
4
5
6% For SLNCS comment above and use
7% \documentclass{llncs}
8
9
10
11
12
13\RequirePackage[latin1]{inputenc}     
14 
15% Mettre les différents packages et fonctions que l'on utilise
16\usepackage[english]{babel} 
17\usepackage{amsmath} 
18\usepackage{amsfonts} 
19%\usepackage{amssymb}
20\usepackage{xspace} 
21\usepackage{latexsym} 
22\usepackage{url} 
23\usepackage{xspace} 
24%\usepackage{fancyvrb}
25\usepackage[all]{xy} 
26%packages pour LNCS
27%\usepackage{semantic}
28%\usepackage{cmll}
29% Packages for RR
30\usepackage{graphics,color}             
31\RequirePackage[latin1]{inputenc}   
32\usepackage{array}
33 
34%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
35%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36 
37\newenvironment{comment}{{\bf MORE WORK:}} 
38 
39\newenvironment{restate-proposition}[2][{}]{\noindent\textbf{Proposition~{#2}}\;\textbf{#1}\  
40}{\vskip 1em} 
41 
42\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{#1}\  
43}{\vskip 1em} 
44 
45\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}\;\textbf{#1}\  
46}{\vskip 1em} 
47 
48\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 
49 
50\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 
51\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 
52\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 
53\newcommand{\Proofitemf}[1]{\noindent $#1\;$} 
54\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 
55\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 
56\newcommand{\Defitemf}[1]{\noindent $#1\;$} 
57 
58 
59%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
60%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61 
62 
63 
64%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
66 
67\newcommand{\eqdef}{=_{\text{def}}} 
68\newcommand{\concat}{\cdot}%%{\mathbin{+}}
69\newcommand{\Int}{\mathit{int}} 
70\newcommand{\nat}{\mathit{nat}} 
71\newcommand{\String}{\mathit{string}} 
72\newcommand{\Ident}{\mathit{ident}} 
73\newcommand{\Block}{\mathit{block}} 
74\newcommand{\Signature}{\mathit{signature}} 
75 
76\newcommand{\pc}{\mathit{pc}} 
77\newcommand{\estack}{\mathit{estack}} 
78\newcommand{\Error}{\epsilon} 
79 
80%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
82 
83% --------------------------------------------------------------------- %
84% Proof rule.                                                           %
85% --------------------------------------------------------------------- %
86 
87\newcommand{\staterule}[3]{%
88  $\begin{array}{@{}l}%
89   \mbox{#1}\\%
90   \begin{array}{c}
91   #2\\ 
92   \hline 
93   \raisebox{0ex}[2.5ex]{\strut}#3%
94   \end{array}
95  \end{array}$} 
96 
97\newcommand{\GAP}{2ex} 
98 
99\newcommand{\recall}[2]{%
100 $\begin{array}{c}
101 #1\\ 
102 \hline 
103 \raisebox{0ex}[2.5ex]{\strut}#2%
104 \end{array}$} 
105 
106\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
107\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
108\newcommand{\ratio}{.3} 
109 
110\newenvironment{display}[1]{\begin{tabbing} 
111  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
112  \noindent\hbra\\[-.5em] 
113  {\ }\textsc{#1}\\[-.8ex] 
114  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
115  }{\\[-.8ex]\hket 
116  \end{tabbing}} 
117 
118 
119\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
120\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
121\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height
122    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
123 
124\newcommand{\entry}[2]{\>$#1$\>\>#2} 
125\newcommand{\clause}[2]{$#1$\>\>#2} 
126\newcommand{\category}[2]{\clause{#1::=}{#2}} 
127\newcommand{\subclause}[1]{\>\>\>#1} 
128\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
129 
130%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
131%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
132 
133% environments
134
135% To be commented for LNCS
136  \newtheorem{theorem}{Theorem} 
137  \newtheorem{fact}[theorem]{Fact} 
138  \newtheorem{definition}[theorem]{Definition} 
139  \newtheorem{lemma}[theorem]{Lemma} 
140  \newtheorem{corollary}[theorem]{Corollary} 
141  \newtheorem{proposition}[theorem]{Proposition} 
142  \newtheorem{example}[theorem]{Example} 
143  \newtheorem{exercise}[theorem]{Exercise} 
144  \newtheorem{remark}[theorem]{Remark} 
145  \newtheorem{question}[theorem]{Question}
146  \newtheorem{proviso}[theorem]{Proviso} 
147   \newtheorem{conjecture}[theorem]{Conjecture}
148
149% proofs 
150 
151\newcommand{\Proof}{\noindent {\sc Proof}. } 
152\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
153% To be commented for LNCS
154 \newcommand{\qed}{\hfill${\Box}$} 
155\newcommand{\EndProof}{\qed}
156 
157% figure environment
158 
159\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures
160\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
161                                                        %environment for figures
162%       ************Macros for mathematical symbols*************
163% Style
164 
165\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic
166\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair)
167\newcommand{\ra}{\rangle} 
168 
169\newcommand{\lf}{\lfloor} 
170\newcommand{\rf}{\rfloor} 
171\newcommand{\ul}[1]{\underline{#1}}     % to underline
172\newcommand{\ol}[1]{\overline{#1}}      % to overline
173\newcommand{\ok}{~ok}                   % well formed context
174 
175% Syntax
176 
177\newcommand{\Gives}{\vdash}             % in a type judgment
178\newcommand{\IGives}{\vdash_{I}}        % intuitionistic provability
179\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
180\newcommand{\CGives}{\vdash_{C}}        % affine-intuitionistic confluent provability
181
182
183\newcommand{\Models}{\mid \! =}              % models
184
185\newcommand{\emptycxt}{\On}              % empty context
186\newcommand{\subs}[2]{[#1 / #2]} 
187\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]   
188\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U}
189
190\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list.
191 
192\newcommand{\impl}{\supset} 
193\newcommand{\arrow}{\rightarrow}        % right thin arrow
194\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure
195%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}}   % linear
196                                % implication
197\newcommand{\limp}{\multimap} %linear implication
198\newcommand{\bang}{\, !} 
199% LNCS
200%\newcommand{\bang}{\oc}
201\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
202\newcommand{\hyp}[3]{#1:(#2, #3)}
203\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3}    % modal let
204\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3}    % simple let
205\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3}    % paragraph let
206\newcommand{\tertype}{{\bf 1}}
207\newcommand{\behtype}{{\bf B}}
208\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree
209\newcommand{\cxt}[1]{#1[~]}             % Context with one hole
210\newcommand{\pr}{\parallel}             % parallel ||
211\newcommand{\Nat}{\mathbf{N}}                 % natural numbers
212\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity
213\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals
214\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity
215\newcommand{\Alt}{ \mid\!\!\mid  } 
216\newcommand{\isum}{\oplus} 
217\newcommand{\csum}{\uplus}              %context sum
218\newcommand{\dpar}{\mid\!\mid} 
219                                        % for the production of a grammar containing \mid
220\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
221                                        % to make a centered inference rule
222 
223% (Meta-)Logic
224 
225\newcommand{\bool}{{\sf bool}}          % boolean values
226\newcommand{\Or}{\vee}                  % disjunction
227\newcommand{\OR}{\bigvee}               % big disjunction
228\newcommand{\AND}{\wedge}               % conjunction
229\newcommand{\ANDD}{\bigwedge}           % big conjunction
230\newcommand{\Arrow}{\Rightarrow}        % right double arrow
231\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces
232\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence
233 
234% Semantics
235 
236\newcommand{\dl}{[\![}                  % semantic [[
237\newcommand{\dr}{]\!]}                  % semantic ]]
238\newcommand{\lam}{{\bf \lambda}}        % semantic lambda
239
240
241% The equivalences for this paper
242
243% the usual ones
244\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
245\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS
246
247% the contextual conv sensitive
248\newcommand{\cbis}{\approx}        % convergence sensitive bis
249\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS
250
251% the labelled conv sensitive
252\newcommand{\lcbis}{\approx^{\ell}} %
253\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
254\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %
255
256
257
258
259
260
261
262\newcommand{\maytest}{=_{\Downarrow}}
263\newcommand{\musttest}{=_{\Downarrow_{S}}}
264
265
266 
267 
268% Sets
269 
270\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set
271\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts
272\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts
273\newcommand{\union}{\cup}               % union
274\newcommand{\inter}{\cap}               % intersection
275\newcommand{\Union}{\bigcup}            % big union
276\newcommand{\Inter}{\bigcap}            % big intersection
277\newcommand{\cpl}[1]{#1^{c}}            % complement
278\newcommand{\card}{\sharp}              % cardinality
279\newcommand{\minus}{\backslash}         % set difference
280\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega}
281\newcommand{\comp}{\circ}               % functional composition
282%\newcommand{\oset}[1]{\{#1\}}            % set enumeration
283\newcommand{\mset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |}
284 
285% Domains
286 
287\newcommand{\two}{{\bf O}}              % Sierpinski space
288\newcommand{\join}{\vee}                % join
289\newcommand{\JOIN}{\bigvee}             % big join 
290\newcommand{\meet}{\wedge}              % meet
291\newcommand{\MEET}{\bigwedge}           % big meet
292\newcommand{\dcl}{\downarrow}           % down closure
293\newcommand{\ucl}{\uparrow}             % up closure
294\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix)
295\newcommand{\diver}{\uparrow}           % diverging term
296\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix)
297\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix)
298\newcommand{\CConv}{\Downarrow_{C}}
299\newcommand{\Diver}{\Uparrow}           % diverging map
300\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D}
301\newcommand{\ret}{\triangleleft}        % retract
302\newcommand{\nor}{\succeq}
303\newcommand{\prj}{\underline{\ret}}     % projection
304\newcommand{\parrow}{\rightharpoonup}   % partial function space
305\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds
306\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds
307\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting
308\newcommand{\forget}[1]{\underline{#1}} % forgetful translation
309
310%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic)
311\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation
312\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no
313                                        %extra space
314\newcommand{\per}[1]{\;#1 \;} 
315\newcommand{\wddagger}{\natural}  % weak suspension
316%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension
317% Categories
318 
319\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >.
320 
321%               *******  Notation for the $\pi$-calculus *********
322% Syntax:
323 
324 
325\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names
326\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names
327\newcommand{\names}[1]{{\it n}(#1)}                     % names
328\newcommand{\true}{{\sf t}}                             % true
329\newcommand{\false}{{\sf f}}                            % false
330\newcommand{\pio}{\pi_1}                                % 1 receptor calculus
331\newcommand{\pioo}{\pi_{1}^{r}} 
332\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match
333\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus
334\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus
335\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus
336\newcommand{\sort}[1]{{\it st}(#1)}                     % sort
337\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort
338\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else
339\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs
340\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
341\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists
342\newcommand{\nil}{{\sf nil}} 
343\newcommand{\cons}{{\sf cons}} 
344\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process
345\newcommand{\conf}[1]{\{ #1 \}}                         %configuration
346\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b
347\newcommand{\mand}{\mbox{ and }} 
348\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector
349\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure
350\newcommand{\w}[1]{{\it #1}}    %To write in math style
351\newcommand{\vcb}[1]{{\bf #1}} 
352\newcommand{\lc}{\langle\!|} 
353\newcommand{\rc}{|\!\rangle} 
354\newcommand{\obj}[1]{{\it obj}(#1)} 
355\newcommand{\move}[1]{{\sf move}(#1)} 
356\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
357\newcommand{\qtype}[4]{\forall #1 :  #2 . (#4,#3)} 
358\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
359\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
360\newcommand{\dpt}{\,:\,} 
361\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
362\newcommand{\s}[1]{{\sf #1}}    % sans-serif 
363\newcommand{\vc}[1]{{\bf #1}} 
364\newcommand{\lnorm}{\lbrack\!\lbrack} 
365\newcommand{\rnorm}{\rbrack\!\rbrack} 
366\newcommand{\sem}[1]{\underline{#1}} 
367\newcommand{\tra}[1]{\langle #1 \rangle}
368\newcommand{\trb}[1]{[ #1 ]}
369\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
370\newcommand{\lcro}{\langle\!|} 
371\newcommand{\rcro}{|\!\rangle} 
372\newcommand{\semi}[1]{\lcro #1\rcro} 
373\newcommand{\sell}{\,\ell\,} 
374\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
375 
376\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3} 
377\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~} 
378\newcommand{\welse}[1]{{\sf else}~#1} 
379
380%Pour la fleche double, il faut rajouter :
381%      \usepackage{mathtools}
382
383\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high
384
385\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}
386
387\newcommand{\set}[1]{\{#1\}}
388\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
389\newcommand{\st}[2]{{\sf set}(#1,#2)}
390\newcommand{\wrt}[2]{{\sf w}(#1,#2)}
391
392\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
393\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}
394
395\newcommand{\get}[1]{{\sf get}(#1)}
396
397%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high
398
399%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high
400
401%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high
402
403%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
404                                %%%high
405
406\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
407                                %%%high
408
409
410%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
411\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}
412
413%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
414\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}
415
416
417 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high
418\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
419\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high
420
421
422\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high
423\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high
424 
425%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}}
426\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
427 
428 
429 
430\newcommand{\eval}{\Downarrow} 
431\newcommand{\Eval}[1]{\Downarrow^{#1}} 
432 
433 
434\newcommand{\Z}{{\bf Z}} 
435\newcommand{\Real}{\mathbb{R}^{+}} 
436\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
437\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
438\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
439\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
440\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
441\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
442\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
443\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
444\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
445\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
446\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
447\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
448\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
449\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
450 
451\newcommand{\hatt}[1]{#1^{+}} 
452\newcommand{\Of}{\mathbin{\w{of}}} 
453 
454\newcommand{\susp}{\downarrow} 
455\newcommand{\lsusp}{\Downarrow_L} 
456\newcommand{\wsusp}{\Downarrow} 
457\newcommand{\commits}{\searrow} 
458 
459 
460\newcommand{\spi}{S\pi} 
461 
462
463 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
464% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
465\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}
466
467
468\newcommand{\tick}{{\sf tick}}          %tick action
469
470 
471 
472\newcommand{\sbis}{\equiv_L} 
473\newcommand{\emit}[2]{\ol{#1}#2} 
474%\newcommand{\present}[4]{#1(#2).#3,#4}
475\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality
476
477\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}
478
479\newcommand{\new}[2]{\nu #1 \ #2} 
480\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
481\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation
482
483\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
484\newcommand{\thread}[1]{{\sf thread} \ #1}
485\newcommand{\store}[2]{(#1 \leftarrow #2)}
486\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}
487
488\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
489\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
490\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}
491
492\newcommand{\upair}[2]{[#1,#2]}
493\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}
494
495\newcommand{\vlt}[1]{{\cal V}(#1)}
496\newcommand{\prs}[1]{{\cal P}(#1)}
497
498\newcommand{\imp}{{\sf Imp}}            %imp language
499\newcommand{\vm}{{\sf Vm}}              %virtual machine language
500\newcommand{\mips}{{\sf Mips}}          %Mips language
501\newcommand{\intel}{{\sf 8051}}         % Intel 8051 language
502\newcommand{\C}{{\sf C}}                % C language
503\newcommand{\Clight}{{\sf Clight}}        %C light language
504\newcommand{\Cminor}{{\sf Cminor}}
505\newcommand{\RTLAbs}{{\sf RTLAbs}}
506\newcommand{\RTL}{{\sf RTL}}
507\newcommand{\ERTL}{{\sf ERTL}}
508\newcommand{\LTL}{{\sf LTL}}
509\newcommand{\LIN}{{\sf LIN}}
510\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
511\newcommand{\ocaml}{{\sf ocaml}}
512\newcommand{\coq}{{\sf Coq}}
513\newcommand{\compcert}{{\sf CompCert}}
514%\newcommand{\cerco}{{\sf CerCo}}
515\newcommand{\cil}{{\sf CIL}}
516\newcommand{\scade}{{\sf Scade}}
517\newcommand{\absint}{{\sf AbsInt}}
518\newcommand{\framac}{{\sf Frama-C}}
519\newcommand{\powerpc}{{\sf PowerPc}}
520\newcommand{\lustre}{{\sf Lustre}}
521\newcommand{\esterel}{{\sf Esterel}}
522\newcommand{\ml}{{\sf ML}}
523
524
525\newcommand{\codeex}[1]{\texttt{#1}}   % code example
526
527
528%%%%%%%%%%%%%%%%%%%%%%%%%%%
529
530
531
532
533
534\bibliographystyle{abbrv} 
535
536\title{Letter to the reviewers commenting the addendum to deliverable D2.1}
537
538
539\date{\today}
540\author{Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas}
541
542\begin{document}
543\thispagestyle{empty}
544
545\vspace*{-1cm}
546\begin{center}
547\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
548\end{center}
549
550\begin{minipage}{\textwidth}
551\maketitle
552\end{minipage}
553
554
555Deliverable D2.1 has been fully revised taking into account your valuable remarks.
556In particular:
557
558\begin{itemize}
559
560\item Appendix~C highlights 
561the optimisations performed by the prototype $\C$ compiler
562which are essentially of two types:
563\begin{enumerate}
564
565\item A standard liveness analysis and register allocation at the level of the
566$\ERTL$ language.
567
568\item A graph compression at the $\LIN$ level.
569
570\end{enumerate}
571
572\item Appendix~E includes an informal discussion
573of related work on worst-case execution time and its relevance to our approach.
574
575\end{itemize}
576
577Two master students (Kayvan Memarian and Ronan Saillard) have worked
578at the formalisation of the proposed proof methodologies in a proof
579assistant ({\sc Coq}) during their internships.  The choice of the
580{\sc Coq} proof assistant was natural since the students and one of
581the main authors of the deliverable were already trained to work with this tool.  The results
582of these experiments were instructive, and promising in the case of
583the labelling approach.  We stress that this formalisation effort is
584an unplanned contribution of deliverable D2.1 which has been possible
585thanks to the work of these two students. This also explains
586why some proofs are still missing in the development.
587
588
589Finally, appendix~G provides an assessment
590of the deliverable {\em with hindsight} and it discusses in particular
591the impact of the program size limitations of the $\intel$ processor
592on deliverable D5.3.
593
594
595
596\vspace*{\fill}
597\noindent
598Project Acronym: \cerco{}\\
599Project full title: Certified Complexity\\
600Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
601
602\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
603
604\end{document}
Note: See TracBrowser for help on using the repository browser.