S. Blazy and X. Leroy, Mechanized semantics for the Clight subset of the C language, Journal of Automated Reasoning, vol.43, pp.263-288, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., A Trusted Mechanised JavaScript Specification, Proc. of the 41st ACM Symposium on Principles of Programming Languages, pp.87-100, 2014.
DOI : 10.1145/2535838.2535876

URL : https://hal.archives-ouvertes.fr/hal-00910135

M. Bodin, T. Jensen, and A. Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Proc. of the 2015 ACM Conference on Certified Programs and Proofs (CPP'15), pp.29-40, 2015.
DOI : 10.1145/2676724.2693174

URL : https://hal.archives-ouvertes.fr/hal-01111588