source: Deliverables/D5.1-5.3/report.tex @ 3285

\documentclass[11pt,epsf,a4wide]{article}
\usepackage{../style/cerco}
\usepackage{pdfpages}

\usepackage{graphics}

% For SLNCS comment above and use
% \documentclass{llncs} 





\RequirePackage[latin1]{inputenc}     
 
% Mettre les différents packages et fonctions que l'on utilise 
\usepackage[english]{babel} 
\usepackage{amsmath} 
\usepackage{amsfonts} 
\usepackage{amssymb} 
\usepackage{xspace} 
\usepackage{latexsym} 
\usepackage{url} 
\usepackage{xspace} 
%\usepackage{fancyvrb} 
\usepackage[all]{xy} 
%packages pour LNCS
%\usepackage{semantic}
%\usepackage{cmll}
% Packages for RR 
\usepackage{graphics,color}              
\RequirePackage[latin1]{inputenc}   
\usepackage{array}
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
\newenvironment{comment}{{\bf MORE WORK:}} 
 
\newenvironment{restate-proposition}[2][{}]{\noindent\textbf{Proposition~{#2}}\;\textbf{#1}\  
}{\vskip 1em} 
 
\newenvironment{restate-theorem}[2][{}]{\noindent\textbf{Theorem~{#2}}\;\textbf{#1}\  
}{\vskip 1em} 
 
\newenvironment{restate-corollary}[2][{}]{\noindent\textbf{Corollary~{#2}}\;\textbf{#1}\  
}{\vskip 1em} 
 
\newcommand{\myparagraph}[1]{\medskip\noindent\textbf{#1}} 
 
\newcommand{\Proofitemb}[1]{\medskip \noindent {\bf #1\;}} 
\newcommand{\Proofitemfb}[1]{\noindent {\bf #1\;}} 
\newcommand{\Proofitem}[1]{\medskip \noindent $#1\;$} 
\newcommand{\Proofitemf}[1]{\noindent $#1\;$} 
\newcommand{\Defitem}[1]{\smallskip \noindent $#1\;$} 
\newcommand{\Defitemt}[1]{\smallskip \noindent {\em #1\;}} 
\newcommand{\Defitemf}[1]{\noindent $#1\;$} 
 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
\newcommand{\eqdef}{=_{\text{def}}} 
\newcommand{\concat}{\cdot}%%{\mathbin{+}} 
\newcommand{\Int}{\mathit{int}} 
\newcommand{\nat}{\mathit{nat}} 
\newcommand{\String}{\mathit{string}} 
\newcommand{\Ident}{\mathit{ident}} 
\newcommand{\Block}{\mathit{block}} 
\newcommand{\Signature}{\mathit{signature}} 
 
\newcommand{\pc}{\mathit{pc}} 
\newcommand{\estack}{\mathit{estack}} 
\newcommand{\Error}{\epsilon} 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
% --------------------------------------------------------------------- % 
% Proof rule.                                                           % 
% --------------------------------------------------------------------- % 
 
\newcommand{\staterule}[3]{% 
  $\begin{array}{@{}l}% 
   \mbox{#1}\\% 
   \begin{array}{c} 
   #2\\  
   \hline 
   \raisebox{0ex}[2.5ex]{\strut}#3% 
   \end{array} 
  \end{array}$} 
 
\newcommand{\GAP}{2ex} 
 
\newcommand{\recall}[2]{% 
 $\begin{array}{c} 
 #1\\  
 \hline 
 \raisebox{0ex}[2.5ex]{\strut}#2% 
 \end{array}$} 
 
\newcommand{\hbra}{\noindent\hbox to \textwidth{\leaders\hrule height1.8mm depth-1.5mm\hfill}} 
\newcommand{\hket}{\noindent\hbox to \textwidth{\leaders\hrule height0.3mm\hfill}} 
\newcommand{\ratio}{.3} 
 
\newenvironment{display}[1]{\begin{tabbing} 
  \hspace{1.5em} \= \hspace{\ratio\linewidth-1.5em} \= \hspace{1.5em} \= \kill 
  \noindent\hbra\\[-.5em] 
  {\ }\textsc{#1}\\[-.8ex] 
  \hbox to \textwidth{\leaders\hrule height1.6mm depth-1.5mm\hfill}\\[-.8ex] 
  }{\\[-.8ex]\hket 
  \end{tabbing}} 
 
 
\newcommand{\sbline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.2ex}\hfill\hspace*{0ex}}} 
\newcommand{\sline}{\hfill\smash[t]{\rule[1.5em]{\textwidth}{0.1ex}\hfill\hspace*{0ex}}} 
\newcommand{\sentry}[2]{\>$#1$\>\ \smash[t]{\vrule width 0.2mm height 
    1.2\baselineskip depth 1.5\baselineskip}\>#2} 
 
\newcommand{\entry}[2]{\>$#1$\>\>#2} 
\newcommand{\clause}[2]{$#1$\>\>#2} 
\newcommand{\category}[2]{\clause{#1::=}{#2}} 
\newcommand{\subclause}[1]{\>\>\>#1} 
\newcommand{\redrule}[3]{$#1$\>\>$#2$\>\>\>#3} 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
% environments 

% To be commented for LNCS 
 \newtheorem{theorem}{Theorem} 
 \newtheorem{fact}[theorem]{Fact} 
 \newtheorem{definition}[theorem]{Definition} 
 \newtheorem{lemma}[theorem]{Lemma} 
 \newtheorem{corollary}[theorem]{Corollary} 
 \newtheorem{proposition}[theorem]{Proposition} 
 \newtheorem{example}[theorem]{Example} 
 \newtheorem{exercise}[theorem]{Exercise} 
 \newtheorem{remark}[theorem]{Remark} 
 \newtheorem{question}[theorem]{Question}
 \newtheorem{proviso}[theorem]{Proviso} 
  \newtheorem{conjecture}[theorem]{Conjecture}

% proofs  
 
\newcommand{\Proof}{\noindent {\sc Proof}. } 
\newcommand{\Proofhint}{\noindent {\sc Proof hint}. } 
% To be commented for LNCS
 \newcommand{\qed}{\hfill${\Box}$} 
\newcommand{\EndProof}{\qed}
 
% figure environment 
 
\newcommand{\Figbar}{{\center \rule{\hsize}{0.3mm}}}    %horizontal thiner line for figures 
\newenvironment{figureplr}{\begin{figure}[t] \Figbar}{\Figbar \end{figure}} 
                                                        %environment for figures 
%       ************Macros for mathematical symbols************* 
% Style 
 
\newcommand{\cl}[1]{{\cal #1}}          % \cl{R} to make R calligraphic 
\newcommand{\la}{\langle}               % the brackets for pairing (see also \pair) 
\newcommand{\ra}{\rangle} 
 
\newcommand{\lf}{\lfloor} 
\newcommand{\rf}{\rfloor} 
\newcommand{\ul}[1]{\underline{#1}}     % to underline 
\newcommand{\ol}[1]{\overline{#1}}      % to overline 
\newcommand{\ok}{~ok}                   % well formed context 
 
% Syntax 
 
\newcommand{\Gives}{\vdash}             % in a type judgment 
\newcommand{\IGives}{\vdash_{I}}        % intuitionistic provability
\newcommand{\AIGives}{\vdash_{{\it AI}}} %affine-intuitionistic provability
\newcommand{\CGives}{\vdash_{C}}        % affine-intuitionistic confluent provability


\newcommand{\Models}{\mid \! =}              % models

\newcommand{\emptycxt}{\On}              % empty context 
\newcommand{\subs}[2]{[#1 / #2]} 
\newcommand{\sub}[2]{[#2 / #1]}         % substitution \sub{x}{U} gives [U/x]    
\newcommand{\Sub}[3]{[#3 / #2]#1}       % Substitution with three arguments \Sub{V}{x}{U} 

\newcommand{\lsub}[2]{#2 / #1}          % substitution \lsub{x}{U} gives U/x, to be used in a list. 
 
\newcommand{\impl}{\supset} 
\newcommand{\arrow}{\rightarrow}        % right thin arrow 
\newcommand{\trarrow}{\stackrel{*}{\rightarrow}}        % trans closure 
%\newcommand{\limp}{\makebox[5mm]{\,$- \! {\circ}\,$}}   % linear
                                % implication
\newcommand{\limp}{\multimap} %linear implication
\newcommand{\bang}{\, !} 
% LNCS
%\newcommand{\bang}{\oc} 
\newcommand{\limpe}[1]{\stackrel{#1}{\multimap}}
\newcommand{\hyp}[3]{#1:(#2, #3)}
\newcommand{\letm}[3]{{\sf let} \ ! #1 = #2 \ {\sf in} \ #3}    % modal let
\newcommand{\lets}[3]{{\sf let} \ #1 = #2 \ {\sf in} \ #3}    % simple let
\newcommand{\letp}[3]{{\sf let} \ \S #1 = #2 \ {\sf in} \ #3}    % paragraph let
\newcommand{\tertype}{{\bf 1}}
\newcommand{\behtype}{{\bf B}}
\newcommand{\bt}[1]{{\it BT}(#1)}       % Boehm tree 
\newcommand{\cxt}[1]{#1[~]}             % Context with one hole 
\newcommand{\pr}{\parallel}             % parallel || 
\newcommand{\Nat}{\mathbf{N}}                 % natural numbers 
\newcommand{\Natmax}{\mathbf{N}_{{\it max}}}  % natural numbers with minus infinity 
\newcommand{\Rat}{\mathbf{Q}^{+}}                 % non-negative rationals 
\newcommand{\Ratmax}{\mathbf{Q}^{+}_{{\it max}}}  % non-negative rationals with minus infinity 
\newcommand{\Alt}{ \mid\!\!\mid  } 
\newcommand{\isum}{\oplus} 
\newcommand{\csum}{\uplus}              %context sum
\newcommand{\dpar}{\mid\!\mid} 
                                        % for the production of a grammar containing \mid 
\newcommand{\infer}[2]{\begin{array}{c} #1 \\ \hline #2 \end{array}} 
                                        % to make a centered inference rule 
 
% (Meta-)Logic 
 
\newcommand{\bool}{{\sf bool}}          % boolean values 
\newcommand{\Or}{\vee}                  % disjunction 
\newcommand{\OR}{\bigvee}               % big disjunction 
\newcommand{\AND}{\wedge}               % conjunction 
\newcommand{\ANDD}{\bigwedge}           % big conjunction 
\newcommand{\Arrow}{\Rightarrow}        % right double arrow 
\newcommand{\IFF}{\mbox{~~iff~~}}       % iff in roman and with spaces 
\newcommand{\iffArrow}{\Leftrightarrow} % logical equivalence 
 
% Semantics 
 
\newcommand{\dl}{[\![}                  % semantic [[ 
\newcommand{\dr}{]\!]}                  % semantic ]] 
\newcommand{\lam}{{\bf \lambda}}        % semantic lambda 


% The equivalences for this paper

% the usual ones
\newcommand{\ubis}{\approx^u}          % usual labelled weak bis
\newcommand{\uabis}{\approx^{u}_{ccs}} % usual labelled weak bis on CCS

% the contextual conv sensitive
\newcommand{\cbis}{\approx}        % convergence sensitive bis
\newcommand{\cabis}{\approx_{ccs}}  % convergence sensitive bis on CCS

% the labelled conv sensitive
\newcommand{\lcbis}{\approx^{\ell}} %
\newcommand{\lcabis}{\approx^{\ell}_{ccs}} % labelled convergence sensitive bis on CCS
\newcommand{\lcbiswrong}{\approx^{\ell \Downarrow}} %







\newcommand{\maytest}{=_{\Downarrow}}
\newcommand{\musttest}{=_{\Downarrow_{S}}}


 
 
% Sets 
 
\newcommand{\prt}[1]{{\cal P}(#1)}      % Parts of a set 
\newcommand{\finprt}[1]{{\cal P}_{fin}(#1)}% Finite parts 
\newcommand{\finprtp}[1]{{\cal P}_{fin}^{+}(#1)}% Non-empty Finite parts 
\newcommand{\union}{\cup}               % union 
\newcommand{\inter}{\cap}               % intersection 
\newcommand{\Union}{\bigcup}            % big union 
\newcommand{\Inter}{\bigcap}            % big intersection 
\newcommand{\cpl}[1]{#1^{c}}            % complement 
\newcommand{\card}{\sharp}              % cardinality 
\newcommand{\minus}{\backslash}         % set difference 
\newcommand{\sequence}[2]{\{#1\}_{#2}}  % ex. \sequence{d_n}{n\in \omega} 
\newcommand{\comp}{\circ}               % functional composition 
%\newcommand{\oset}[1]{\{#1\}}            % set enumeration 
\newcommand{\mset}[1]{\{\! | #1 |\!\}}  % pseudo-set notation {| |} 
 
% Domains 
 
\newcommand{\two}{{\bf O}}              % Sierpinski space 
\newcommand{\join}{\vee}                % join 
\newcommand{\JOIN}{\bigvee}             % big join  
\newcommand{\meet}{\wedge}              % meet 
\newcommand{\MEET}{\bigwedge}           % big meet 
\newcommand{\dcl}{\downarrow}           % down closure 
\newcommand{\ucl}{\uparrow}             % up closure 
\newcommand{\conv}{\downarrow}          % synt. conv. pred. (postfix) 
\newcommand{\diver}{\uparrow}           % diverging term 
\newcommand{\Conv}{\Downarrow}          % sem. conv. pred. (postfix) 
\newcommand{\SConv}{\Downarrow_{S}}          % sem. conv. pred. (postfix) 
\newcommand{\CConv}{\Downarrow_{C}}
\newcommand{\Diver}{\Uparrow}           % diverging map 
\newcommand{\cpt}[1]{{\cal K}(#1)}      % compacts, write \cpt{D} 
\newcommand{\ret}{\triangleleft}        % retract 
\newcommand{\nor}{\succeq}
\newcommand{\prj}{\underline{\ret}}     % projection 
\newcommand{\parrow}{\rightharpoonup}   % partial function space 
\newcommand{\ub}[1]{{\it UB}(#1)}       % upper bounds 
\newcommand{\mub}[1]{{\it MUB}(#1)}     % minimal upper bounds 
\newcommand{\lift}[1]{(#1)_{\bot}}      % lifting 
\newcommand{\forget}[1]{\underline{#1}} % forgetful translation

%\newcommand{\rel}[1]{\;{\cal #1}\;}     % infix relation (calligraphic) 
\newcommand{\rl}[1]{\;{\cal #1}\;}             % infix relation 
\newcommand{\rel}[1]{{\cal #1}}         %calligraphic relation with no 
                                        %extra space 
\newcommand{\per}[1]{\;#1 \;} 
\newcommand{\wddagger}{\natural}  % weak suspension 
%\newcommand{\wddagger}{=\!\!\!\!\parallel}  % weak suspension 
% Categories 
 
\newcommand{\pair}[2]{\langle #1 , #2 \rangle} % pairing \pair{x}{y}, do not use < >. 
 
%               *******  Notation for the $\pi$-calculus ********* 
% Syntax: 
 
 
\newcommand{\fn}[1]{{\it fn}(#1)}                       % free names 
\newcommand{\bn}[1]{{\it bn}(#1)}                       % bound names 
\newcommand{\names}[1]{{\it n}(#1)}                     % names 
\newcommand{\true}{{\sf t}}                             % true 
\newcommand{\false}{{\sf f}}                            % false 
\newcommand{\pio}{\pi_1}                                % 1 receptor calculus 
\newcommand{\pioo}{\pi_{1}^{r}} 
\newcommand{\piom}{\pi_{1}^{-}}                         % 1 receptor calculus wo match 
\newcommand{\pioi}{\pi_{1I}}                    % 1 receptor I-calculus 
\newcommand{\pifo}{\pi_{\w{1f}}}                                % functional calculus 
\newcommand{\pilo}{\pi_{\w{1l}}}                                % located calculus 
\newcommand{\sort}[1]{{\it st}(#1)}                     % sort 
\newcommand{\ia}[1]{{\it ia}(#1)}                     % sort 
\newcommand{\ite}[3]{{\sf if~} #1 {\sf ~then~} #2 {\sf ~else~} #3}      %if then else 
\newcommand{\casep}[2]{{\sf case}^{\times}(#1, \pair{x}{y}\Arrow#2)}      %case on pairs 
\newcommand{\casel}[3]{{\sf case}^{L}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists 
\newcommand{\caseb}[3]{{\sf case}^{b}(#1, #2, \s{cons}(x,y)\Arrow#3)}      %case on lists 
\newcommand{\nil}{{\sf nil}} 
\newcommand{\cons}{{\sf cons}} 
\newcommand{\idle}[1]{{\it Idle}(#1)}                   %idle process 
\newcommand{\conf}[1]{\{ #1 \}}                         %configuration 
\newcommand{\link}[2]{#1 \mapsto #2}                    %likn a ->b 
\newcommand{\mand}{\mbox{ and }} 
\newcommand{\dvec}[1]{\tilde{{\bf #1}}}                 %double vector 
\newcommand{\erloc}[1]{{\it er}_{l}(#1)}                % location erasure 
\newcommand{\w}[1]{{\it #1}}    %To write in math style 
\newcommand{\vcb}[1]{{\bf #1}} 
\newcommand{\lc}{\langle\!|} 
\newcommand{\rc}{|\!\rangle} 
\newcommand{\obj}[1]{{\it obj}(#1)}  
\newcommand{\move}[1]{{\sf move}(#1)}  
\newcommand{\qqs}[2]{\forall\, #1\;\: #2} 
\newcommand{\qtype}[4]{\forall #1 :  #2 . (#4,#3)} 
\newcommand{\xst}[2]{\exists\, #1\;\: #2} 
\newcommand{\xstu}[2]{\exists\, ! #1\;\: #2} 
\newcommand{\dpt}{\,:\,} 
\newcommand{\cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} 
\newcommand{\s}[1]{{\sf #1}}    % sans-serif  
\newcommand{\vc}[1]{{\bf #1}} 
\newcommand{\lnorm}{\lbrack\!\lbrack} 
\newcommand{\rnorm}{\rbrack\!\rbrack} 
\newcommand{\sem}[1]{\underline{#1}} 
\newcommand{\tra}[1]{\langle #1 \rangle}
\newcommand{\trb}[1]{[ #1 ]}
\newcommand{\squn}{\mathop{\scriptstyle\sqcup}} 
\newcommand{\lcro}{\langle\!|} 
\newcommand{\rcro}{|\!\rangle} 
\newcommand{\semi}[1]{\lcro #1\rcro} 
\newcommand{\sell}{\,\ell\,} 
\newcommand{\SDZ}[1]{\marginpar{\textbf{SDZ:} {#1}}} 
 
\newcommand{\when}[3]{{\sf when}~#1~{\sf then}~#2~{\sf else}~#3}  
\newcommand{\wthen}[2]{{\sf when}~#1~{\sf then}~#2~}  
\newcommand{\welse}[1]{{\sf else}~#1}  

%Pour la fleche double, il faut rajouter :
%      \usepackage{mathtools}

\newcommand{\act}[1]{\xrightarrow{#1}} %labelled actionlow %high

\newcommand{\lact}[1]{\stackrel{#1}{\makebox[5mm]{\,$- \! {\circ}\,$}}}

\newcommand{\set}[1]{\{#1\}}
\newcommand{\pst}[2]{{\sf pset}(#1,#2)}
\newcommand{\st}[2]{{\sf set}(#1,#2)}
\newcommand{\wrt}[2]{{\sf w}(#1,#2)}

\newcommand{\chtype}[2]{{\it Ch_{#1}(#2)}}
\newcommand{\rgtype}[2]{{\it {\sf Reg}_{#1} #2}}

\newcommand{\get}[1]{{\sf get}(#1)}

%\newcommand{\wact}[1]{\xRightarrow{#1}} %weak labelled action low high

%\newcommand{\mact}[1]{\xrightarrow{#1}_{m}} %labelled action low %high

%\newcommand{\wmact}[1]{\xRightarrow{#1}_{m}} %weak labelled action low high

%\newcommand{\act}[1]{\stackrel{#1}{\rightarrow}} %labelled action low
                                %%%high 

\newcommand{\acteq}[1]{\stackrel{#1}{\leadsto}} %labelled action low
                                %%%high 


%\newcommand{\actI}[1]{\stackrel{#1}{\rightarrow_{1}}} %labelled action low
\newcommand{\actI}[1]{\xrightarrow{#1}_{1}}

%\newcommand{\actII}[1]{\stackrel{#1}{\rightarrow_{2}}} %labelled action low
\newcommand{\actII}[1]{\xrightarrow{#1}_{2}}


 \newcommand{\wact}[1]{\stackrel{#1}{\Rightarrow}} %weak labelled action low high 
\newcommand{\wactI}[1]{\stackrel{#1}{\Rightarrow_{1}}} %weak labelled action low high
\newcommand{\wactII}[1]{\stackrel{#1}{\Rightarrow_{2}}} %weak labelled action low high


\newcommand{\mact}[1]{\stackrel{#1}{\rightarrow_{m}}} %labelled action low %high 
\newcommand{\wmact}[1]{\stackrel{#1}{\Rightarrow_{m}}} %weak labelled action low high 
 
%\newcommand{\lact}[1]{\stackrel{#1}{\leftarrow}} 
\newcommand{\lwact}[1]{\stackrel{#1}{\Leftarrow}} 
 
 
 
\newcommand{\eval}{\Downarrow} 
\newcommand{\Eval}[1]{\Downarrow^{#1}} 
 
 
\newcommand{\Z}{{\bf Z}} 
\newcommand{\Real}{\mathbb{R}^{+}}  
\newcommand{\Return}{\ensuremath{\mathtt{return}}\xspace}                 
\newcommand{\Stop}{\ensuremath{\mathtt{stop}}\xspace} 
\newcommand{\Wait}{\ensuremath{\mathtt{wait}}\xspace} 
\newcommand{\Read}{\ensuremath{\mathtt{read}}\xspace} 
\newcommand{\Write}{\ensuremath{\mathtt{write}}\xspace} 
\newcommand{\Yield}{\ensuremath{\mathtt{yield}}\xspace} 
\newcommand{\Next}{\ensuremath{\mathtt{next}}\xspace} 
\newcommand{\Load}{\ensuremath{\mathtt{load}}\xspace} 
\newcommand{\Call}{\ensuremath{\mathtt{call}}\xspace} 
\newcommand{\Tcall}{\ensuremath{\mathtt{tcall}}\xspace} 
\newcommand{\Pop}{\ensuremath{\mathtt{pop}}\xspace} 
\newcommand{\Build}{\ensuremath{\mathtt{build}}\xspace} 
\newcommand{\Branch}{\ensuremath{\mathtt{branch}}\xspace} 
\newcommand{\Goto}{\ensuremath{\mathtt{goto}}\xspace} 
 
\newcommand{\hatt}[1]{#1^{+}} 
\newcommand{\Of}{\mathbin{\w{of}}} 
 
\newcommand{\susp}{\downarrow} 
\newcommand{\lsusp}{\Downarrow_L} 
\newcommand{\wsusp}{\Downarrow} 
\newcommand{\commits}{\searrow} 
 
 
\newcommand{\spi}{S\pi} 
 

 \newcommand{\pres}[2]{#1\triangleright #2} %TCCS else next (alternative)
% \newcommand{\pres}[2]{ \lfloor #1 \rfloor (#2)}  %TCCS else next
\newcommand{\present}[3]{{\sf present} \ #1 \ {\sf do } \ #2 \ {\sf  else} \ #3}


\newcommand{\tick}{{\sf tick}}          %tick action

 
 
\newcommand{\sbis}{\equiv_L} 
\newcommand{\emit}[2]{\ol{#1}#2}  
%\newcommand{\present}[4]{#1(#2).#3,#4} 
\newcommand{\match}[4]{[#1=#2]#3,#4}       %pi-equality 

\newcommand{\matchv}[4]{[#1 \unrhd #2]#3,#4}

\newcommand{\new}[2]{\nu #1 \ #2} 
\newcommand{\outact}[3]{\new{{\bf #1}}{\emit{#2}{#3}}} 
\newcommand{\real}{\makebox[5mm]{\,$\|\!-$}}% realizability relation 

\newcommand{\regterm}[2]{{\sf reg}_{#1} #2}
\newcommand{\thread}[1]{{\sf thread} \ #1}
\newcommand{\store}[2]{(#1 \leftarrow #2)}
\newcommand{\pstore}[2]{(#1 \Leftarrow #2)}

\newcommand{\regtype}[2]{{\sf Reg}_{#1} #2}
\newcommand{\uregtype}[3]{{\sf Reg}_{#1}(#2, #3)}
\newcommand{\urtype}[2]{{\sf Reg}(#1, #2)}

\newcommand{\upair}[2]{[#1,#2]}
\newcommand{\letb}[3]{\mathsf{let}\;\oc #1 = #2\;\mathsf{in}\;#3}

\newcommand{\vlt}[1]{{\cal V}(#1)}
\newcommand{\prs}[1]{{\cal P}(#1)}

\newcommand{\imp}{{\sf Imp}}            %imp language
\newcommand{\vm}{{\sf Vm}}              %virtual machine language
\newcommand{\mips}{{\sf Mips}}          %Mips language
\newcommand{\C}{{\sf C}}                % C language
\newcommand{\Clight}{{\sf Clight}}        %C light language
\newcommand{\Cminor}{{\sf Cminor}}
\newcommand{\RTLAbs}{{\sf RTLAbs}}
\newcommand{\RTL}{{\sf RTL}}
\newcommand{\ERTL}{{\sf ERTL}}
\newcommand{\LTL}{{\sf LTL}}
\newcommand{\LIN}{{\sf LIN}}
\newcommand{\access}[1]{\stackrel{#1}{\leadsto}}
\newcommand{\ocaml}{{\sf ocaml}}
\newcommand{\coq}{{\sf Coq}}
\newcommand{\compcert}{{\sf CompCert}}
%\newcommand{\cerco}{{\sf CerCo}}
\newcommand{\cost}{{\sf Cost}}
\newcommand{\lamcost}{\sf LamCost}
\newcommand{\ilcost}{{\sf IndLabCost}}
\newcommand{\ilacc}{{\sf IndLabAcc}}
\newcommand{\cil}{{\sf CIL}}
\newcommand{\scade}{{\sf Scade}}
\newcommand{\absint}{{\sf AbsInt}}
\newcommand{\framac}{{\sf Frama-C}}
\newcommand{\powerpc}{{\sf PowerPc}}
\newcommand{\lustre}{{\sf Lustre}}
\newcommand{\esterel}{{\sf Esterel}}
\newcommand{\ml}{{\sf ML}}

\newcommand{\codeex}[1]{\texttt{#1}}   % code example

\bibliographystyle{abbrv} 

\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Report \\
D5.1 Untrusted CerCo Prototype \\
and \\
D5.3 Case study: analysis of synchronous code
\\
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas, Paolo Tranquilli
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: \cerco{}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\

\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}

\newpage


\vspace*{7cm}

\paragraph{Summary}
The deliverable D5.1-D5.3 is composed of the following parts:

\begin{enumerate}

\item This summary.

\item The paper \cite{A12} and the related software $\cost$.

\item The paper \cite{T12} and the related prototype compiler \ilacc{} (and its \cost{} branch, \ilcost{}).

\item The paper \cite{ARG11} and the related software $\lamcost$.

\item The paper \cite{MA11}.

\end{enumerate}

This document and the softwares mentioned above can be downloaded at the 
page:
\begin{center}
{\tt http://cerco.cs.unibo.it/}
\end{center}

{\scriptsize
\begin{thebibliography}{99}


\bibitem{A12}
N.~Ayache.
\newblock Synthesis of certified cost bounds.
\newblock Universit\'e Paris Diderot. Internal report documenting the $\cost$ software, 2012.


\bibitem{ARG11}
R.M.~Amadio, Y.~R\'egis-Gianas.
\newblock Certifying and reasoning on cost annotations of functional programs.
\newblock In Proc. FOPARA, Springer LNCS (to appear), 2012. 
\newblock Also Research Report, Universit\'e Paris Diderot,
{\tt http://hal.inria.fr/inria-00629473/en/}, 2011.


\bibitem{MA11}
A.~Madet, R.M.~Amadio.
\newblock An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.
\newblock In Proc. TLCA, Springer LNCS 6690:138-152, 2011. 
\newblock Also Research Report, Universit\'e Paris Diderot, 
{\tt http://hal.archives-ouvertes.fr/hal-00569095/fr/}, 2011.

\bibitem{T12}
P.~Tranquilli.
\newblock Indexed labels for loop iteration dependent costs.
\newblock Universit\`a di Bologna. Internal report documenting the indexed labels software, 2012.

\end{thebibliography}}

\newpage

\paragraph{Aim}
The main aim of WP5 is to develop proof of concept prototypes where
the (untrusted) compiler implemented in WP2 is interfaced with existing tools 
in order to synthesize complexity  assertions on the execution 
time of programs. Eventually, the approach should be adapted to
the trusted compiler developed in WP3 and WP4 (cf. deliverable D5.2 at
month 36).

The main planned contribution of deliverable D5.1 is a
tool that takes as input an annotated C program produced by the CerCo
compiler and tries to synthesize a certified bound on the execution
time of the program.  The related expected contribution of deliverable
D5.3 amounts to apply the tool described in D5.1 to the C programs generated
by a Lustre compiler.  This planned work is described in the first
document...which accompanies a software distribution...
Frama-C plug-in ...more examples...

\paragraph{Synthesis of certified cost bounds}
The main planned contribution of deliverable D5.1 is a tool that takes
as input an annotated $\C$ program produced by the $\cerco$ compiler
and tries to synthesize a certified bound on the execution time of the
program.  The related expected contribution of deliverable D5.3
amounts to apply the developed tool to the $\C$ programs generated by
a $\lustre$ compiler.  This work is described in the first document
\cite{A12} which accompanies a software distribution called $\cost$.
The development takes the form of a `$\framac$ plug-in'.  $\framac$ is
an open source and well-established platform to reason formally on
$\C$ programs. The proof obligations generated from Hoare style
assertions on $\C$ programs are passed to a small number of provers
that try to discharge them automatically. The platform has been
designed to be extensible by means of so called plug-in's written in
$\ocaml$.  The $\cost$ software is a $\framac$ plug-in which in first
approximation takes the following actions: (1) it receives as input a
$\C$ program, (2) it applies the $\cerco$ compiler to produce a
related $\C$ program with cost annotations, (3) it applies some
heuristics to produce a tentative bound on the cost of executing a
$\C$ function as a function of the value of its parameters, (4) it
calls the provers embedded in the $\framac$ tool to discharge the
related proof obligations.  The current size of the $\cost$ plug-in is
4K lines of $\ocaml$ code.  More details are available in the first
part of the document \cite{A12}.  The second part of the document
(formally, corresponding to deliverable D5.3) tries to delimit the
practical applicability of the plug-in. To this end, the tool has been
applied to the $\C$ code generated by the $\lustre$ compiler and to
some other simple $\C$ programs.

We pause to recall a redistribution of the workforce of the UPD site.
Following the resignation of the doctoral student at the end of year
1, the contract of the post-doc which expired at month 13 
has been as extended till month 33.  
It follows that in the UPD site there has been a shift of manpower from
the third to the second year. Because of this shift we 
anticipate the presentation of deliverable D5.3 at month 24 rather
than month 36. 


\paragraph{Indexed labels for loop iteration dependent costs}
The first year scientific review report, among other things, contrasts
the $\cerco$ approach with the one adopted in tools such as $\absint$
which are used by the WCET community and it recommends that the
approach to cost annotations described in WP2 is made {\em coarser},
{\em i.e.}, that a label covers a larger portion of code.  During the
second year, most of the work of a post-doc at UNIBO was aimed at
addressing this remark \cite{T12}.  This has resulted in a refinement
of the labelling approach into a so called {\em indexed labelling}.
It consists in formally indexing cost labels with the iterations of
the containing loops they occur in within the source code.  These
indexes can be transformed during the compilation, and when lifted
back to source code they produce dependent costs. Preliminary
experiments suggest that this refinement allows to retain preciseness
when the program is subject to loop transformations such as loop
peeling and loop unrolling.  A prototype implementation has been
developed on top of the untrusted $\cerco$ compiler D2.2.


% so as to take into account the effects of 
%% cache memories and pipelines. Following this suggestion
%% a post-doc at UB has worked on these issues and we have invited
%% C. Ferdinand to present the AbsInt tool.
%% (*** Lack of compositionality --- timing anomalies --- ***)



\paragraph{Certifying and reasoning on cost annotations of functional programs}
During the second year some unplanned work related to deliverables
D5.1 and D5.3 has taken place at UPD.  The main development
\cite{ARG11} concerns the extension of the $\cerco$ labelling approach
described in D2.1 to a standard compilation chain from a higher-order
functional language of the $\ml$ family to $\C$.  This
work shows that the approach is sufficiently general to be applied to
higher-order programs whose concrete complexity is generally regarded
as difficult to estimate.  Moreover, the introduction of
higher-order functions calls for a higher-order logic to reason on the
cost annotations.  In this respect, we have built on previous work by
one of the authors on a higher-order Hoare logic. Starting from a
(higher-order) specification of the expected cost of a function our
tool $\lamcost$ produces automatically a list of proof obligations. Preliminary
experiments suggest that a large part of these proof obligations can
be discharged automatically and that the remaining ones can be proved
in a proof assistant such as $\coq$.  Ongoing work that should be
completed within the third year of the project is extending the
compilation chain and the cost analysis to include garbage collection
using a {\em region based} memory management \`a la Tofte-Talpin.

\paragraph{An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.}
A second development at UPD is of a more speculative nature and is
concerned with the design of a type system for a functional language
with side effects that guarantees complexity bounds \cite{MA11}. As far as we
know, this is the first work that accounts for side effects. The
obtained result concerns {\em elementary time} and ongoing work that
should be completed within the third year of the project concerns a
similar result for {\em polynomial time}.  We regard this work as a
step towards bridging the $\cerco$ approach with the work on {\em
  Implicit computational complexity} (ICC) in which our universities
are also involved (in 2011, the $\cerco$ project organised in Paris a
joint workshop with an ICC oriented project).  As a matter of fact,
there is still a large gap to be filled before the results in ICC can
have an impact on the practice of programming.

A second development is of a more speculative nature and 
concerned with the development of a type system
for a functional langauge with side effects that guarantees a complexity
bound... First work to account for side effects... Ongoing work tries to
extend the framework to polynomial time. Eventually we hope to join
the thread on implicit complexity...??? 



\newpage

\includepdf[pages={-}]{plugin.pdf}


\newpage

\includepdf[pages={-}]{tranquilli.pdf}

\newpage


\includepdf[pages={-}]{fopara.pdf}


\newpage

\includepdf[pages={-}]{tlca.pdf}


\end{document}