Changeset 3358

Timestamp:

Jun 14, 2013, 4:43:46 PM (8 years ago)

Author:

sacerdot

Message:

...

Location:

Papers/itp-2013

Files:

• ccexec.bib (modified) (1 diff)
• ccexec2.tex (modified) (2 diffs)

Papers/itp-2013/ccexec.bib

@@ -468 +468 @@
 
 
+@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

@@ -697 +697 @@
 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.
@@ -856 +856 @@
 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