Changeset 1852 for Deliverables


Ignore:
Timestamp:
Mar 15, 2012, 4:02:06 PM (8 years ago)
Author:
campbell
Message:

Revise WP3 down.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP3.tex

    r1845 r1852  
    3434%\setbeamertemplate{footline}[page number]
    3535%\setbeamertemplate{sidebar right}{}
     36\setbeamertemplate{navigation symbols}{}
    3637
    3738\lstdefinelanguage{coq}
     
    7576
    7677\frame{
    77 \frametitle{Introduction}
    78 
    79 An interleaved presentation of work on:
    80 \begin{description}
    81 \item[T3.2] The encoding of the front-end of the \cerco{} compiler in CIC
    82 \item[T3.3] Defining the executable semantics of the front-end's intermediate
    83   language
    84 \item[T3.4] Correctness proofs
     78\frametitle{Achievements in period 2}
     79
     80\begin{description}[T3.2]
     81\item[T3.2] \alert{Completed}: Matita encoding of compiler front-end
     82\item[T3.3] \alert{Completed}: Executable semantics for intermediate  languages
     83\item[T3.4] \alert{In progress}: Correctness proofs
    8584\end{description}
    8685
    8786\bigskip
    88 Deliverables D3.2 and D3.3 have been produced.
     87Deliverables D3.2 and D3.3 submitted.
     88
     89\bigskip
     90This talk is an interleaved presentation of these results.
     91
    8992
    9093}
     
    9598
    9699\begin{itemize}
    97 \item Common definitions for everything
    98 \item The front end:
    99 \end{itemize}
    100 
    101 \begin{tabbing}
     100\item Shared definitions
     101%\item The front end:
     102%\end{itemize}
     103%\vspace{-3ex}
     104\item \begin{tabbing}
    102105\quad \= $\downarrow$ \quad \= \kill
    103106\gray{\textsf{C} (unformalized)}\\
     
    115118\> \,\gray{\vdots} \> \gray{start of target specific backend}
    116119\end{tabbing}
    117 
    118 \begin{itemize}
     120%\vspace{-3ex}
     121%\begin{itemize}
    119122\item Structured traces
    120123\end{itemize}
     
    122125}
    123126
    124 \section{Common}
    125 
    126 \begin{frame}[fragile]
    127 \frametitle{Common: identifiers}
    128 
    129 Variable and function names, cost labels, registers, CFG labels, \dots
     127\section{Shared}
     128
     129\begin{frame}[fragile]
     130\frametitle{Shared definitions}
     131
     132Identifiers: variables, cost labels, CFG labels, \dots
    130133
    131134\begin{itemize}
    132135\item Represented by arbitrarily large binary numbers and trees
    133136\begin{itemize}
    134 \item D3.3 described a `lazy failure' approach reusing existing structures
    135 \item Impractical for adding invariants (types may depend on success of
    136   name generation)
    137 \item Use this CompCert-like system instead
     137\item D3.3 `lazy failure' approach reusing existing structures
     138\item Invariant's types may depend on success of name generation
     139%\item Use this CompCert-like system instead
    138140\end{itemize}
    139141\item Tags for some type safety:
     
    144146\end{itemize}
    145147
    146 \end{frame}
    147 
    148 \frame{
    149 \frametitle{Other common definitions}
    150 
    151 \begin{itemize}
    152 \item Memory, global environments from D3.1
    153 \item Bit vector based arithmetic from D4.1
     148Memory, global environments from D3.1\\
     149Bit vector based arithmetic from D4.1
    154150  \begin{itemize}
    155151  \item added extra operations, increased efficiency
    156152  \end{itemize}
    157 \item Common record type for small-step executable semantics
    158   \begin{itemize}
    159   \item used for animation
    160   \item intended to be used when defining simulations
    161   \end{itemize}
    162 \end{itemize}
    163 
    164 \bigskip
    165 
    166 \bigskip
     153%Common record type for small-step executable semantics
     154%  \begin{itemize}
     155%  \item used for animation
     156%  \item intended to be used when defining simulations
     157%  \end{itemize}
     158
     159
     160
    167161\textsf{Cminor} and \textsf{RTLabs} share operations on values.
    168162
    169 \begin{itemize}
    170 \item one syntax, one semantics
    171 \item straightforward
    172 \item no overloading (unlike \textsf{Clight})
    173 \end{itemize}
    174 
    175 }
     163
     164\end{frame}
    176165
    177166\section{Clight}
     
    179168\frametitle{Clight: syntax and semantics}
    180169
    181 Largely unchanged from D3.1, except:
     170Modest evolution from D3.1, except:
    182171
    183172\medskip
     
    197186\frametitle{Clight: cast simplification}
    198187
    199 \begin{itemize}
    200 \item C insists on arithmetic promotion
     188C insists on arithmetic promotion
     189\begin{itemize}
    201190\item CIL-based \ocaml{} parser adds suitable casts
    202191\item bad for our target (32-bit ops instead of 8-bit)
    203192\end{itemize}
    204193
    205 Prototype recognises fixed patterns:
     194\medskip
     195Prototype recognises fixed patterns to simplify:
    206196\[ (t)((t_1)e_1\ op\ (t_2)e_2) \]
    207 and replaces when types are right.  Have done some preliminary proofs that this
    208 works.
     197\vspace{-4ex}
    209198\begin{itemize}
    210199\item Deep pattern matching is awkward in Matita
     
    212201\end{itemize}
    213202
    214 \red{Instead}: recursive `coerce to desired type' approach.\\
     203\medskip
     204\red{Instead}: recursive `coerce to desired type' approach.
     205
     206Have done some preliminary proofs that this
     207works.
    215208% (Doesn't get some things,
    216209% e.g., \lstinline'==')
     
    223216
    224217\begin{itemize}
    225 \item Implemented as a simple recursive function, like prototype
     218\item a simple recursive function, like prototype
    226219\item uses common identifiers definition to produce fresh cost labels
    227220\end{itemize}
     
    241234\frametitle{Cminor syntax and semantics}
    242235
    243 Similar language to CompCert's but developed from prototype.
     236Similar to CompCert's --- but developed from prototype.
    244237
    245238\begin{itemize}
     
    288281\frametitle{Invariants for identifiers}
    289282
    290 Invariants change between language syntax/semantics and compilation stages:
     283
     284Invariants change between languages and compilation:
    291285
    292286\begin{description}
     
    296290\end{description}
    297291
    298 When using or creating function records we prove that we can switch between
    299 them:
     292When using or creating function definitions have proved that we can switch between
     293invariants:
    300294\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    301295lemma populates_env : $\forall$l,e,u,l',e',u'.
     
    303297  populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *)
    304298  $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* Anything in the environment... *)
    305       Env_has e' i t.
    306       (* maps to something of the correct type *)
    307 \end{lstlisting}
    308 
     299      Env_has e' i t.      (* maps to something of the correct type *)
     300\end{lstlisting}
     301
     302\vfill
    309303\end{frame}
    310304
     
    313307
    314308Embedded invariant in the function record:
    315 \begin{lstlisting}[language=matita,basicstyle=\scriptsize\tt]
     309\begin{lstlisting}[language=matita,basicstyle=\scriptsize\tt,morekeywords=f_inv]
    316310record internal_function : Type[0] ≝
    317311{ f_return     : option typ
     
    333327\end{enumerate}
    334328
    335 How is \lstinline'stmt_P' defined?
    336 \end{frame}
     329\end{frame}
     330
     331
     332\section{Clight to Cminor}
     333
     334\begin{frame}
     335\frametitle{Clight to Cminor}
     336
     337Two main jobs:
     338\begin{enumerate}
     339\item make memory allocation of variables explicit
     340\item use simpler control structures
     341\end{enumerate}
     342Again, based on prototype rather than CompCert.
     343
     344\bigskip
     345Added type checking:
     346\begin{itemize}
     347\item satisfies the restrictions for Cminor expressions
     348\item could separate out, have a `nice Clight' language
     349\end{itemize}
     350Similarly, code checks
     351\begin{itemize}
     352\item variable environments are well-formed
     353\item all \lstinline'goto' labels are translated
     354\end{itemize}
     355\end{frame}
     356
     357\begin{frame}
     358\frametitle{Clight to Cminor proofs}
     359
     360Beyond the invariants already shown, we will prove:
     361
     362\medskip
     363\begin{enumerate}
     364\item a simulation relation
     365  \begin{itemize}
     366  \item between statement and continuation pairs
     367  \item using memory injection (similar to CompCert)
     368  \end{itemize}
     369\item syntactic cost labelling properties are preserved
     370  \begin{itemize}
     371  \item structural induction on function body
     372  \end{itemize}
     373\end{enumerate}
     374\end{frame}
     375
     376\section{Initialisation}
     377\begin{frame}
     378\frametitle{Cminor: initialization}
     379
     380Replace initialization data by code in the initial function.
     381
     382\begin{itemize}
     383\item straightforward to define
     384\item instantiate a slightly different version of the semantics for it
     385\begin{itemize}
     386\item Can't accidentally forget the pass
     387\end{itemize}
     388\end{itemize}
     389
     390\bigskip
     391Correctness should follow because the state after the initialisation will
     392be the same as the initial state of the original.
     393\end{frame}
     394
     395\section{RTLabs}
     396\begin{frame}[fragile]
     397\frametitle{RTLabs: syntax and semantics}
     398
     399Register Transfer Language with front-end operations.
     400
     401Control flow graph implemented by generic identifiers map:
     402
     403\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
     404definition label := identifier LabelTag.
     405definition graph : Type[0] $\rightarrow$ Type[0] := identifier_map LabelTag.
     406
     407inductive statement : Type[0] ≝
     408| St_skip : label $\rightarrow$ statement
     409| St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement
     410| St_op1 : $\forall$t,t'. unary_operation t' t $\rightarrow$ register
     411   $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement
     412...
     413\end{lstlisting}
     414\vspace{-1.5ex}
     415\begin{itemize}
     416\item Shares basic operations (including semantics) with Cminor.
     417\item Tags prevent confusion of labels (graph vs.~goto vs.~cost).
     418\end{itemize}
     419
     420Semantics straightforward interpretation of statements.
     421\end{frame}
     422
     423\begin{frame}[fragile]
     424\frametitle{RTLabs: syntax and semantics}
     425
     426\begin{lstlisting}[language=matita]
     427record internal_function : Type[0] ≝
     428{ f_labgen    : universe LabelTag
     429; f_reggen    : universe RegisterTag
     430...
     431; f_graph     : graph statement
     432; f_closed    : graph_closed f_graph
     433; f_typed     : graph_typed (f_locals @ f_params) f_graph
     434...
     435\end{lstlisting}
     436
     437Enforce that
     438\begin{itemize}
     439\item every statement's successor labels are present in the CFG
     440\item every statement should be well-typed (for limited type system)
     441\end{itemize}
     442
     443\end{frame}
     444
     445\section{Cminor to RTLabs}
     446\begin{frame}
     447\frametitle{Cminor to RTLabs}
     448
     449Break down statements and expressions into RTL graph.
     450
     451\begin{itemize}
     452\item Incrementally build function backwards
     453\item all state is in function record, like prototype
     454\end{itemize}
     455
     456%\bigskip
     457%May investigate whether a state monad makes invariant management easier.
     458
     459\bigskip
     460Showing graph closure requires
     461\begin{itemize}
     462\item monotonicity of graph construction
     463\item eventual insertion of all \lstinline'goto' destinations
     464\end{itemize}
     465
     466Carry these along in the partially built function record.
     467
     468\end{frame}
     469
     470% \begin{frame}[fragile]
     471% \frametitle{Cminor nesting depth}
     472
     473% Want to prevent
     474% \begin{lstlisting}[language=C]
     475% void f() {
     476%   block { loop { exit 5; } }
     477% }
     478% \end{lstlisting}
     479
     480% Index statements by block depth
     481% \begin{lstlisting}[language=matita]
     482% inductive stmt : $\forall$blockdepth:nat. Type[0] ≝
     483% | St_skip : $\forall$n. stmt n
     484% ...
     485% | St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n
     486% | St_exit : $\forall$n. Fin n $\rightarrow$ stmt n
     487% ...
     488% \end{lstlisting}
     489
     490% \begin{itemize}
     491% \item In semantics index continuations too
     492% \item Use \lstinline[language=matita]'Fin n' to make \lstinline'k_exit'
     493% a total function
     494% \end{itemize}
     495
     496% (May be able to remove entirely if we redo \lstinline[language=C]{switch}?)
     497% \end{frame}
     498
     499\begin{frame}[fragile]
     500\frametitle{Establishing RTLabs invariants}
     501
     502Use dependent pairs to show invariant along with results.
     503
     504\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%]
     505let rec add_expr ... (e:expr ty)
     506   (Env:expr_vars ty e (present ?? env))
     507   (f:partial_fn le)
     508 on e: $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝
     509
     510match e return
     511   $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$ ... with
     512[ ...
     513| Cst _ c $\Rightarrow$ $\lambda$_. %\guillemotleft%add_fresh_to_graph ? (St_const dst c) f ?, ?%\guillemotright%
     514...
     515\end{lstlisting}
     516
     517Continually appeal to monotonicity (\lstinline'fn_graph_included').\\
     518Use unification hints to simplify stepping back.
     519
     520\end{frame}
     521
     522\frame{
     523\frametitle{Cminor to RTLabs: cost labels}
     524
     525Two cost label properties are the same, the third will require more
     526work:
     527\begin{enumerate}
     528\item cost label at head of function
     529\item cost label after branching instructions
     530\item cost labels at the head of each loop / \lstinline'goto' destination
     531\end{enumerate}
     532
     533No simple notion of the head of a loop or \lstinline'goto' any more.
     534
     535\medskip
     536Instead: will prove in \alert{Cminor} that after following a finite
     537number of instructions we reach either
     538\begin{itemize}
     539\item a cost label, or
     540\item the end of the function
     541\end{itemize}
     542
     543}
     544
     545\section{Structured traces}
     546\frame{
     547\frametitle{RTLabs structured traces}
     548
     549Front-end only uses flat traces consisting of single steps.
     550
     551\bigskip
     552The back-end will need the function call structure and the labelling
     553properties in order to show that the generated costs are correct.
     554
     555\begin{itemize}
     556\item Traces are structured in sections from cost label to cost label,
     557\item the entire execution of function calls nested as a single `step',
     558\item a coinductive definition presents non-terminating traces, using the
     559  inductive definition for all terminating function calls
     560\end{itemize}
     561
     562\bigskip
     563RTLabs chosen because it is the first languages where statements:
     564\begin{itemize}
     565\item take one step each (modulo function calls)
     566\item have individual `addresses'
     567\end{itemize}
     568}
     569
     570\frame{
     571\frametitle{RTLabs structured traces}
     572Have already established the existence of such traces
     573\begin{itemize}
     574\item termination decided classically
     575\item syntactic labelling properties used to build semantic structure
     576\item show stack preservation to ensure that function calls \texttt{return}
     577  to the correct location
     578\item tricky to establish guardedness of definitions
     579\end{itemize}
     580
     581\bigskip
     582Next, prove that flattening these traces yields the original.
     583}
     584
     585\frame{
     586\frametitle{Conclusion}
     587
     588Syntax, semantics and translations of prototype now implemented in Matita.
     589
     590\bigskip
     591Have defined and established
     592\begin{itemize}
     593\item invariants regarding variables, typing and program structure
     594\item a rich form of execution trace to pass to the back-end
     595\end{itemize}
     596
     597\medskip
     598Work in progress:
     599\begin{itemize}
     600\item showing functional correctness of the front-end
     601\item proving that cost labelling is appropriate, and preserved
     602\end{itemize}
     603
     604Finally, \alert{end-to-end} functional and cost correctness results.
     605
     606}
     607
     608\frame{
     609\frametitle{Extra detail beyond here...}
     610}
    337611
    338612\begin{frame}[fragile]
     
    360634
    361635\end{frame}
    362 
    363 
    364 \section{Clight to Cminor}
    365 
    366 \begin{frame}
    367 \frametitle{Clight to Cminor}
    368 
    369 Two main jobs:
    370 \begin{enumerate}
    371 \item make memory allocation of variables explicit
    372 \item use simpler control structures
    373 \end{enumerate}
    374 Again, based on prototype rather than CompCert.
    375 
    376 \bigskip
    377 Added type checking:
    378 \begin{itemize}
    379 \item satisfies the restrictions for Cminor expressions
    380 \item could separate out, have a `nice Clight' language
    381 \end{itemize}
    382 Similarly, check variable environments are sane, check all \lstinline'goto'
    383 labels are translated.
    384 \end{frame}
    385 
    386 \begin{frame}
    387 \frametitle{Clight to Cminor proofs}
    388 
    389 Beyond the invariants already shown, we need to prove:
    390 \begin{enumerate}
    391 \item a simulation using
    392   \begin{itemize}
    393   \item memory injection (similar to CompCert)
    394   \item relation based around source and target's statements and continuations
    395   \end{itemize}
    396 \item syntactic cost labelling properties are preserved
    397   \begin{itemize}
    398   \item structural induction on function body
    399   \end{itemize}
    400 \end{enumerate}
    401 \end{frame}
    402 
    403 \section{Initialisation}
    404 \begin{frame}
    405 \frametitle{Cminor: initialization}
    406 
    407 Replace initialization data by code in the initial function.
    408 
    409 \begin{itemize}
    410 \item straightforward to define
    411 \item instantiate a slightly different version of the semantics for it
    412 \begin{itemize}
    413 \item Can't accidentally forget the pass
    414 \end{itemize}
    415 \end{itemize}
    416 
    417 \bigskip
    418 Correctness should follow because the state after the initialisation will
    419 be the same as the initial state of the original.
    420 \end{frame}
    421 
    422 \section{RTLabs}
    423 \begin{frame}[fragile]
    424 \frametitle{RTLabs: syntax and semantics}
    425 
    426 Register Transfer Language with front-end operations.
    427 
    428 Control flow graph implemented by generic identifiers map:
    429 
    430 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    431 definition label ≝ identifier LabelTag.
    432 definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag.
    433 
    434 inductive statement : Type[0] ≝
    435 | St_skip : label $\rightarrow$ statement
    436 | St_cost : costlabel $\rightarrow$ label $\rightarrow$ statement
    437 | St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement
    438 | St_op1 : $\forall$t,t'. unary_operation t' t $\rightarrow$ register
    439    $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement
    440 ...
    441 \end{lstlisting}
    442 \begin{itemize}
    443 \item Shares basic operations (including semantics) with Cminor.
    444 \item Tags prevent confusion of labels (graph vs.~goto vs.~cost).
    445 \end{itemize}
    446 
    447 Semantics are straightforward interpretation of statements.
    448 \end{frame}
    449 
    450 \begin{frame}[fragile]
    451 \frametitle{RTLabs: syntax and semantics}
    452 
    453 \begin{lstlisting}[language=matita]
    454 record internal_function : Type[0] ≝
    455 { f_labgen    : universe LabelTag
    456 ; f_reggen    : universe RegisterTag
    457 ...
    458 ; f_graph     : graph statement
    459 ; f_closed    : graph_closed f_graph
    460 ; f_typed     : graph_typed (f_locals @ f_params) f_graph
    461 ...
    462 \end{lstlisting}
    463 
    464 Enforce that
    465 \begin{itemize}
    466 \item every statement's successor labels are present in the CFG
    467 \item every statement should be well-typed (for limited type system)
    468 \end{itemize}
    469 
    470 \end{frame}
    471 
    472 \section{Cminor to RTLabs}
    473 \begin{frame}
    474 \frametitle{Cminor to RTLabs}
    475 
    476 Break down statements and expressions into RTL graph.
    477 
    478 \begin{itemize}
    479 \item Incrementally build function backwards
    480 \item all state is in function record, like prototype
    481 \end{itemize}
    482 
    483 \bigskip
    484 May investigate whether a state monad makes invariant management easier.
    485 
    486 \bigskip
    487 Showing graph closure requires
    488 \begin{itemize}
    489 \item monotonicity of graph construction
    490 \item eventual insertion of all \lstinline'goto' destinations
    491 \end{itemize}
    492 
    493 Carry these along in the partially built function record.
    494 
    495 \end{frame}
    496 
    497 % \begin{frame}[fragile]
    498 % \frametitle{Cminor nesting depth}
    499 
    500 % Want to prevent
    501 % \begin{lstlisting}[language=C]
    502 % void f() {
    503 %   block { loop { exit 5; } }
    504 % }
    505 % \end{lstlisting}
    506 
    507 % Index statements by block depth
    508 % \begin{lstlisting}[language=matita]
    509 % inductive stmt : $\forall$blockdepth:nat. Type[0] ≝
    510 % | St_skip : $\forall$n. stmt n
    511 % ...
    512 % | St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n
    513 % | St_exit : $\forall$n. Fin n $\rightarrow$ stmt n
    514 % ...
    515 % \end{lstlisting}
    516 
    517 % \begin{itemize}
    518 % \item In semantics index continuations too
    519 % \item Use \lstinline[language=matita]'Fin n' to make \lstinline'k_exit'
    520 % a total function
    521 % \end{itemize}
    522 
    523 % (May be able to remove entirely if we redo \lstinline[language=C]{switch}?)
    524 % \end{frame}
    525 
    526 \begin{frame}[fragile]
    527 \frametitle{Establishing RTLabs invariants}
    528 
    529 Use dependent pairs to show invariant along with results.
    530 
    531 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%]
    532 let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
    533    (Env:expr_vars ty e (present ?? env))
    534    (dst:register)
    535    (f:partial_fn le)
    536  on e: $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝
    537 
    538 match e return
    539    $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$
    540          $\Sigma$f':partial_fn le. fn_graph_included le f f' with
    541 [ ...
    542 | Cst _ c $\Rightarrow$ $\lambda$_. %\guillemotleft%add_fresh_to_graph ? (St_const dst c) f ?, ?%\guillemotright%
    543 ...
    544 \end{lstlisting}
    545 
    546 Continually appeal to monotonicity (\lstinline'fn_graph_included'),
    547 use unification hints to simplify stepping back.
    548 
    549 \end{frame}
    550 
    551 \frame{
    552 \frametitle{Cminor to RTLabs: cost labels}
    553 
    554 Two of the cost label properties are easy to deal with, the third will require more
    555 work:
    556 \begin{enumerate}
    557 \item cost label at head of function
    558 \item cost label after branching instructions
    559 \item cost labels at the head of each loop / \lstinline'goto' destination
    560 \end{enumerate}
    561 
    562 No simple notion of the head of a loop or \lstinline'goto' any more.
    563 
    564 \medskip
    565 Instead will prove in \alert{Cminor} that after following a finite
    566 number of instructions we reach either
    567 \begin{itemize}
    568 \item a cost label, or
    569 \item the end of the function
    570 \end{itemize}
    571 
    572 }
    573 
    574 \section{Structured traces}
    575 \frame{
    576 \frametitle{RTLabs structured traces}
    577 
    578 Front-end only uses flat traces consisting of single steps.
    579 
    580 \bigskip
    581 The back-end will need the function call structure and the labelling
    582 properties in order to show that the generated costs are correct.
    583 
    584 \begin{itemize}
    585 \item Traces are structured in sections from cost label to cost label,
    586 \item the entire execution of function calls nested as a single `step',
    587 \item a coinductive definition presents non-terminating traces, using the
    588   inductive definition for all terminating function calls
    589 \end{itemize}
    590 
    591 \bigskip
    592 RTLabs chosen because it is the first languages where statements:
    593 \begin{itemize}
    594 \item take one step each (modulo function calls)
    595 \item have individual `addresses'
    596 \end{itemize}
    597 }
    598 
    599 \frame{
    600 \frametitle{RTLabs structured traces}
    601 Have already established the existence of these traces
    602 \begin{itemize}
    603 \item termination decided classically
    604 \item syntactic labelling properties used to build the semantic structure
    605 \item show stack preservation to ensure that function calls \texttt{return}
    606   to the correct location
    607 \item tricky to establish guardedness of definitions
    608 \end{itemize}
    609 
    610 \bigskip
    611 Next, prove that flattening these traces yields the original.
    612 }
    613 
    614 \frame{
    615 \frametitle{Conclusion}
    616 
    617 The syntax, semantics and translations of the prototype compiler have
    618 been implemented in Matita.
    619 
    620 \bigskip
    621 We have already defined and established
    622 \begin{itemize}
    623 \item invariants regarding variables, typing and program structure
    624 \item a rich form of execution trace to pass to the back-end
    625 \end{itemize}
    626 
    627 \medskip
    628 We have plans for
    629 \begin{itemize}
    630 \item showing functional correctness of the front-end
    631 \item proving that the cost labelling is appropriate, and is preserved
    632 \item using the above in the whole compiler functional and cost correctness results.
    633 \end{itemize}
    634 
    635 }
    636 
    637636\end{document}
Note: See TracChangeset for help on using the changeset viewer.