@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"
}