Kuroda's Translation for the -Calculus Modulo Theory and Dedukti
arXiv:2407.06626 · doi:10.4204/EPTCS.404.3
Abstract
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.
In Proceedings LFMTP 2024, arXiv:2407.05822