Changeset 3358
- Timestamp:
- Jun 14, 2013, 4:43:46 PM (8 years ago)
- Location:
- Papers/itp-2013
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/itp-2013/ccexec.bib
r2635 r3358 468 468 469 469 470 @misc{fopara, 471 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}, 472 title = {Certified Complexity (CerCo)}, 473 note = {Submitted to FOPARA 2013}, 474 year = 2013 475 } 476 470 477 @techreport{EDI-INF-RR-1412, 471 478 author = {Brian Campbell and Randy Pollack}, -
Papers/itp-2013/ccexec2.tex
r3357 r3358 697 697 Let's consider a generic unstructured language already equipped with a 698 698 small step structured operational semantics (SOS). We introduce a 699 deterministic labelled transition system ~\cite{LTS}$(S,\Lambda,\to)$699 deterministic labelled transition system $(S,\Lambda,\to)$ 700 700 that refines the 701 701 SOS by observing function calls/returns and the beginning of basic blocks. … … 856 856 We achieve this by independently proving the three properties for each compiler 857 857 pass. 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.858 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. 859 859 First a relation between the corresponding 860 860 source and target states is defined. Then a lemma establishes
Note: See TracChangeset
for help on using the changeset viewer.