Personal tools
You are here: Home Events Abstract Archives 2005 Type Theory in Sequent Calculus

Type Theory in Sequent Calculus

Stephane 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 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.

Document Actions