@book(Aho:2006:CPT:1177220,
 author       = {Alfred V. Aho and Monica S. Lam and Ravi Sethi and Jeffrey D. Ullman},
 year         = {2006},
 title        = {Compilers: Principles, Techniques, and Tools (2Nd Edition)},
 publisher    = {Addison-Wesley Longman Publishing Co., Inc.},
 address      = {Boston, MA, USA},
)
@inproceedings(clochard:hal-01094488,
 author       = {Martin Clochard and L{\'e}on Gondelman},
 year         = {2015},
 title        = {{Double WP : Vers une preuve automatique d'un compilateur}},
 booktitle    = {{Journ{\'e}es Francophones des Langages Applicatifs}},
 address      = {Val d'Ajol, France},
 pages        = {1--18},
 url          = {https://hal.inria.fr/hal-01094488},
)
@misc(register,
 author       = {Filli\IeC{\^a}tre, Jean-Christophe and Martin Clochard},
 year         = {2013},
 title        = {{A tiny register allocator for tree expressions}},
 howpublished = {\url{http://toccata.lri.fr/gallery/register\_allocation.en.html}},
 note         = {Online; accessed May 15th 2018},
)
@article(DBLP:journals/entcs/GlesnerFJ05,
 author       = {Sabine Glesner and Simone Forster and Matthias J{\"{a}}ger},
 year         = {2005},
 title        = {A Program Result Checker for the Lexical Analysis of the {GNU} {C} Compiler},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {132},
 number       = {1},
 pages        = {19--35},
 doi          = {10.1016/j.entcs.2005.01.029},
)
@misc(doublewp,
 author       = {L\IeC{\'e}on Gondelman and Martin Clochard},
 year         = {2013},
 title        = {{Double WP}},
 howpublished = {\url{http://toccata.lri.fr/gallery/double\_wp.en.html}},
 note         = {Online; accessed May 15th 2018},
)
@book(citeulike:14362116,
 author       = {Jason Hickey and Anil Madhavapeddy and Yaron Minsky},
 year         = {2014},
 title        = {{Real World OCaml}},
 publisher    = {"O'Reilly Media, Inc."},
 url          = {http://www.worldcat.org/isbn/144932391},
)
@misc(why3,
 author       = {Inria},
 year         = {2013},
 title        = {{Why3 - Home}},
 howpublished = {\url{http://why3.lri.fr/}},
 note         = {Online; accessed May 15th 2018},
)
@article(Leroy-Compcert-CACM,
 author       = {Xavier Leroy},
 year         = {2009},
 title        = {Formal verification of a realistic compiler},
 journal      = {Communications of the ACM},
 volume       = {52},
 number       = {7},
 pages        = {107--115},
 doi          = {10.1145/1538788.1538814},
 url          = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
)
@inproceedings(ZhaoNMZ12,
 author       = {Jianzhou Zhao and Santosh Nagarakatte and Milo M. K. Martin and Steve Zdancewic},
 year         = {2012},
 title        = {Formalizing the LLVM intermediate representation for verified program transformations.},
 editor       = {John Field and Michael Hicks},
 booktitle    = {POPL},
 publisher    = {ACM},
 pages        = {427--440},
 doi          = {10.1145/2103656.2103709},
 url          = {http://dblp.uni-trier.de/db/conf/popl/popl2012.html#ZhaoNMZ12},
)