source: Deliverables/D2.1/Revision/report.tex @ 2732

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

Deliverable D2.1 with addendum

File size: 20.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{
537INFORMATION AND COMMUNICATION TECHNOLOGIES\\
538(ICT)\\
539PROGRAMME\\
540\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
541
542\date{ }
543\author{}
544
545\begin{document}
546\thispagestyle{empty}
547
548\vspace*{-1cm}
549\begin{center}
550\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
551\end{center}
552
553\begin{minipage}{\textwidth}
554\maketitle
555\end{minipage}
556
557
558\vspace*{0.5cm}
559\begin{center}
560\begin{LARGE}
561\bf
562Report n. D2.1\\
563Compiler design and intermediate languages\\
564\end{LARGE} 
565\end{center}
566
567\vspace*{2cm}
568\begin{center}
569\begin{large}
570Version 1.0 with Addendum
571\end{large}
572\end{center}
573
574\vspace*{0.5cm}
575\begin{center}
576\begin{large}
577Main Authors:\\
578Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas
579\end{large}
580\end{center}
581
582\vspace*{\fill}
583\noindent
584Project Acronym: \cerco{}\\
585Project full title: Certified Complexity\\
586Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
587
588\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
589
590\newpage
591
592
593\vspace*{7cm}
594\paragraph{Abstract}
595\input{abstract}
596
597\newpage
598
599{\footnotesize \tableofcontents}
600
601\newpage
602
603\input{text-report}
604
605\end{document}
Note: See TracBrowser for help on using the repository browser.