A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti: a logical framework based on the ??-calculus modulo theory, 2016.

J. M. Almendros-jiménez and G. Vidal, Automatic partial inversion of inductively sequential functions, Implementations and Applications of Functional Languages, vol.4449, pp.253-270, 2007.

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

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization in the algebraic-?-cube, Journal of Functional Porgramming, vol.7, issue.6, pp.613-660, 1997.

D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-pi-calculus modulo, LNCS, vol.4583, pp.102-117, 2007.

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation, vol.1, pp.253-281, 1991.

N. Nishida, M. Sakai, and T. Sakabe, Partial inversion of constructor term rewriting systems, Term Rewriting and Applications, vol.3467, pp.264-278, 2005.

R. Saillard, Type checking in the lambda-Pi-calculus modulo: theory and practice, 2015.