| 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 | |
|---|
| 555 | Deliverable D2.1 has been fully revised taking into account your valuable remarks. |
|---|
| 556 | In particular: |
|---|
| 557 | |
|---|
| 558 | \begin{itemize} |
|---|
| 559 | |
|---|
| 560 | \item Appendix~C highlights |
|---|
| 561 | the optimisations performed by the prototype $\C$ compiler |
|---|
| 562 | which 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 |
|---|
| 573 | of related work on worst-case execution time and its relevance to our approach. |
|---|
| 574 | |
|---|
| 575 | \end{itemize} |
|---|
| 576 | |
|---|
| 577 | Two master students (Kayvan Memarian and Ronan Saillard) have worked |
|---|
| 578 | at the formalisation of the proposed proof methodologies in a proof |
|---|
| 579 | assistant ({\sc Coq}) during their internships. The choice of the |
|---|
| 580 | {\sc Coq} proof assistant was natural since the students and one of |
|---|
| 581 | the main authors of the deliverable were already trained to work with this tool. The results |
|---|
| 582 | of these experiments were instructive, and promising in the case of |
|---|
| 583 | the labelling approach. We stress that this formalisation effort is |
|---|
| 584 | an unplanned contribution of deliverable D2.1 which has been possible |
|---|
| 585 | thanks to the work of these two students. This also explains |
|---|
| 586 | why some proofs are still missing in the development. |
|---|
| 587 | |
|---|
| 588 | |
|---|
| 589 | Finally, appendix~G provides an assessment |
|---|
| 590 | of the deliverable {\em with hindsight} and it discusses in particular |
|---|
| 591 | the impact of the program size limitations of the $\intel$ processor |
|---|
| 592 | on deliverable D5.3. |
|---|
| 593 | |
|---|
| 594 | |
|---|
| 595 | |
|---|
| 596 | \vspace*{\fill} |
|---|
| 597 | \noindent |
|---|
| 598 | Project Acronym: \cerco{}\\ |
|---|
| 599 | Project full title: Certified Complexity\\ |
|---|
| 600 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
|---|
| 601 | |
|---|
| 602 | \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} |
|---|
| 603 | |
|---|
| 604 | \end{document} |
|---|
