M. Sig-ager, D. Biernacki, O. Danvy, and J. Midtgaard, A functional correspondence between evaluators and abstract machines, Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp.27-29

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pp.418-430, 2011.

O. Danvy and K. Millikin, Refunctionalization at work, Science of Computer Programming Special Issue on Mathematics of Program Construction, vol.74, issue.8, pp.534-549, 2006.
DOI : 10.1007/11783596_2

O. Danvy and L. R. Nielsen, Defunctionalization at work, Proceedings of the 3rd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP '01, pp.162-174, 2001.
DOI : 10.7146/brics.v8i23.21684
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.8417

O. Danvy and L. R. Nielsen, Syntactic Theories in Practice, Electronic Notes in Theoretical Computer Science, vol.59, issue.4, pp.358-374, 2001.
DOI : 10.1016/S1571-0661(04)00297-X
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.6276

J. Filliâtre, La supériorité de l'ordre supérieur, Journées Francophones des Langages Applicatifs, pp.15-26, 2002.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

J. Filliâtre and M. Pereira, Itérer avec confiance, Vingt-septièmes Journées Francophones des Langages Applicatifs, 2016.

J. Filliâtre and M. Pereira, A Modular Way to Reason About Iteration, 8th NASA Formal Methods Symposium, 2016.
DOI : 10.1007/978-3-319-40648-0_24

G. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

J. Kanig, Spécification et preuve de programmes d'ordre supérieur, Thèse de doctorat, 2010.

J. Kanig and J. Filliâtre, Who, Proceedings of the 2009 ACM SIGPLAN workshop on ML, ML '09, 2009.
DOI : 10.1145/1596627.1596634
URL : https://hal.archives-ouvertes.fr/hal-00777585

Y. Koda and F. Ruskey, A Gray Code for the Ideals of a Forest Poset, Journal of Algorithms, vol.15, issue.2, pp.324-340, 1993.
DOI : 10.1006/jagm.1993.1044

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot : Reasoning with the awkward squad, Proceedings of ICFP'08, 2008.

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1
URL : http://doi.org/10.1016/0304-3975(75)90017-1

F. Pottier and N. Gauthier, Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, pp.125-162, 2006.
DOI : 10.1007/s10990-006-8611-7

Y. Régis-gianas and F. Pottier, A Hoare Logic for Call-by-Value Functional Programs, Proceedings of the Ninth International Conference on Mathematics of Program Construction (MPC'08), pp.305-335, 2008.
DOI : 10.1007/978-3-540-70594-9_17

C. John and . Reynolds, Definitional interpreters for higher-order programming languages, Higher- Order and Symbolic Computation, pp.363-397, 1998.