A Curry-Howard-De Bruijn Isomorphism Modulo. Under submission

The rewriting calculus combines in a unified setting the frameworks and capabilities of rewriting and -calculus. Its most general typed version, called Pure Pattern Type Systems (P 2TS) and adapted from Barendregt’s -cube, is especially interesting from a logical point of view. We show how to use a subset of P 2TS as a proof-term language for natural deduction modulo, extending the Curry-Howard-De Bruijn isomorphism for this class of log-ical formalisms. The pattern matching featured in the cal-culus allows us to model any congruence given by a term rewriting system. We characterize how proofs can be denoted by P 2TS terms and we discuss the interest of our proof-term lan-guage for the issue of cut elimination. Finally, we explore some relations between our proof-term language and other formalisms: extraction of -terms and/or rewrite rules from P 2TS-terms, but also automated generation of proof-terms by a rewriting-based language.