A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

Roy Dyckhoff, S Lengrand, James Hugh McKinna

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


Basic proof search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of defining such sequent calculi for Pure Type Systems (PTS, which were originally presented in natural deduction) and then organizing their rules for effective proof search. First, we introduce the idea of a Pure Type Sequent Calculus (PTSC) by enriching a permutation-free sequent calculus for propositional logic due to Herbelin, which is strongly related to natural deduction and already well adapted to proof-search. Such a PTSC admits a normalisation procedure, adapted from Herbelin's and defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satisfies the Subject Reduction property and is confluent. Each PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising iff the latter is. Second, we make the logical rules of PTSC syntax-directed for proof search, by incorporating the conversion rules as in syntax-directed presentations of the PTS rules for type checking. Third, we consider an extension PTSCa of PTSC with explicitly scoped meta-variables, representing partial proof-terms, and use it to analyse interactive proof construction. This sets up a framework in which we are able to study proof-search strategies, type inhabitant enumeration and unification.
Original languageEnglish
Pages (from-to)1--35
Number of pages35
JournalLogical Methods in Computer Science
Issue number1:6
Publication statusPublished - 2011


  • Type theory
  • PTS
  • Sequent Calculus
  • Strong normalisation
  • proof-search
  • interactive proof construction


Dive into the research topics of 'A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems'. Together they form a unique fingerprint.

Cite this