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
, Handbook of Logic in Computer Science, vol.2, 1992.
Auto-validation d'un système de preuves avec familles inductives, 1999. ,
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
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