Natural deduction and sequent typed lambda calculus


Silvia Ghilezan




Two different formulations of the simply typed lambda calculus: the natural deduction and the sequent system, are considered. An analogue of cut elimination is proved for the sequent lambda calculus.