Index: /Papers/itp-2013/ccexec.bib
===================================================================
--- /Papers/itp-2013/ccexec.bib (revision 3357)
+++ /Papers/itp-2013/ccexec.bib (revision 3358)
@@ -468,4 +468,11 @@
+@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},
Index: /Papers/itp-2013/ccexec2.tex
===================================================================
--- /Papers/itp-2013/ccexec2.tex (revision 3357)
+++ /Papers/itp-2013/ccexec2.tex (revision 3358)
@@ -697,5 +697,5 @@
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,5 +856,5 @@
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