https://hal.inria.fr/inria-00198543Burel, GuillaumeGuillaumeBurelPAREO - Formal islands: foundations and applications - INRIA Lorraine - Inria - Institut National de Recherche en Informatique et en Automatique - LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications - Inria - Institut National de Recherche en Informatique et en Automatique - UHP - Université Henri Poincaré - Nancy 1 - Université Nancy 2 - INPL - Institut National Polytechnique de Lorraine - CNRS - Centre National de la Recherche ScientifiqueA First-Order Representation of Pure Type Systems Using SuperdeductionHAL CCSD2008deduction modulofirst-order logiclambda-calculus with explicit substitutionsnatural deduction vs. sequent calculuslogical frameworks[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]Burel, GuillaumeFrank Pfenning2007-12-17 15:23:432023-03-24 14:52:492007-12-17 15:51:09enConference papershttps://hal.inria.fr/inria-00198543/document10.1109/LICS.2008.22application/pdf1Superdeduction is a formalism closely related to deduction modulo which permits to enrich a deduction system (especially a first-order one such as natural deduction or sequent calculus) with new inference rules automatically computed from the presentation of a theory. We give a natural encoding from every functional Pure Type System (PTS) into superdeduction by defining an appropriate first-order theory. We prove that this translation is correct and conservative, showing a correspondence between valid typing judgments in the PTS and provable sequents in the corresponding superdeductive system. As a byproduct, we also introduce the superdeductive sequent calculus for intuitionistic logic, which was until now only defined for classical logic. We show its equivalence with the superdeductive natural deduction. This implies that superdeduction can be easily used as a logical framework. These results lead to a better understanding of the implementation and the automation of proof search for PTS, as well as to more cooperation between proof assistants.