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.
A Strong Normalization Condition for Pure Type System
VALENTINI, SILVIO
2007
Abstract
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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
