Kuroda's Translation for the $\lambda\Pi$-Calculus Modulo Theory and Dedukti
<|reference_start|>Kuroda's Translation for the $\lambda\Pi$-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 lambdaPi-calculus modulo theory, a logical framework that extends lambda-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 lambdaPi-calculus modulo theory.<|reference_end|>
@article{traversié2024kuroda's,
    title={Kuroda's Translation for the $\lambda\Pi$-Calculus Modulo Theory and
  Dedukti},
    author={Thomas Traversi'e (MICS, CentraleSup'elec, Universit'e
  Paris-Saclay)},
    journal={EPTCS 404, 2024, pp. 35-48},
    year={2024},
    doi={10.4204/EPTCS.404.3},
    archivePrefix={arXiv},
    eprint={2407.06626},
    primaryClass={cs.LO}
}