R. Bagnara, P. M. Hill, A. Pescetti, and E. Zaffanella, Verification of C programs via natural semantics and abstract interpretation The Netherlands, Proc. of the IFM 2007 C/C++ Verification Workshop, Technical Report ICIS- R07015, Institute for Computing and Information Sciences (iCIS), pp.75-80, 2007.

M. Bodin, T. Jensen, and A. Schmitt, Pretty-big-step-semantics-based certified abstract interpretation (preliminary version) In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, of Electronic Proceedings in Theoretical Computer Science, pp.360-383, 2013.

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., A trusted mechanised javascript specification, POPL, pp.87-100, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00910135

M. Bodin, T. Jensen, and A. Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, 2015.
DOI : 10.1145/2676724.2693174
URL : https://hal.archives-ouvertes.fr/hal-01111588

D. Cachera and D. Pichardie, A Certified Denotational Abstract Interpreter, In ITP, pp.9-24, 2010.
DOI : 10.1007/978-3-642-14052-5_3
URL : https://hal.archives-ouvertes.fr/inria-00537810

D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theor. Comput. Sci, pp.56-78, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00564633

A. Charguéraud, Pretty-Big-Step Semantics, ESOP, pp.41-60, 2013.
DOI : 10.1007/978-3-642-37036-6_3

P. Cousot, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

V. Gouranton and D. L. Métayer, Dynamic slicing: a generic analysis based on a natural semantics format, Journal of Logic and Computation, vol.9, issue.6, 1999.
DOI : 10.1093/logcom/9.6.835
URL : https://hal.archives-ouvertes.fr/hal-00137413

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, pp.583-626, 2003.
DOI : 10.1016/S0304-3975(02)00869-1

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

X. Leroy and H. Grall, Coinductive big-step operational semantics, Information and Computation, vol.207, issue.2, pp.284-304, 2009.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

C. Mcbride, Elimination with a motive In Types for proofs and programs, pp.197-216, 2002.

J. Midtgaard and T. Jensen, A calculational approach to controlflow analysis by abstract interpretation, SAS, pp.347-362, 2008.

J. Midtgaard and T. Jensen, Control-flow analysis of function calls and returns by abstract interpretation, ICFP, pp.287-298, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00758152

D. Park, Fixpoint induction and proofs of program properties, Machine Intelligence 5, pp.59-78, 1969.

D. Pichardie, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, FICS, pp.225-239, 2008.
DOI : 10.1016/j.entcs.2008.04.064
URL : https://hal.archives-ouvertes.fr/inria-00332365

C. B. Poulsen and P. D. Mosses, Deriving Pretty-Big-Step Semantics from Small-Step Semantics, Programming Languages and Systems, pp.270-289, 2014.
DOI : 10.1007/978-3-642-54833-8_15

D. A. Schmidt, Natural-semantics-based abstract interpretation (preliminary version), SAS, pp.1-18, 1995.
DOI : 10.1007/3-540-60360-3_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.73.5172

D. A. Schmidt, Abstract interpretation of small-step semantics, Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple- Agent Languages, pp.76-99, 1997.
DOI : 10.1007/3-540-62503-8_4

D. Van-horn and M. Might, Abstracting abstract machines, ICFP, pp.51-62, 2010.