Dedukti: a logical framework based on the ??-calculus modulo theory, 2016. ,
Automatic partial inversion of inductively sequential functions, Implementations and Applications of Functional Languages, vol.4449, pp.253-270, 2007. ,
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
Modularity of strong normalization in the algebraic-?-cube, Journal of Functional Porgramming, vol.7, issue.6, pp.613-660, 1997. ,
Embedding pure type systems in the lambda-pi-calculus modulo, LNCS, vol.4583, pp.102-117, 2007. ,
A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation, vol.1, pp.253-281, 1991. ,
Partial inversion of constructor term rewriting systems, Term Rewriting and Applications, vol.3467, pp.264-278, 2005. ,
Type checking in the lambda-Pi-calculus modulo: theory and practice, 2015. ,