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 proof-search. We enrich a proof-term 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 Cut-elimination, 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 proof-search, where the conversion rules (those that change the type of a term into a convertible type) are incorporated into the other rules. Simple proof-search tactics can then be expressed as the bottom-up 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 higher-order matching.