A Strong Normalisation Condition for Pure Type Systems

Milena Stefanova
Agency for sustainable growth, ENEA, Bologna (Italy)

Silvio Valentini
Dip. Matematica Pura e Applicata, Università di Padova, Padova (Italy)


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.

Full text