A. Bibliography, G. Assaf, R. Burel, D. Cauderlier, G. Delahaye et al., Dedukti: a Logical Framework based on the ??-Calculus Modulo Theory, 2016.

[. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus Modulo as a Universal Proof Language, the Second International Workshop on Proof Exchange for Theorem Proving, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

[. Blanqui, Definitions by rewriting in the calculus of constructions, 16th Annual IEEE Symposium on Logic in Computer Science Proceedings, pp.9-18, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00105568

[. Boespflug, Design and implementation of a proof verifying kernel for the ??-calculus modulo. Theses, Ecole Polytechnique X, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00672699

[. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications , 8th International Conference Proceedings, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

[. Dowek, Models and termination of proof reduction in the lambda pi-calculus modulo theory, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, pp.1-10914, 2017.

P. Hyvernat, The Size-Change Termination Principle for Constructor Based Languages. 19 pages + 3 pages d'appendice, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00547440

D. Neil, N. Jones, and . Bohr, Call-by-value termination in the untyped lambda-calculus, Logical Methods in Computer Science, vol.4, issue.1, 2008.

[. Lee, N. D. Jones, M. Amir, and . Ben-amram, The sizechange principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '01, pp.81-92, 2001.
DOI : 10.1145/373243.360210
URL : ftp://ftp.diku.dk/diku/semantics/papers/D-429.ps.gz

R. Lepigre and C. Raffalli, Subtyping-based typechecking for system f with induction and coinduction. arXiv preprint, 2016.

F. Vincent-van-oostrom and . Van-raamsdonk, Weak orthogonality implies confluence: The higher order case, Proceedings of the Third International Symposium on Logical Foundations of Computer Science, LFCS '94, pp.379-392, 1994.

R. Saillard, Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi- Calcul Modulo : théorie et pratique), 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

[. Wahlstedt, Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion, 2007.