A. W. Appel, Compiling with continuations, 1992.
DOI : 10.1017/CBO9780511609619

A. Balaa and Y. Bertot, Fonctions récursives générales par itération en théorie des types, Journées Francophones des Langages Applicatifs, pp.27-42, 2002.

G. Barthe, J. Forest, D. Pichardie, and V. Rusu, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Proc. 8th Int. Symp. on Functional and Logic Programming (FLOPS'06), pp.114-129, 2006.
DOI : 10.1007/11737414_9

URL : https://hal.archives-ouvertes.fr/inria-00564237

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, Types for Proofs and Programs, pp.66-81, 2004.
DOI : 10.1007/11617990_5

URL : https://hal.archives-ouvertes.fr/inria-00289549

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

J. C. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X

J. C. Filliâtre, The Why software verification tool. Software and documentation available at http://why.lri, 2003.

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

X. Leroy, D. Doligez, J. Garrigue, and J. Vouillon, The Objective Caml system. Software and documentation available at http://caml.inria.fr, 1996.

P. Letouzey, A New Extraction for Coq, Lecture Notes in Computer Science, vol.2646, pp.200-219, 2002.
DOI : 10.1007/3-540-39185-1_12

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

C. May, The parallel assignment problem redefined, IEEE Transactions on Software Engineering, vol.15, issue.6, pp.821-824, 1989.
DOI : 10.1109/32.24735

R. Sethi, A note on implementing parallel assignment instructions, Information Processing Letters, vol.2, issue.4, pp.91-95, 1973.
DOI : 10.1016/0020-0190(73)90024-0

P. H. Welch, Parallel assignment revisited. Software Practice and Experience, pp.1175-1180, 1983.
DOI : 10.1002/spe.4380131208