# Changeset 3358 for Papers

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

...

Location:
Papers/itp-2013
Files:
2 edited

### Legend:

Unmodified
 r3357 Let's consider a generic unstructured language already equipped with a small step structured operational semantics (SOS). We introduce a deterministic labelled transition system~\cite{LTS} $(S,\Lambda,\to)$ deterministic labelled transition system $(S,\Lambda,\to)$ that refines the SOS by observing function calls/returns and the beginning of basic blocks. We achieve this by independently proving the three properties for each compiler pass. 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. The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this. First a relation between the corresponding source and target states is defined. Then a lemma establishes