Sequent calculi for the normal terms of the $\lambda\Pi$- and $\lambda\Pi\Sigma$-calculi

Abstract

This paper presents two sequent calculi, requiring no clausal form for types, whose typable terms are in 1-1 correspondence with the normal terms of the $\lambda\Pi$- and $\lambda\Pi\Sigma-4calculi. Such sequent calculi allow no permutations in the order in which inference rules occur on derivations of typable terms and are thus appropriate for proof search. In these calculi proof search can be performed in a root-first fashion and type conversions are solely required in axiom formation.