R. Milner, Communication and Concurrency, 1990.

R. Milner, Communicating and Mobile Systems: the pi-Calculus, 1999.

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093

B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich, Engineering formal metatheory, 35th symposium Principles of Programming Languages, pp.3-15, 2008.
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948

A. W. Appel and D. A. Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems, vol.23, issue.5, pp.657-683, 2001.
DOI : 10.1145/504709.504712

N. A. Danielsson, Operational semantics using the partiality monad, International Conference on Functional Programming 2012, pp.127-138, 2012.

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, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symposium Principles of Programming Languages, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM 2006: Int. Symp. on Formal Methods, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

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

A. W. Appel and S. Blazy, Separation Logic for Small-Step cminor, Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs, pp.5-21, 2007.
DOI : 10.1007/978-3-540-74591-4_3
URL : https://hal.archives-ouvertes.fr/inria-00165915

M. Felleisen and D. P. Friedman, Control operators, the SECD machine and the ?calculus In: Formal Description of Programming Concepts III, pp.131-141, 1986.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

P. L. Curien and G. Munch-maccagnoni, The Duality of Computation under Focus, Theoretical Computer Science -6th IFIP International Conference, TCS 2010 of IFIP Advances in Information and Communication Technology, pp.165-181, 2010.
DOI : 10.1007/978-3-642-15240-5_13
URL : https://hal.archives-ouvertes.fr/hal-01054461

N. Benton and C. K. Hur, Biorthogonality, step-indexing and compiler correctness, International Conference on Functional Programming, pp.97-108, 2009.
DOI : 10.1145/1596550.1596567
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.146.2953