A Strong Normalisation Condition for Pure Type Systems
A proof theoretical analysis suggests that the process of
cut elimination in a sequent calculus corresponds to the normalisation of the
proofs in natural deduction. If one moves to proofs decorated with lambda terms
according to the Curry-Howard’s
isomorphism, the same observation leads to realising that the process of normalisation of the lambda-terms decorating the proofs in natural deduction is deeply connected with the property of closure under substitution of the lambda terms decorating the proofs in a sequent calculus. In this paper we show that this observation becomes a criterion to recognise the strongly normalising Pure Type Systems.