source: Deliverables/D5.1/report.tex @ 1659

Last change on this file since 1659 was 1659, checked in by amadio, 8 years ago
File size: 22.8 KB
Line 
1
2\documentclass[11pt,epsf,a4wide]{article}
3\usepackage{../style/cerco}
4\usepackage{pdfpages}
5
6\usepackage{graphics}
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 \\
556D5.1 Untrusted CerCo Prototype \\
557and \\
558D5.3 Case study: analysis of synchronous code
559\\
560\end{LARGE} 
561\end{center}
562
563\vspace*{2cm}
564\begin{center}
565\begin{large}
566Version 1.0
567\end{large}
568\end{center}
569
570\vspace*{0.5cm}
571\begin{center}
572\begin{large}
573Main Authors:\\
574Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas,
575\end{large}
576\end{center}
577
578\vspace*{\fill}
579\noindent
580Project Acronym: \cerco{}\\
581Project full title: Certified Complexity\\
582Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
583
584\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
585
586\newpage
587
588
589\vspace*{7cm}
590
591\paragraph{Summary}
592The main aim of WP5 is to develop proof of concept prototypes where
593the (untrusted) compiler developed in WP2 is interfaced with existing tools
594in order to synthesize complexity  assertions on the execution
595time of programs. Eventually, the approach should be adapted to
596the trusted compiler developed in WP3 and WP4 (cf. deliverable D5.2 at
597month 36).
598
599In particular, the main planned contribution of deliverable D5.1 is a
600tool that takes as input an annotated C program produced by the CerCo
601compiler and tries to synthesize a certified bound on the execution
602time of the program.  The related expected contribution of deliverable
603D5.3 amounts to apply the developed tool to the C programs generated
604by a Lustre compiler.  This planned work is described in the first
605document...which accompanies a software distribution...
606Frama-C plug-in ...more examples...
607
608We pause to recall a redistribution of the workforce of the UDP site.
609Following the resignation of the doctoral student at the end of year
6101, the contract of the post-doc has been as extended till month ??  It
611follows that in the UPD site there has been a shift of manpower from
612the third to the second year. Because of this shift we decided to
613anticipate the presentation of deliverable D5.3 at month 24 rather
614than month 36.
615
616During the second year some unplanned work related to deliverables
617D5.1 and D5.3 has taken place at UPD.
618
619The main development concerns the extension of the CerCo labelling
620approach to a standard compilation chain from a higher-order
621functional language of the ML family to C and the development of
622framework to reason about the cost annotations. This work shows...the
623generality of the approach...  Parallel the work done for C...
624Ongoing work tries to produce valid garbage collection statements by
625typing...
626
627A second development is of a more speculative nature and
628concerned with the development of a type system
629for a functional langauge with side effects that guarantees a complexity
630bound... First work to account for side effects... Ongoing work tries to
631extend the framework to polynomial time. Eventually we hope to join
632the thread on implicit complexity???
633
634
635
636\newpage
637
638\includepdf[pages={-}]{plugin.pdf}
639
640
641\newpage
642
643\includepdf[pages={-}]{fopara.pdf}
644
645
646\newpage
647
648\includepdf[pages={-}]{tlca.pdf}
649
650
651\end{document}
Note: See TracBrowser for help on using the repository browser.