A. Balaa and Y. Bertot, Fix-Point Equations for Well-Founded Recursion in Type Theory, Proceedings of TPHOLs'00, pp.1-16, 2000.
DOI : 10.1007/3-540-44659-1_1

G. Barthe and P. Courtieu, Efficient Reasoning about Executable Specifications in Coq, Proceedings of TPHOLs'02, pp.31-46, 2002.
DOI : 10.1007/3-540-45685-6_4

G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo et al., A Formal Executable Semantics of the JavaCard Platform, Proceedings of ESOP'01, pp.302-319, 2001.
DOI : 10.1007/3-540-45309-1_20

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

S. Berghofer and T. Nipkow, Executing Higher Order Logic, Proceedings of TYPES'00, pp.24-40, 2002.
DOI : 10.1007/3-540-45842-5_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.1332

Y. Bertot, V. Capretta, and K. Das-barman, Type-Theoretic Functional Semantics, Proceedings of TPHOLs'02, pp.83-98, 2002.
DOI : 10.1007/3-540-45685-6_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.8750

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

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

A. Bove and V. Capretta, Modelling general recursion in type theory, Mathematical Structures in Computer Science, vol.15, issue.4, pp.671-708, 2005.
DOI : 10.1017/S0960129505004822

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00564633

D. Cachera and D. Pichardie, Embedding of Systems of Affine Recurrence Equations in Coq, Proceedings ofTPHOLs'03, number 2758 in Lecture Notes in Computer Science, pp.155-170, 2003.
DOI : 10.1007/10930755_10

V. Capretta, General recursion via coinductive types, Logical Methods in Computer Science, vol.1, issue.2, pp.1-18, 2005.
DOI : 10.2168/LMCS-1(2:1)2005
URL : http://arxiv.org/abs/cs/0505037

P. Dybjer, Abstract, The Journal of Symbolic Logic, vol.49, issue.02, pp.525-549, 2000.
DOI : 10.1017/CBO9780511569807.011

M. J. Gordon and T. F. Melham, Introduction to HOL: A theorem proving environment for higher-order logic, 1993.

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Proceedings of TPHOLs'05, pp.98-113, 2005.
DOI : 10.1007/11541868_7

M. Katsushige, N. Kiyoshi, and K. Hitoshi, Pipelined LMS Adaptative Filter Using a New Look-Ahead Transformation, IEEE Transactions on Circuits and Systems, vol.46, pp.51-55, 1999.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Proceedings of POPL'06, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

C. Mcbride and J. Mckinna, The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004.
DOI : 10.1017/S0956796803004829

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.
DOI : 10.1007/3-540-45949-9

B. Nordström, Terminating general recursion, BIT, vol.24, issue.3, pp.605-619, 1988.
DOI : 10.1007/BF01941137

C. Project, N. Shankar, S. Owre, and J. M. Rushby, The PVS Proof Checker: A Reference Manual, 1993.

K. Slind, Reasoning about Terminating Functional Programs, 1999.

H. Xi, Dependent types for program termination verification. Higher-Order and Symbolic Computation, pp.91-131, 2002.