
Type Theory in Sequent CalculusStephane Lengrand University of St. Andrews and University Paris VII 11am Friday 28th October 2005 Room 2511, JCMB, King's Buildings Sequent calculus is an convenient formalism to express proofsearch. We enrich a proofterm assignment system due to Herbelin in order to express Pure Type Systems in the framework of Sequent Calculus. Each system is equipped with a normalisation procedure satisfying Subject Reduction and is logically equivalent to its version in Natural Deduction. The normalisation procedure, adapted from Herbelin's, is defined by local rewrite rules as in Cutelimination, using explicit substitutions. Its strong normalisation is equivalent to that of the PTS in natural deduction. We present an alternative presentation of the sequent calculus systems for the purpose of proofsearch, where the conversion rules (those that change the type of a term into a convertible type) are incorporated into the other rules. Simple proofsearch tactics can then be expressed as the bottomup application of the typing rules. We then mention a few ideas to express more powerful tactics, such as existential declarations in environments and the use of explicit substitutions for higherorder matching. Document Actions 
