A. Charguéraud, Characteristic Formulae for Mechanized Program Verification, 2010.

P. Cousot and R. Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.83-94, 1992.
DOI : 10.1145/143165.143184

P. Cousot and R. Cousot, Bi-inductive structural semantics: (extended abstract) Electronic Notes Theoretical Computer Sciences, pp.29-44, 2007.

P. Cousot and R. Cousot, Bi-inductive structural semantics. Information and Computation, pp.258-283, 2009.
DOI : 10.1016/j.ic.2008.03.025
URL : http://doi.org/10.1016/j.ic.2008.03.025

N. Anders-danielsson, Operational semantics using the partiality monad, ICFP, pp.127-138, 2012.

A. Carl, D. Gunter, and . Rémy, A proof-theoretic assessment of runtime type errors, 1993.

G. Kahn, Natural semantics, Symposium on Theoretical Aspects of Computer Science (STACS), pp.22-39, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

X. Leroy, Coinductive big-step operational semantics, European Symposium on Programming (ESOP), pp.54-68, 2006.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

X. Leroy and H. Grall, Coinductive big-step operational semantics. CoRR, 2008.
DOI : 10.1016/j.ic.2007.12.004
URL : https://hal.archives-ouvertes.fr/inria-00309010

K. Nakata and T. Uustalu, Trace-Based Coinductive Operational Semantics for While, TPHOLs, pp.375-390, 2009.
DOI : 10.1051/ita:1999125

G. D. Plotkin, A structural approach to operational semantics, 1981.

K. Andrew, M. Wright, and . Felleisen, A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.