Lambdapi is an implementation of the λΠ-calculus modulo rewriting.
The λΠ-calculus is also known as λP or LF. In the λΠ-calculus modulo rewriting, the conversion typing rule includes user rewriting rules defining function and predicate symbols.
-
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory, Ali Assaf, Guillaume Burel, Raphaël Cauderlier , David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Draft, 2016.
-
Typechecking in the λΠ-Calculus Modulo: Theory and Practice, Ronan Saillard. PhD thesis, 2015.
-
Definitions by rewriting in the Calculus of Constructions, Frédéric Blanqui, in Mathematical Structures in Computer Science 15(1):37-92.
-
More papers can be found here.