A. Abel, Semi-continuous sized types and termination. Logical Methods in Com-814 puter Science, vol.4, p.3, 2008.
DOI : 10.1007/11874683_5
URL : http://arxiv.org/pdf/0804.0876v1.pdf

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, The Matita 817 interactive theorem prover, Nikolaj Bjørner and Viorica Sofronie-Stokkermans, p.818
DOI : 10.1007/978-3-642-22438-6_7

, Automated Deduction -CADE-23, pp.64-69, 2011.

G. Barthe, B. Grégoire, and F. Pastawski, Cic?: type-based termination 821 of recursive definitions in the calculus of inductive constructions, Logic for Programming, p.822

, 13th International Conference, LPAR 2006, p.823

C. Penh, Proceedings, pp.257-271, 2006.

. Jasmin-christian, J. Blanchette, A. Hölzl, L. Lochbihler, and . Panny, Andrei, vol.826

D. Popescu and . Traytel, Truly modular (co)datatypes for isabelle/hol, p.827

R. Klein and . Gamboa, Interactive Theorem Proving, pp.93-110, 2014.

L. De-moura, S. Kong, J. Avigad, F. Van-doorn, and J. V. Raumer,

, In Amy P. Felty and Aart Middeldorp, edi-831 tors, Automated Deduction -CADE-25, pp.378-388, 2015.

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: fast, p.834

?. Embeddable and . Interpreter, Proceedings of LPAR, 2015.

C. Keller and M. Lasson, Parametricity in an Impredicative Sort, CSL -26th International Workshop/21st Annual Conference of 838 the EACSL -2012, vol.16, pp.381-395, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730913

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, vol.842
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

, Interactive Theorem, p.843

. Proving, , pp.19-34, 2013.

A. Mahboubi and E. Tassi, Mathematical Components. draft, pp.1-183, 2018.

C. Mcbride, H. Goguen, and J. Mckinna, A few constructions on constructors

, Types 847 for Proofs and Programs, pp.186-200, 2006.

D. Miller, Abstract syntax for variable binders: An overview, p.849

U. Dahl, M. Furbach, K. Kerber, C. Lau, and . Palamidessi, Luís Moniz, vol.850

Y. Pereira, P. J. Sagiv, and . Stuckey, Computational Logic -CL 2000, vol.851, pp.239-253, 2000.

D. Miller and G. Nadathur, Programming with Higher-Order Logic. Cambridge Uni-853 versity Press, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant 855 for Higher-order Logic, 2002.

U. Norell, Towards a practical programming language based on dependent type theory, p.858

, SE-412 96 Göteborg, 2007.

J. L. Sacchini, On type-based termination and dependent pattern matching in the calculus 860 of inductive constructions. Theses, École Nationale Supérieure des Mines de Paris, vol.861, 2011.

T. Sheard and S. , Template meta-programming for haskell, SIGPLAN 863 Not, vol.37, issue.12, p.864, 2002.

M. Sozeau and N. Oury, First-class type classes, Proceedings of the 21st In-866 ternational Conference on Theorem Proving in Higher Order Logics, TPHOLs '08, vol.867, pp.978-981, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

E. Tassi, Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi ?Prolog 870 dialect). CoqPL, 2018.

, The Coq Development Team. The coq proof assistant, version 8.8.0, 2018.

D. Traytel, A. Popescu, and J. C. Blanchette, Foundational, compositional 874 (co)datatypes for higher-order logic: Category theory applied to theorem proving, Pro-875 ceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, p.876

, LICS '12, pp.596-605, 2012.

P. Wadler, Theorems for free! In Proceedings of the Fourth International Conference 879 on Functional Programming Languages and Computer Architecture, FPCA '89, vol.359, p.881, 1989.