source: Deliverables/D2.1/report.tex @ 1462

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

er-cor

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