Ignore:
Timestamp:
Jun 14, 2013, 4:43:46 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec2.tex

    r3357 r3358  
    697697Let's consider a generic unstructured language already equipped with a
    698698small step structured operational semantics (SOS). We introduce a
    699 deterministic labelled transition system~\cite{LTS} $(S,\Lambda,\to)$
     699deterministic labelled transition system $(S,\Lambda,\to)$
    700700that refines the
    701701SOS by observing function calls/returns and the beginning of basic blocks.
     
    856856We achieve this by independently proving the three properties for each compiler
    857857pass.
    858 The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert}) that runs like this.
     858The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this.
    859859First a relation between the corresponding
    860860source and target states is defined. Then a lemma establishes
Note: See TracChangeset for help on using the changeset viewer.