Changeset 3358


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

...

Location:
Papers/itp-2013
Files:
2 edited

Legend:

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

    r2635 r3358  
    468468
    469469
     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
    470477@techreport{EDI-INF-RR-1412,
    471478  author = {Brian Campbell and Randy Pollack},
  • 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.