Uniform Schemata for Proof Rules - Ulrich Berger (Computability in Europe 2015 (CiE 2015), 2014)
Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate introduction and elimination rules in natural deduction and sequent calculus style. In addition, the system supports program extraction from proofs by generating realizers for the proof rules automatically.