Dedukti: a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory

Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7

Dedukti is a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…