A. Assaf, A framework for defining computational higher-order logics. (Un cadre de définition de logiques calculatoires d'ordre supérieur), 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

H. P. Barendregt, Handbook of Logic in Computer Science, vol.2, 1992.

B. Barras, Auto-validation d'un système de preuves avec familles inductives, 1999.

T. Coquand and &. Hugo-herbelin, A -Translation and Looping Combinators in Pure Type Systems, J. Funct. Program, vol.4, issue.1, pp.77-88, 1994.
URL : https://hal.archives-ouvertes.fr/inria-00159085

V. Siles, Investigation on the typing of equality in type systems. (Etude sur le typage de l'égalité dans les systèmes de types), 2010.
URL : https://hal.archives-ouvertes.fr/pastel-00556578