At the heart of the connections between Proof Theory and Type Theory, the Curry-Howard correspondence provides proof-terms that are equipped with computational features and equational theories, i.e. notions of normalisation and equivalence. We extend the framework of these concepts in three directions: proof-theoretic formalisms (such as sequent calculus) that are appealing for logical purposes like proof-search, powerful systems beyond propositional logic such as type theories, and classical (rather than intuitionistic) reasoning.
We review proof-term calculi for (intuitionistic) sequent calculus, with rewrite systems performing cut-elimination in the typed case. We recall the Call-by-name and Call-by-value reductions in these systems, the T-restriction and Q-restriction. We show how, from the Q-restriction, we obtain the depth-bounded sequent calculus G4 and an internal cut-elimination procedure for it, which becomes unsound with respect to beta-equivalence.
We then enrich the T-restriction into Pure Type Sequent Calculi (PTSC), which are to sequent calculus what Pure Type Systems are to natural deduction. The former are equivalent (with respect to both provability and normalisation) to the latter. We show how PTSC are better adapted for proof-search in such type theories, since their inference rules are both closer to basic proof-search tactics of proof assistants and able to express type inhabitant enumeration algorithms.
Finally we present some approaches to classical Type Theory, starting with a sequent calculus for a classical version of System Fomega. Beyond such a type theory (e.g. with dependent types), the notion of equivalence of classical proofs
becomes crucial and, with such a notion based on parallel rewriting in the Calculus of Structures, we compute canonical representatives of equivalent proofs.