X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

A. Barthwal and M. Norrish, Verified, Executable Parsing, European Symposium on Programming, pp.160-174, 2009.
DOI : 10.1007/978-3-642-00590-9_12
URL : http://hdl.handle.net/1885/57413

A. Barthwal, A formalisation of the theory of context-free languages in higher order logic, 2010.

F. L. Deremer, Simple LR(k) grammars, Communications of the ACM, vol.14, issue.7, pp.453-460, 1971.
DOI : 10.1145/362619.362625

T. Anderson, J. Eve, and J. J. Horning, EfficientLR (1) parsers, Acta Informatica, vol.9, issue.1, pp.12-39, 1973.
DOI : 10.1007/BF00571461

D. Pager, A practical general method for constructing LR(k) parsers, Acta Informatica, vol.20, issue.3, pp.249-268, 1977.
DOI : 10.1007/BF00290336

D. E. Knuth, On the translation of languages from left to right, Information and Control, vol.8, issue.6, pp.607-639, 1965.
DOI : 10.1016/S0019-9958(65)90426-2

F. Pottier and Y. Régis-gianas, The Menhir parser generator http://gallium. inria.fr

J. H. Jourdan, F. Pottier, and X. Leroy, Coq code for validating LR(1) parsers http

J. C. Filliâtre and P. Letouzey, Functors for Proofs and Programs, European Symposium on Programming, pp.370-384, 2004.
DOI : 10.1007/978-3-540-24725-8_26

I. Iec, Programming languages ? C (2007) International standard ISO, IEC, vol.9899, p.3

Y. Padioleau, Parsing C/C++ Code without Pre-processing, Lecture Notes in Computer Science, vol.5501, pp.109-125, 2009.
DOI : 10.1007/978-3-642-00722-4_9

F. Pottier and Y. Régis-gianas, Towards Efficient, Typed LR Parsers, Electronic Notes in Theoretical Computer Science, vol.148, issue.2, pp.155-180, 2006.
DOI : 10.1016/j.entcs.2005.11.044
URL : https://hal.archives-ouvertes.fr/inria-00629090

B. Ford, Packrat parsing: simple, powerful, lazy, linear time, ACM International Conference on Functional Programming (ICFP), pp.36-47, 2002.

B. Ford, Parsing expression grammars: a recognition-based syntactic foundation, ACM Symposium on Principles of Programming Languages (POPL), pp.111-122, 2004.

A. Warth, J. R. Douglass, and T. D. Millstein, Packrat parsers can support left recursion, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation , PEPM '08, pp.103-110, 2008.
DOI : 10.1145/1328408.1328424

A. Koprowski and H. Binsztok, TRX: A formally verified parser interpreter, Logical Methods in Computer Science, vol.7, issue.2, 2011.

R. Wisnesky, G. Malecha, and G. Morrisett, Certified web services in Ynot In: Workshop on Automated Specification and Verification of Web Systems, 2009.

H. Samet, Automatically Proving the Correctness of Translations Involving Optimized Code, 1975.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Lecture Notes in Computer Science, vol.1384, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

G. C. Necula, Translation validation for an optimizing compiler, ACM Conference on Programming Language Design and Implementation (PLDI), pp.83-95, 2000.

J. B. Tristan and X. Leroy, A simple, verified validator for software pipelining, ACM Symposium on Principles of Programming Languages (POPL), pp.83-92, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00529836

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

A. V. Aho and J. D. Ullman, The theory of parsing, translation, and compiling, 1972.

M. Sozeau, Program-ing finger trees in Coq, ACM International Conference on Functional Programming (ICFP), pp.13-24, 2007.