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.
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.
URL : https://hal.archives-ouvertes.fr/hal-01111588

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, pp.56-78, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00564633

A. Charguéraud, Pretty-big-step Semantics, European Symposium on Programming (ESOP'13). Springer LNCS, vol.7792, pp.41-60, 2013.

M. Churchill, D. Peter, N. Mosses, P. Sculthorpe, and . Torrini, Reusable Components of Semantic Specifications, Transactions on Aspect-Oriented Software Development XII, pp.132-179, 2015.

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: A unified lattice model for static analysis of programs by construction of approximations of fixpoints, Proc. of 4th ACM Symposium on Principles of Programming Languages (POPL '77), pp.238-252, 1977.

A. ?tef?nescu, D. Park, S. Yuwen, Y. Li, and G. Ro?u, Semantics-Based Program Verifiers for All Languages, Proc. of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'16), pp.74-91, 2016.

T. Dinsdale-young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang, Views: Compositional Reasoning for Concurrent Programs, Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13), pp.287-300, 2013.

E. , Language Specification (ECMA-262, 2018.

P. Gardner, S. Maffeis, and G. Smith, Towards a Program Logic for JavaScript, ACM SIGPLAN Notices, vol.47, pp.31-44, 2012.

R. Harper, F. Honsell, and G. D. Plotkin, A Framework for Defining Logics, Proc. of the Symposium on Logic in Computer Science (LICS '87, pp.194-204, 1987.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A Formally-Verified C Static Analyzer, Proc. of the 42nd ACM Symposium on Principles of Programming Languages (POPL '15), pp.247-259, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01078386

R. Jung, R. Krebbers, and J. Jourdan, Ale? Bizjak, Lars Birkedal, and Derek Dreyer. 2017. Iris from the Ground Up, 2017.

S. Keidel, C. Bach-poulsen, and S. Erdweg, Compositional Soundness Proofs of Abstract Interpreters, Proc. ACM Program. Lang. 2, ICFP, Article 72, vol.26, 2018.
DOI : 10.1145/3236767
URL : http://dl.acm.org/ft_gateway.cfm?id=3236767&type=pdf

G. Klein and T. Nipkow, Verified Bytecode Verifiers, Theoretical Computer Science, vol.298, pp.583-626, 2002.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: a verified implementation of ML, Proc. of 41st Annual ACM Symposium on Principles of Programming Languages, POPL '14, pp.179-192, 2014.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Proc/ of 33rd ACM Symposium on Principles of Programming Languages (POPL'06), pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

L. Li and E. L. Gunter, IsaK: A Complete Semantics of K, 2018.
DOI : 10.1007/978-3-030-02146-7_10

S. Maffeis, J. C. Mitchell, and A. Taly, An Operational Semantics for JavaScript, Proc. of APLAS'08, vol.5356, pp.307-325, 2008.
DOI : 10.1007/978-3-540-89330-1_22
URL : http://www.doc.ic.ac.uk/~maffeis/aplas08.pdf

J. Midtgaard and T. Jensen, A Calculational Approach to Control-Flow Analysis by Abstract Interpretation, Proc. of 15th Static Analysis Symposium (SAS'08). Springer LNCS, vol.5079, pp.347-362, 2008.
DOI : 10.1007/978-3-540-69166-2_23

D. Peter, Mosses. 1992. Action Semantics

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, Lem: Reusable Engineering of Real-world Semantics, Proc. of the 19th ACM SIGPLAN International Conference on Functional Programming, 2014.

F. Nielson, R. Hanne, C. Nielson, and . Hankin, Principles of Program Analysis, 1999.
DOI : 10.1007/978-3-662-03811-6
URL : http://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec11-AbstractInt.pdf

M. Norrish, C formalised in HOL, 1998.

S. Owens, A Sound Semantics for OCamllight, Proc. of 17th European Symposium on Programming, vol.4960, pp.1-15, 2008.

, Proc. ACM Program. Lang, vol.3, p.31, 2019.

J. Palsberg, Closure Analysis in Constraint Form, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.17, pp.47-62, 1995.
DOI : 10.1145/200994.201001

F. Pfenning and C. Schürmann, System Description: Twelf-A Meta-Logical Framework for Deductive Systems, Proc. of 16th International Conference on Automated Deduction, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

G. Plotkin, A Structural Approach to Operational Semantics, 1981.

G. Ro?u, Matching Logic, Logical Methods in Computer Science, vol.13, pp.1-61, 2017.

G. Ro?u-and-traian-florin and . ?erb?nu??, An Overview of the K Semantic Framework, Journal of Logic and Algebraic Programming, vol.79, pp.397-434, 2010.

A. David and . Schmidt, Natural-semantics-based Abstract Interpretation (preliminary version), Proc. of 3rd Static Analysis Symposium (SAS'95). Springer LNCS, vol.983, pp.1-18, 1995.

D. A. Schmidt, Abstract Interpretation in the Operational Semantics Hierarchy, BRICS Report Series, vol.4, 1997.

D. A. Schmidt, Abstract Interpretation of Small-Step Semantics, Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages. Springer LNCS, vol.1192, pp.76-99, 1997.

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott: Effective Tool Support for the Working Semanticist, Journal of Functional Programming, vol.20, pp.71-122, 2010.

D. Turi and G. Plotkin, Towards a Mathematical Operational Semantics, Proc. of 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), pp.280-291, 1997.

T. Uustalu, Coinductive Big-Step Semantics for Concurrency, Proceedings 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2013, vol.137, pp.63-78, 2013.

D. Van-horn and M. Might, Abstracting Abstract Machines, Proc. of ACM 2010 Int. Conf. on Functional Programming (ICFP'10), pp.51-62, 2010.

D. Van-horn and M. Might, Abstracting Abstract Machines: A Systematic Approach to Higher-order Program Analysis, Commun. ACM, vol.54, pp.101-109, 2011.