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, 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) of Lecture Notes in Computer Science, 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.

Y. Bertot, B. Grégoire, and X. Leroy, A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis, of Lecture Notes in Computer Science, 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 frontend, of Lecture Notes in Computer Science, pp.460-475, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00106401

J. 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. Filliâtre, The Why software verification tool'. Software and documentation available at http, 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

P. Letouzey, A New Extraction for Coq, of Lecture Notes in Computer Science, 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