Kuroda's Translation for the λΠ-Calculus Modulo Theory and Dedukti

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations.Recently, Brown and Rizkallah extended this translation to higher-order logic.In this paper, we adapt it for theories encoded in higher-order logic in the λ Π-calculus modulo theory, a logical framework that extends λ -calculus with dependent types and user-defined rewrite rules.We develop a tool that implements Kuroda's translation for proofs written in DEDUKTI, a proof language based on the λ Π-calculus modulo theory.