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

Last change on this file since 1657 was 1657, checked in by amadio, 8 years ago

preliminary version of D5

File size: 22.4 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 n. D5.1 Untrusted CerCo Prototype \\
556and \\
557D5.3 Case study: analysis of synchronous code
558\\
559\end{LARGE} 
560\end{center}
561
562\vspace*{2cm}
563\begin{center}
564\begin{large}
565Version 1.0
566\end{large}
567\end{center}
568
569\vspace*{0.5cm}
570\begin{center}
571\begin{large}
572Main Authors:\\
573Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas,
574\end{large}
575\end{center}
576
577\vspace*{\fill}
578\noindent
579Project Acronym: \cerco{}\\
580Project full title: Certified Complexity\\
581Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
582
583\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
584
585\newpage
586
587
588\vspace*{7cm}
589
590\paragraph{Summary}
591The main aim of WP5 is to develop proof of concept prototypes where
592the (untrusted) compiler developed in WP 2 is interfaced with existing tools
593in order to synthesize complexity  assertions on the execution
594time of programs. 
595
596The main expected contribution (D5.1) is a Frama-C plug-in that takes as
597input the annotated C program produced by the CerCo compiler and
598tries to synthesize a certified bound on the execution time.
599
600Because of the redistribution of the workforce in the UDP site
601(following the resignation of the doctoral student at the end of year 1
602the contract of the post-doc has been extended till month ??) we propose
603to anticipate at month 24 instead of month 36 the presentation of
604deliverable D5.3 which is consists in particular in applying
605the Frama-C plug-in to the C programs generated by a Lustre compiler.
606
607This work is described in the document ...
608
609During the second year some unplanned work has taken place.
610
611The main development concerns the extension of the CerCo labelling
612approach to a standard compilation chain from a higher-order functional
613language of the ML family to C and the development of framework to reason
614about the cost annotations. This work shows...the generality of the approach...
615Parallel the work done for C...
616Ongoing work tries to produce valid garbage collection statements by typing...
617
618A second development is concerned with the development of a type system
619for a functional langauge with side effects that guarantees a complexity
620bound... First work to account for side effects... Ongoing work tries to
621extend the framework to polynomial time. Eventually we hope to join
622the thread on implicit complexity???
623
624\newpage
625
626\includepdf[pages={-}]{plugin.pdf}
627
628
629\newpage
630
631\includepdf[pages={-}]{fopara.pdf}
632
633
634\newpage
635
636\includepdf[pages={-}]{tlca.pdf}
637
638
639\end{document}
Note: See TracBrowser for help on using the repository browser.