# Changeset 3358

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

...

Location:
Papers/itp-2013
Files:
2 edited

Unmodified
Added
Removed
• ## Papers/itp-2013/ccexec.bib

 r2635 @misc{fopara, author = {R.~M. Amadio and N.~Ayache and F.~Bobot and J.~P. Boender and B.~Campbell and I.~Garnier and A.~Madet and J.~McKinna and D.~P. Mulligan and M.~Piccolo and R.~Pollack and Y.~R\'egis-Gianas and C.~Sacerdoti Coen and I.~Stark and P.~Tranquilli}, title = {Certified Complexity (CerCo)}, note = {Submitted to FOPARA 2013}, year = 2013 } @techreport{EDI-INF-RR-1412, author = {Brian Campbell and Randy Pollack},
• ## Papers/itp-2013/ccexec2.tex

 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
Note: See TracChangeset for help on using the changeset viewer.