Version longue et mise a jour du papier sur le front-end (premier jet).

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1033 insertions, 0 deletions

diff --git a/papers/cfrontend_new/blazy.bib b/papers/cfrontend_new/blazy.bib
new file mode 100755
index 00000000..d51242c0
--- /dev/null
+++ b/papers/cfrontend_new/blazy.bib
@@ -0,0 +1,1033 @@
+@String{CSM = {Proc. of the Conf. on Soft. Maintenance (CSM)}}
+@String{PLDI = {Proc. of the Programming Languages Design and Implementation Conf. (PLDI)}}
+@String{POPL = {Proc. of Principles Of Progamming Languages symposium (POPL)}}
+@String{LNCS = {Lecture Notes in Computer Science}}
+@String{TOPLAS = {ACM Transactions on Programing Languages and Systems}}
+@String{SV = {Springer-Verlag}}
+@String{JUCS = "Journal of Universal Computer Science"}
+
+@Book{B:book,
+	AUTHOR = "J.R. Abrial",
+	TITLE = "The B-Book assigning programs to meanings",
+	PUBLISHER="Cambridge University Press",
+	YEAR = "1996"}
+
+@Book{compil:book,
+	AUTHOR = "A.V. Aho and R.Sethi and J.D.Ullman",
+	TITLE = "Compilers: Principles, Techniques and Tools",
+	PUBLISHER="Addison-Wesley",
+	YEAR = "1988"}
+
+@phdthesis{C:andersen,
+	AUTHOR = "L.O. Andersen",
+	TITLE = "Program analysis and specialization for the C programming language",
+	YEAR="1994",
+	SCHOOL="University of Copenhagen", NOTE="DIKU report 94/19"}
+
+@InProceedings{ppc:appel,
+  author = 	 {A.W. Appel},
+  title = 	 {Foundational Proof-Carrying Code},
+  booktitle = {16th Annual IEEE Symp. on Logic in Computer Science (LICS)},
+  year = 	 {2001},
+  month = 	 {June},
+ address = {Washington, DC, United States},
+ pages = {247}
+}
+
+@INPROCEEDINGS{pepm:glueck,
+	AUTHOR="R. Baier and R. Gl{\"u}ck and R. Z{\"o}chling",
+	TITLE="Partial evaluation of numerical programs in {F}ortran",
+	PAGES="119-132",
+	BOOKTITLE = "Proc. of the Partial Evaluation and semantics based Program Manipulation Workshop",
+	ORGANIZATION="ACM SIGPLAN",
+	ADDRESS="Melbourne", YEAR="1994"}
+
+@ARTICLE{slicing:berg,
+	AUTHOR="J.A. Bergstra and T.B. Dinesh and J. Field and J. Heering",
+	TITLE="Toward a complete transformational toolkit for compilers",
+	PAGES="639-684",
+	JOURNAL = TOPLAS,
+	VOLUME="19", NUMBER="5",
+	MONTH = "September", YEAR="1997"}
+
+@Book{CoqArt,
+  author = 	 "Y. Bertot and P. Castéran",
+  title = 	 {Interactive Theorem Proving and Program Development
+Coq'Art: The Calculus of Inductive Constructions},
+  publisher = 	 {Springer Verlag},
+  year = 	 {2004},
+}
+
+@TechReport{bertot:compilo,
+  author = 	 {Y. Bertot},
+  title = 	 {A certified compiler for an imperative langage},
+  institution =  {INRIA},
+  year = 	 {1998},
+  number = 	 {RR-3488}
+}
+
+@inproceedings{coq:bertot95,
+    author = "Y. Bertot and R. Fraer",
+    title = "Reasoning with Executable Specifications",
+    booktitle = "{TAPSOFT '95}: Theory and Practice of Software Development",
+    series = LNCS, volume = "915",
+    publisher = "Springer-Verlag",
+    editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach",
+    pages = "531--45",
+    ADDRESS = "Aarhus", MONTH = "May", year = "1995"}
+
+@PhdThesis{these:sb,
+  author = 	 {S.Blazy},
+  title = 	 {La spécialisation de programmes pour l'aide à la maintenance du logiciel},
+  school = 	 {CNAM},
+  year = 	 {1993},
+  month = 	 {December}
+}
+
+@INPROCEEDINGS{washington:sb,
+	AUTHOR = "S. Blazy and P. Facon",
+	TITLE = "{SFAC}, a tool for program comprehension by specialization",
+	BOOKTITLE = "Proc. of the Third Workshop on Program Comprehension",
+	ORGANIZATION = "IEEE",
+	PAGES = "162-167",
+	ADDRESS = "Washington D.C.", MONTH = "November", YEAR = {1994}	}
+
+@INPROCEEDINGS{tapsoft:sb,
+	AUTHOR = "S. Blazy and P. Facon",
+	TITLE = "Formal specification and prototyping of a program specializer",
+	BOOKTITLE = "{TAPSOFT '95}: Theory and Practice of Software Development",
+	PAGES = "666-680",
+	SERIES = LNCS, VOLUME = "915",
+        publisher = "Springer-Verlag",
+        editor = "P. D. Mosses and M. Nielsen and M. I. Schwartzbach",
+	ADDRESS = "Aarhus", MONTH = "May", YEAR = {1995}	}
+
+@INPROCEEDINGS{pe1996:sb,
+	AUTHOR = "S. Blazy and P. Facon",
+	TITLE = "An automatic interprocedural analysis for the understanding of scientific application
+	Programs",
+	PAGES = "1-16",
+	crossref={pe1996:tout}	}
+
+@ARTICLE{sope:sb,
+	AUTHOR = "S. Blazy and P. Facon",
+	TITLE = "Partial evaluation for program understanding",
+        crossref={sope:tout} }
+
+@INPROCEEDINGS{ase:sb,
+	AUTHOR = "S. Blazy and P. Facon",
+	TITLE = "Application of formal methods to the development of a software maintenance tool",
+	BOOKTITLE = "Proc. of the Automated Software Engineering Conference",
+	PAGES = "162-171",
+	ORGANIZATION = "IEEE",
+	MONTH = "November", YEAR = {1997}	}
+
+@article{sekejal:sb,
+	AUTHOR = "S. Blazy",
+	TITLE = "Partial Evaluation for the understanding of {F}ortran programs",
+	journal = "Journal of Software Engineering and Knowledge Engineering",
+	VOLUME = "4", NUMBER = "4",
+	PAGES = "535-559",
+	YEAR = {1994}	}
+
+@article{asejal:sb,
+	AUTHOR = "S. Blazy",
+	TITLE = "Specifying and Automatically Generating a Specialization Tool for {F}ortran 90",
+	journal = "Journal of Automated Software Engineering",
+	VOLUME = "7", NUMBER = "4",
+	PAGES = "345-376",
+	MONTH = "December", YEAR = {2000}	}
+
+@techreport{cedric02:sb,
+  title = "Transformations certifiées de programmes impératifs",
+  author = "S. Blazy",
+  type = "Technical report",
+  institution = "CEDRIC",
+  number = "398",
+  month = "December",
+  year = "2002",
+}
+
+@INPROCEEDINGS{icfem:sb,
+	AUTHOR = "S. Blazy and X. Leroy",
+	TITLE = "Formal verification of a memory model for
+                         {C}-like imperative languages",
+	BOOKTITLE = "Proc. of Int. Conf. on Formal Engineering Methods {ICFEM}",
+	PAGES =  {280--299},
+	SERIES = LNCS, VOLUME = 3785 ,
+        publisher = "Springer-Verlag",
+	ADDRESS = "Manchester, UK", 
+        MONTH = "November", 
+        YEAR = {2005}
+}
+ 
+@inproceedings{blazy06:fm,
+  author    = {Sandrine Blazy and Zaynah Dargaye and
+               Xavier Leroy},
+  title     = {Formal Verification of a {C} Compiler Front-End},
+  booktitle = {Symp. on Formal Methods (FM'06)},
+   SERIES = {Lecture Notes in Computer Science},
+  VOLUME = 4805,
+  year      = {2006},
+  pages     = {460-475},
+  ee        = {http://dx.doi.org/10.1007/11813040_31}}
+
+
+@InProceedings{table:ob,
+        author = {O. Boite and C. Dubois},
+        title = {Proving {T}ype {S}oundness of a {S}imply {T}yped {ML}-like {L}anguage with {R}eferences},
+        year = 2001,
+        Booktitle = {Supplemental Proc. of TPHOL'01, Informatics
+                     Research Report EDI-INF-RR-0046 of University of Edinburgh},
+        Editor = {R. Boulton and P. Jackson},
+        pages = {69--84}
+}
+
+@INPROCEEDINGS{coq:dataflow,
+  AUTHOR = {D. Cachera and T. Jensen and D. Pichardie and V. Rusu},
+  TITLE = {{Extracting a Data Flow Analyser in Constructive Logic}},
+  BOOKTITLE = {Proc.\ of 13th European Symp. on Programming (ESOP'04)},
+  YEAR = {2004},
+  PAGES = {385--400},
+  NUMBER = {2986},
+  SERIES = LNCS,
+  PUBLISHER = SV}
+}
+
+@INPROCEEDINGS{pldi:carini,
+	AUTHOR = "R. Carini and M. Hind",
+	TITLE = "Flow-sensitive interprocedural constant propagation",
+	BOOKTITLE = PLDI,
+	ORGANIZATION="ACM SIGPLAN",
+	PAGES = "23-31",
+	ADDRESS = "La Jolla",
+	MONTH = "June", YEAR = {1995}	}
+
+@misc{cavalcanti-procedures,
+  author = "Ana Cavalcanti and Augusto Sampaio and Jim Woodcock",
+  title = "Procedures, Parameters, And Substitution In The Refinement Calculus",
+  url = "citeseer.nj.nec.com/cavalcanti97procedures.html" }
+
+@MANUAL{Centaur,
+	TITLE = "Centaur 1.2 documentation",
+	ORGANIZATION = "INRIA",
+	YEAR = "1994"	}
+
+@Misc{Coq,
+  title = 	 {The {C}oq proof assistant},
+  note = "http://coq.inria.fr"
+}
+
+@INPROCEEDINGS{pldi:chase,
+	AUTHOR = "D.R. Chase and F.K. Zadeck",
+	TITLE = "Analysis of pointers and structures",
+	BOOKTITLE = PLDI,
+	ORGANIZATION="ACM SIGPLAN",
+	PAGES = "296-31",
+	ADDRESS = "White Plains",
+	MONTH = "June", YEAR = {1990}	}
+
+@PhdThesis{chrzaszcz04phd,
+  author = 	 {J. Chrz{\k a}szcz},
+  title = 	 {Modules in Type Theory with Generative Definitions},
+  school = 	 {Warsaw Univerity and University of Paris-Sud},
+  year = 	 2004,
+  month =	 {January}
+}
+
+@article{pe:conselproof,
+    author = "C. Consel and S.-C. Khoo",
+    title = "On-Line  Off-Line Partial Evaluation: Semantic Specifications and Correctness Proofs",
+    journal = "Journal of Functional Programming",
+    volume = "5",
+    number = "4",
+    pages = "461-500",
+    year = "1995" }
+
+@InProceedings{pe:tutorial,
+  author = 	 {C.Consel and O.Danvy},
+  title = 	 {Tutorial notes on partial evaluation},
+  booktitle = POPL,
+  pages = 	 {493-501},
+  year = 	 {1993},
+}
+
+@InProceedings{coq:courtieu,
+  author = {P. Courtieu},
+  title =  {Normalized types},
+  booktitle = {CSL},
+  year = 	 {2001},
+}
+
+@INPROCEEDINGS{preuve:despeyroux,
+	AUTHOR = "J. Despeyroux",
+	TITLE = "Proof of translation in natural semantics",
+	BOOKTITLE = "Proc. of the Symposium on Logic in Computer Science",
+	ADDRESS = "Cambridge, USA",
+	MONTH = "June", YEAR = {1986}	}
+
+@mastersthesis{stage:pointeurs,
+	AUTHOR = "N. Dubois and P. Sayarath",
+	TITLE = "Aide {\`{a}} la {compr\'{e}hension} et {\`{a}} la maintenance:
+	pointeurs pour la {sp\'{e}cialisation} de programmes",
+	MONTH = "June", YEAR="1996",
+	SCHOOL="IIE-CNAM", NOTE="in French"}
+
+@INPROCEEDINGS{pldi:emami,
+	AUTHOR = "M. Emami and R. Ghiya and L.J. Hendren",
+	TITLE = "Context-sensitive interprocedural points-to analysis in the presence of function pointers",
+	BOOKTITLE = PLDI,
+	ORGANIZATION="ACM SIGPLAN",
+	PAGES = "242-256",
+	MONTH = "June", YEAR = {1994}	}
+
+@techreport {cite110,
+  title = "Modelling program compilation in the refinement calculus",
+  author = "C. J. Fidge",
+  type = "Technical report",
+  institution = "Software Verification Research Centre",
+  address = "School of Information Technology,
+   The University of Queensland, Brisbane 4072. Australia",
+  number = "97-22",
+  month = may,
+  year = "1997",
+  keywords = "refinement, compilers.",
+  abstract = "This report shows how compilation of high-level language 
+programs to assembler code can be formally represented in the 
+refinement calculus. New operators are introduced to widen the 
+modelling language to encompass assembler code. A compilation 
+strategy is then embodied as a set of derived refinement rules.",
+  url = "http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-22"
+}
+
+@INPROCEEDINGS{slicing:field,
+	AUTHOR = "J. Field and G. Ramalingam and F. Tip",
+	TITLE = "Parametric program slicing",
+	BOOKTITLE = POPL,
+	ADDRESS = "San Francisco, USA",
+        PAGES = "379-392",
+	YEAR = {1995}	}
+
+@InProceedings{fsets,
+  author = 	  {J.-C. Filli{\^a}tre and P. Letouzey},
+  title = 	 {Functors for Proofs and Programs},
+  booktitle =  {{European Symposium on Programing, (ESOP)}},
+  volume = 2986,
+  publisher =    {Springer-Verlag},
+  series =       LNCS, 
+  year = 	 {2004},
+  address = 	 {Barcelona, Spain},
+  month = 	 {April},
+}
+
+@INPROCEEDINGS{caduceus,
+  AUTHOR = {J.-C. Filli\^atre and C. March\'e},
+  TITLE = {{Multi-Prover Verification of C Programs}},
+  BOOKTITLE = {6th Int. Conf. on  Formal Engineering Methods (ICFEM)},
+  YEAR = 2004,
+  ADDRESS = {Seattle},
+  MONTH = {November},
+  PUBLISHER = SV,
+  SERIES = LNCS,
+  VOLUME = 3308,
+  PAGES = {15--29}
+}
+
+@INCOLLECTION{frazer:reverse,
+        AUTHOR = "A. Frazer",
+        TITLE = "Reverse engineering",
+        BOOKTITLE = "Software reuse and reverse engineering in practice",
+        PUBLISHER = "P.A.V. Hall",
+        YEAR = "1992",
+        PAGES = "209-243" }
+
+@ARTICLE{slicing:gallagher,
+	AUTHOR = "K. Gallagher and J.R. Lyle",
+	TITLE = "Using program slicing in software mainetnance",
+	JOURNAL = {ACM Trans. Soft. Eng.},
+	VOLUME = {17}, NUMBER = {8},
+        PAGES = "751-761",
+	YEAR = {1991}	}
+
+@Article{Glesner:2003,
+  author =     "S. Glesner",
+  title =      "{Using Program Checking to Ensure the Correctness of Compiler Implementations}",
+  journal =    JUCS,
+  year =       "2003",
+  volume =     "9",
+  number =     "3",
+  pages =      "191--222",
+  month =      {March}}
+
+@inproceedings{verifix,
+ author = {G. Goos and W. Zimmermann},
+ title = {Verification of Compilers},
+ booktitle = {Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel)},
+ year = {1999},
+ pages = {201--230},
+ publisher = SV,
+ address = {London, UK}
+ }
+
+@article{fpcc:coq,
+  author = {N. Hamid and Z. Shao and  V. Trifonov and S. Monnier and Z. Ni}, 
+  title = {A Syntactic Approach to Foundational Proof-Carrying Code}, 
+  journal= {Journal of Automated Reasoning}, 
+  volume = 31, 
+  number={3-4}, 
+  year= {2003}, 
+  month= {September},
+  pages= "191-229"
+}
+
+@ARTICLE{natsem:hannan,
+	AUTHOR="J. Hannan",
+	TITLE="Extended natural semantics",
+	PAGES="123-152",
+	JOURNAL = "Journal of functional programming",
+	VOLUME="3", NUMBER="2",
+	MONTH = "April", YEAR="1993"}
+
+@INPROCEEDINGS{pe:haraldsson,
+	AUTHOR = "A. Haraldsson",
+	TITLE = "A partial evaluator and its Use for compiling iterative statements in Lisp",
+	BOOKTITLE = POPL,
+	ADDRESS = "Tucson",
+	YEAR = {1978}	}
+
+@INPROCEEDINGS{pldi:horwitz,
+	AUTHOR = "R. Hasti and S. Horwitz",
+	TITLE = "Using static single assignment form to improve flow-insensitive pointer analysis",
+	BOOKTITLE = PLDI,
+	ORGANIZATION="ACM SIGPLAN",
+	PAGES = "97-105", 
+	ADDRESS = "Montreal",
+	MONTH = "June", YEAR = {1998}	}
+
+@inproceedings{pe:hatcliff95,
+    author = "J. Hatcliff",
+    title = "Mechanically Verifying the Correctness of an Offline Partial Evaluator",
+    booktitle = "Proc. of the 7th Int. Symp. on Programming Languages: Implementations, Logics and Programs",
+    month = "September",
+    series = LNCS, volume = "982",
+    publisher = "Springer-Verlag",
+    address = "Utrecht, The Netherlands",
+    editor = "M. Hermenegildo and S.D. Swierstra",
+    pages = "279--298",
+    year = "1995"}
+
+@article{hatcliff97computational,
+    author = "John Hatcliff and Olivier Danvy",
+    title = "A Computational Formalization for Partial Evaluation",
+    journal = "Mathematical Structures in Computer Science",
+    volume = "7",
+    number = "5",
+    pages = "507-541",
+    year = "1997"}
+
+
+@Article{hoare:verif,
+  author = 	 {T. Hoare},
+  title = 	 {The Verifying Compiler: a Grand Challenge for Computing Research},
+  journal = 	 {Journal of the ACM},
+  year = 	 {2003},
+  volume = 	 {50},
+  number = 	 {1},
+  pages = 	 {63-69},
+  month = 	 {January},
+}
+
+@article{jifeng93specification,
+    author = "{H. Jifeng} and J. P. Bowen",
+    title = "Specification, Verification and Prototyping of an Optimized Compiler",
+    journal = "Formal Aspects of Computing",
+    volume = "6",
+    number = "6",
+    pages = "643-658",
+    year = "1993" }
+
+@Book{VDM:book,
+	AUTHOR = "C.B. Jones",
+	TITLE = "Systematic development using VDM",
+	PUBLISHER="Prentice-Hall",
+	YEAR = "1990"}
+
+@Book{pe:book,
+	AUTHOR = "N.D. Jones and C.K. Gomard and P. Sestoft",
+	TITLE = "Partial evaluation and automatic program generation",
+	PUBLISHER="Prentice-Hall",
+	YEAR = "1993"}
+
+@inproceedings{natsem:kahn, 
+	AUTHOR = "G.Kahn",
+	booktitle = {{Proc. of the Symp. on Theoretical Aspects of Comp. Science}}, 
+	pages = {237-257}, 
+        publisher = "Springer-Verlag",
+	SERIES = LNCS, VOLUME = "247",
+	title = {{Natural Semantics}}, 
+	year = {1987} 
+} 
+
+@INPROCEEDINGS{pldi:landi,
+	AUTHOR = "W. Landi and B.G. Ryder",
+	TITLE = "A safe approximate algorithm for interprocedural pointer aliasing",
+	BOOKTITLE = PLDI,
+	PAGES = "235-248",
+	ORGANIZATION="ACM SIGPLAN",
+	MONTH = "June", YEAR = {1992}	}
+
+@inproceedings{lawall:sound,
+    author = "J. Lawall and P. Thiemann",
+    title = "Sound Specialization in the Presence of Computational Effects",
+    booktitle = "Theoretical Aspects of Computer Software",
+    series = LNCS, volume = "1281",
+    publisher = "Springer-Verlag",
+    pages = "165--190",
+    month = "September",
+    address = 	 {Sendai, Japan},
+    year = "1997"}
+
+@inproceedings{paul:sefm,
+    author= {D. Leinenbach and W. Paul and E. Petrova},
+    title= {Towards the Formal Verification of a {C}0 Compiler},
+    booktitle= {Proc. Conf. on Software Engineering and Formal Methods (SEFM)}, 
+    month={September},
+    year= 2005, 
+    address= {Koblenz, Germany}
+}
+
+@INPROCEEDINGS{rhodium:popl,
+	AUTHOR = "S.Lerner and T. Millstein and E. Rice and C. Chambers",
+	TITLE = "Automated soundness proofs for dataflow analyses and transformations",
+	BOOKTITLE = POPL,
+	ADDRESS = "Long Beach, United States",
+	YEAR = {2005}	}
+
+@InProceedings{xl:jfla,
+  author = 	 {X. Leroy},
+  title = 	 {Certification d'un Compilateur: Enjeux, Problèmes et Approches},
+  booktitle = {Journées Francophones des Langages Applicatifs (JFLA)},
+  year = 	 {2004},
+  month = 	 {January},
+  organization = {INRIA},
+  note = 	 {invited talk}
+}
+
+@InProceedings{xl:popl,
+  author = 	 {X. Leroy}, 
+  title = 	 {Formal certification of a compiler back-end, or: programming a compiler 
+                  with a proof assistant},
+  booktitle = POPL,
+  year = 	 {2006},
+  month = "January",
+  address = {Charleston, USA},
+  pages = "42--54",
+  publisher = "ACM Press"
+}
+
+@TechReport{xl:cminor,
+  author = 	 {X. Leroy},
+  title = 	 {Le langage Intermédiaire {C} minor},
+  institution =  {Concert technical report},
+  year = 	 {2003},
+  month = 	 {February},
+}
+
+@misc{xl:compcert-backend,
+  author =      {X. Leroy},
+  title =       {The {Compcert} certified compiler back-end --
+                 commented {Coq} development},
+  howpublished = {Available on-line at \citeurl{http://cristal.inria.fr/~xleroy/compcert-backend/}},
+  year =        {2006}
+}
+
+@INPROCEEDINGS{fse:liang,
+	AUTHOR = "D. Liang and M.J. Harrold",
+	TITLE = "Efficient points-to analysis for whole-program analysis",
+	BOOKTITLE = "Proc. of ESEC/FSE joint Conf.",
+	ADDRESS = "Toulouse, France",
+	PAGES = "199-215",
+	SERIES = LNCS, VOLUME = "1687",
+	ORGANIZATION="ACM SIGSOFT",
+	MONTH = "September", YEAR = {1999}	}
+
+@phdthesis{letouzey04,
+        author       = "P. Letouzey",
+        month        = "July",
+        school       = "Universit{\'e} Paris-Sud",
+        title        = "Programmation fonctionnelle certifi{\'e}e -- L'extraction de programmes dans l'assistant {Coq}",
+        year         = "2004"
+}
+
+@InProceedings{nipkow:pt,
+  author = 	 {F. Mehta and T. Nipkow},
+  title = 	 {Proving pointer programs in higher-order logic},
+  booktitle="Automated Deduction --- CADE-19",
+  editor="F. Baader",
+  year=2003,
+  publisher=SV,
+  series=LNCS, 
+  volume={2741},
+  pages={121--135}}
+
+}
+
+@InProceedings{seplog:ref,
+  author = 	 {I. Mijajlovic and N. Torp-Smith},
+  title = 	 {Refinement in Separation Context},
+  booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)},
+  year = 	 {2004},
+  address = 	 {Venice, Italy},
+  month = 	 {January},
+}
+
+@InProceedings{space:region,
+  author = 	 {S.Monnier},
+  title = 	 {Typed regions},
+  booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)},
+  year = 	 {2004},
+  address = 	 {Venice, Italy},
+  month = 	 {January},
+}
+
+@Book{muchnik:book,
+	AUTHOR = "S.S. Muchnick",
+	TITLE = "Advanced compiler-design and implementation",
+	PUBLISHER="Morgan Kaufmann",
+	YEAR = "1997"}
+
+
+
+@InProceedings{pcc:necula,
+  author = 	 {G. Necula},
+  title = 	 {Proof Carrying Code},
+  booktitle = POPL,
+  year = 	 {1997},
+  month = 	 {January},
+} 
+
+@InProceedings{tv:necula,
+  author =       "G. Necula",
+  title =        "Translation Validation for an Optimizing Compiler",
+  booktitle =      "{ACM} {SIG\-PLAN} Conf. on Programming Language
+                 Design and Implementation (PLDI)",
+  pages =        "83--95",
+  year =         "2000"
+}
+
+@inproceedings{russes:C,
+  author    = {V.A. Nepomniaschy and I.S. Anureev and A.V. Promsky},
+  title     = {Verification-Oriented Language {C}-Light and Its Structural
+               Operational Semantics.},
+  booktitle = {Ershov Memorial Conference},
+  year      = {2003},
+  pages     = {103-111},
+}
+
+@inproceedings{tv:pnueli,
+ author = {A. Pnueli and M. Siegel and E. Singerman},
+ title = {Translation Validation},
+ booktitle = {Proc. of the 4th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS)},
+ year = {1998},
+ pages = {151--166},
+ publisher = SV,
+ address = {London, UK}
+ }
+
+@inproceedings{cocv:pnueli,
+ author = {Y. Hu and C. Barrett and B. Goldberg and A. Pnueli},
+ title = {Validating More Loop Optimizations},
+ booktitle = {Workshop on Compiler Optimization Meets Compiler Verification (COCV)},
+ year = {2005},
+ address = {Edinburgh, UK}
+ }
+
+
+@Book{nielson:book,
+	AUTHOR = "H.R. Nielson and F. Nielson",
+	TITLE = "Semantics with application - A formal introduction",
+	PUBLISHER="John Wiley and Sons",
+	YEAR = "1992"}
+
+@Book{intabs:book,
+	AUTHOR = "F. Nielson and H.R. Nielson and C. Hankin",
+	TITLE = "Principles of Program Analysis",
+	PUBLISHER="Springer-Verlag",
+	YEAR = "1999"}
+
+@INPROCEEDINGS{ase:consel,
+	AUTHOR = "R. Marlet and S. Thibault and C. Consel",
+	TITLE = "Mapping software architectures to efficient implementation via partial evaluation",
+	BOOKTITLE = "Proc. of the Automated Software Engineering Conference",
+	PAGES = "183-192",
+	ORGANIZATION = "IEEE",
+	MONTH = "November", YEAR = {1997}	}
+
+@InProceedings{cil,
+  author = {G. Necula and S. McPeak and S.P. Rahul and W. Weimer},
+  title = {CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs},
+  booktitle = {Conf. on Compiler Construction (CC'02)},
+  address = {Grenoble, France},
+  year = 	 {2002},
+  month = 	 {March},
+}
+
+@article{borger:C,
+    author = "{E. B{\"o}rger} and N.G. Fruja and V.Gervasi and R.F. St{\"a}rk",
+    title = "A high-level modular definition of the semantics of {C\#}",
+    journal = "Theoretical Computer Science",
+    volume = "336",
+    number = "2-3",
+    pages = "235-284",
+    year = "2005" }
+
+@InProceedings{gurevich:C,
+   author = "Y. Gurevich and  J.K. Huggins", 
+   title = "The Semantics of the {C} Programming Language",
+   booktitle = "Proc. of CSL'92 (Computer Science Logic)", 
+   publisher = "Springer Verlag",
+   SERIES = LNCS, VOLUME = "702",
+   year = 1993, 
+   pages = "274-308",
+}
+
+@techreport{KleinN-Toplas,
+        author =        {Gerwin Klein and Tobias Nipkow},
+        title =         {A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
+        number =        {0400001T.1},
+        institution=    {National ICT Australia},
+        month=mar,
+        year=2004,
+        note =          "To appear in ACM TOPLAS"}
+}
+ 
+@PhdThesis{Norrish:phd,
+  author =       "M. Norrish",
+  title =        "{C} formalised in HOL",
+  school =       "University of Cambridge",
+  year =         1998,
+  month =        "December"
+}
+
+
+@misc{norvell94machine,
+  author = "T. Norvell",
+  title = "Machine code programs are predicates too",
+  text = "Theodore S. Norvell. Machine code programs are predicates too. In David
+    Till, editor, Sixth Refinement Workshop, Workshops in Computing, pages 188--204.
+    Springer Verlag, 1994.",
+  year = "1994"}
+
+@article{palsberg93correctness,
+    author = "J. Palsberg",
+    title = "Correctness of Binding-Time Analysis",
+    journal = "Journal of Functional Programming",
+    volume = "3",
+    number = "3",
+    pages = "347-363",
+    year = "1993"}
+ 
+@PhdThesis{papaspyrou-1998-fscpl,
+  author =       "N.S. Papaspyrou",
+  title =        "A formal semantics for the {C} programming language",
+  school =       "National Technical University of Athens",
+  year =         1998,
+  month =        "February"
+}
+
+@TechReport{strecker05:_compil_verif_c0,
+  author = 	 {Martin Strecker},
+  title = 	 {Compiler Verification for {C0}},
+  institution =  {Universit{\'e} Paul Sabatier},
+  year = 	 2005,
+  address =	 {Toulouse},
+  month =	 {April}
+}
+
+@inproceedings{rival:popl,
+ author = {X. Rival},
+ title = {Symbolic transfer function-based approaches to certified compilation},
+ booktitle = POPL,
+ year = {2004},
+ pages = {1--13},
+ location = {Venice, Italy},
+ publisher = {ACM Press},
+ }
+
+@manual{f90,
+	author = "S. Ramsden and F. Lin and M.A. Pettipher and G.S. Noland and J.M. Brooke",
+	title="{Fortran} 90: a conversion course for {F}ortran 77 programmers",
+	organization="Manchester and north {HC} {T\&EC}",
+	edition="Third",
+	year="1995"
+}
+
+@Misc{coq:renard,
+  author = 	 {C. Renard},
+  title = 	 {Un peu d'extensionnalité en {C}oq},
+  note = 	 {Université Paris VI},
+  year = 	 {2001},
+  howpublished = {Mémoire de DEA},
+  month = 	 {September}
+}
+
+@INPROCEEDINGS{rinard:compil,
+	AUTHOR ="M. Rinard and D. Marinov",
+        TITLE = "Credible compilation with pointers",
+        BOOKTITLE = "Workshop on Run-Time Result Verification (RTRV)", 
+         address = {Trento, Italy}, 
+        MONTH = "July",
+        YEAR = {1999} }
+
+@manual{f90:norme,
+	title="Programming language {Fortran 90}",
+	organization="ANSI",
+	address="New York",
+	year="1992",
+	note="ANSI X3.198-1992 and ISO/IEC 1539-1991(E)"
+}
+
+@INPROCEEDINGS{ptr:sagiv,
+	AUTHOR = "M. Sagiv and T. Reps and R. Wilhelm",
+	TITLE = "Solving shape-analysis problems in languages with destructive updating",
+	BOOKTITLE = POPL,
+	MONTH = "January", YEAR = {1997}	}
+
+
+
+@Book{sampaio:compil,
+  author = 	 {A.Sampaio},
+  title = 	 {An algebraic approach to compiler design},
+  publisher = 	 {World Scientific},
+  year = 	 {1997},
+  volume = 	 {4},
+  OPTnumber = 	 {},
+  series = 	 {AMAST series in computing},
+  OPTaddress = 	 {},
+  OPTedition = 	 {},
+  OPTmonth = 	 {},
+  OPTnote = 	 {},
+  OPTannote = 	 {}
+}
+
+@inproceedings{mem:crf,
+ author = {X. Shen and  Arvind and L. Rudolph},
+ title = {Commit-reconcile \& fences ({CRF}): a new memory model for architects and compiler writers},
+ booktitle = {ISCA '99: Proc. of the 26th symposium on Computer architecture},
+ year = {1999},
+ pages = {150--161},
+ location = {Atlanta, Georgia, United States},
+ address = {Washington, DC, United States},
+ }
+
+@INPROCEEDINGS{ptr:steens,
+	AUTHOR = "B. Steensgaard",
+	TITLE = "Points-to analysis in almost linear time",
+	BOOKTITLE = POPL,
+	PAGES = "32-41",
+	YEAR = {1996}	}
+
+@inproceedings{coq:terrasse,
+    author = "D. Terrasse",
+    title = "Encoding Natural Semantics in {Coq}",
+    booktitle = "Proc. of the 4th Conf. on Algebraic Methodology and Software Technology",
+    publisher = SV, 
+    SERIES = LNCS, VOLUME = "936",
+    address = "Montreal, Canada",
+    editor = "V. S. Alagar",
+    pages = "230--244",
+    year = "1995" }
+
+@mastersthesis{stage:vassallo,
+	AUTHOR = "R. Vassallo",
+	TITLE = "Ergonomie et {\'{e}volution} d'un outil de {compr\'{e}hension} de programmes",
+	MONTH = "June", YEAR="1996",
+	SCHOOL="IIE-CNAM", NOTE="in French"}
+
+@Article{Wand93,
+  author = 	"M. Wand",
+  title = 	"Specifying the Correctness of Binding-Time Analysis",
+  journal = 	"Journal of Functional Programming",
+  year = 	"1993",
+  volume = 	"3",
+  number = 	"3",
+  pages = 	"365--387",
+  month = 	"July"}
+
+@INPROCEEDINGS{pldi:wilson,
+	AUTHOR = "R.P. Wilson and M.S. Lam",
+	TITLE = "Efficient context-sensitive pointer analysis for C programs",
+	BOOKTITLE = PLDI,
+	PAGES = "1-12",
+	ORGANIZATION="ACM SIGPLAN",
+	MONTH = "June", YEAR = {1995}	}
+
+@Book{formal:winskel,
+	AUTHOR = "G. Winskel",
+	TITLE = "The formal semantics of programming languages - an introduction",
+	PUBLISHER="MIT Press",
+	YEAR = "1993"}
+
+@INPROCEEDINGS{alias:ryder,
+	AUTHOR = "S. Zhang and B. Ryder and W. Landi",
+	TITLE = "Program decomposition for pointer aliasing: a step toward practical analyses",
+        BOOKTITLE = "Proc. of the Symp. on Foundations of Soft. Eng.",
+	ADDRESS = "San Francisco", 
+	MONTH = "October", YEAR = "1996",
+	PAGES = "81-92" }
+
+@PROCEEDINGS{pe1996:tout,
+	editor = "O. Danvy and R. Gl{\"u}ck and P. Thiemann",
+	TITLE = "International seminar on partial evaluation",
+	ADDRESS = "Dagstuhl castle",
+	SERIES = LNCS, VOLUME = "1110",
+	publisher = SV,
+	MONTH = "February", YEAR = {1996}	}
+
+@proceedings{sope:tout,
+	TITLE = "Symposium on partial evaluation",
+	SERIES = "ACM Computing Surveys", 
+	ORGANIZATION = "ACM",
+	NUMBER = "4",
+	MONTH = "December", YEAR = {1998}	}
+
+@TechReport{outil:2,
+  	author      = {M.G.J. van den Brand and P. Klint and C. Verhoef},
+  	title       = {{R}everse engineering and system renovation: an annotated bibliography},
+  	institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup},
+  	number      = {P9603},
+ 	year        = {1996},
+ 	fileurl     = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/P9603.ps.Z},
+ 	 abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1996/abstracts/P9603.txt},
+}
+                 
+@TechReport{P9702,
+  author      = {M.G.J. van den Brand and M.P.A. Sellink and C. Verhoef},
+  title       = {{R}eengineering {COBOL} {S}oftware {I}mplies {S}pecification of the
+                {U}nderlying {D}ialects},
+  institution = {{U}niversity of {A}msterdam, {P}rogramming {R}esearch {G}roup},
+  number      = {P9702},
+  year        = {1997},
+  fileurl     = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/P9702.ps.Z},
+  abstracturl = {http://ftp.wins.uva.nl/pub/programming-research/reports/1997/abstracts/P9702.txt},
+  note        = {Available by anonymous ftp from ftp.wins.uva.nl,
+                 file pub/programming-research/reports/1997/P9702.ps.Z}
+}
+
+@INPROCEEDINGS{outil:3,
+  	author      = {M.P.A. Sellink and C. Verhoef},
+  	title       = {Scaffolding for Software Renovation},
+	BOOKTITLE = CSM,
+	ORGANIZATION = "IEEE",
+	ADDRESS = "Z{\"u}rich", MONTH = "March", YEAR = "2000",
+}
+
+@INPROCEEDINGS{outil:4,
+  	author      = {H. Yank and P. Luker and W.Chu},
+  	title       = {Code understanding through program transformation for reusable component identification},
+	BOOKTITLE = "Fifth Workshop on Program Comprehension Proceedings",
+	ORGANIZATION = "IEEE",
+	YEAR = "1997",
+}
+
+@INPROCEEDINGS{outil:1,
+  	author      = {I. Baxter and A. Yahin and L. Moura and M. Sant'Anna and L. Bier},
+  	title       = {Clone detection using abstract syntax trees},
+	BOOKTITLE = CSM,
+	ORGANIZATION = "IEEE",
+	YEAR = "1998",
+}
+
+@article{mem:sota,
+	AUTHOR = "R.D. Tennent and D.R. Ghica and ",
+	TITLE = "Abstract models of storage",
+    journal = "Higher-Order and Symbolic Computation",
+    volume = "13",
+    number = "1/2",
+	MONTH = "", YEAR = "2000",
+	PAGES = "119-129" }
+ 
+
+
+@INPROCEEDINGS{mem:bornat,
+	AUTHOR = "R. Bornat",
+	TITLE = "Proving pointer programs in {H}oare logic",
+        BOOKTITLE = "5th Conf. on Mathematics of Program Construction",
+        publisher = SV, 
+	MONTH = "", YEAR = "2000",
+	PAGES = "102-126" }
+
+@PROCEEDINGS{space:tout,
+	TITLE = "Second workshop on semantics, program analysis, and computing environments for memory management",
+	ADDRESS = "Venice",
+	ORGANIZATION="ACM SIGPLAN",
+	MONTH = "January", YEAR = {2004}	}
+
+@InProceedings{typebin:popl,
+  author = 	 {Z. Shao and B.Saha and V. Trifonov and N. Papaspyrou},
+  title = 	 {A type system for certified binaries},
+  booktitle = POPL,
+  year = 	 {2002},
+  address = 	 {Portland, United States},
+  month = 	 {January},
+  pages = "217-232"
+}
+
+@InProceedings{shao:cac,
+  author = 	 {D.Yu and Z. Shao},
+  title = 	 {Verification of safety properties for concurrent assembly code},
+  booktitle = {Int. Conf. on Functional Programming (ICFP)},
+  year = 	 {2004},
+  address = 	 {Snowbird, United States},
+  month = 	 {September},
+  pages = "175-188"
+}
+
+  @InProceedings{walker:space,
+  author = 	 {D. Walker},
+  title = 	 {Stacks, heaps and regions: one logic to bind them},
+  year = 	 {2004},
+booktitle = {Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE)},
+  note = 	 {invited talk},
+  address = 	 {Venice, Italy},
+  month = 	 {January},
+}
+
+
+
+@InProceedings{mem:watson,
+  author   = {G.Watson},
+  title    = {Compilation of refinement for a practical language},
+  booktitle     = {Proc. of the 5th Int. Conf. on Formal Engineering Methods (ICFEM)},
+  crossref = {icfem2003}
+}
+
+@Misc{concert,
+  title = 	 {ARC Concert},
+  note = {http://www-sop.inria.fr/lemme/concert},
+}
+
+
+@proceedings{icfem2003,
+  editor    = {J. S. Dong and J. Woodcock},
+  title     = {Proc. of the 5th Int. Conf. on Formal Engineering Methods, ICFEM 2003},
+  publisher = SV,
+  series    = LNCS,
+  volume    = {2885},
+  address   = {Singapore},
+  year      = {2003},
+  month     = {November}
+}
+
+@article{dave:survey,
+        author = {Maulik A. Dave},
+        title = {Compiler verification: a bibliography},
+        journal = {SIGSOFT Softw. Eng. Notes},
+        volume = {28},
+        number = {6},
+        year = {2003},
+        pages = {2--2},
+        urlpublisher = {http://doi.acm.org/10.1145/966221.966235},
+        publisher = "ACM Press"
+}
+