#References ##0 dummy

##1 U. Berger, S. Berghofer, P. Letouzey, and H. Schwichtenberg. Program extraction from normalization proofs. Studia Logica, 82, 2005. Special issue.

##2 L. Cruz-Filipe and P. Letouzey. A Large-Scale Experiment in Executing Extracted Programs. In 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus’2005, 2005.

##3 J.-C. Filliâtre and P. Letouzey. Functors for Proofs and Programs. In D. Schmidt, editor, European Symposium on Programing, ESOP’2004, volume 2986 of Lecture Notes in Computer Science. Springer-Verlag, 2004.

##4 D. Pichardie G. Barthe, J. Forest and V. Rusu. Dening and reasoning about recursive functions: a practical tool for the coq proof assistant. In FLOPS’06, volume 3945 of LNCS, 2006.

##5 O. Lee and K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):707 723, July 1998.

##6 Xavier Leroy. Formal certication of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages, pages 4254. ACM Press, 2006.

##7 P. Letouzey. A New Extraction for Coq. In H. Geuvers and F. Wiedijk, editors, TYPES 2002, volume 2646 of LNCS. Springer-Verlag, 2003.

##8 P. Letouzey. Programmation fonctionnelle certiée L’extraction de programmes dans l’assistant Coq. PhD thesis, Université Paris-Sud, July 2004. see http: //

##9 C. Parent. Synthèse de preuves de programmes dans le Calcul des Constructions Inductives. thèse d’université, École Normale Supérieure de Lyon, January 1995.

##10 M. Sozeau. Program-ing Finger Trees in Coq. In ICFP’07, pages 1324. ACM Press, 2007.