Curry and Feys (1958) extended the correspondence idea to one between type theory and Gentzen’s sequent calculus. In the paper already cited, circulated in 1969, but only published in a volume in a Festschrift for Curry in 1980, W.A. Howard (1969) deepened the CH correspondence by demonstrating a correspondence between intuitionistic sequent form natural deduction and type theory in \(\lambda\)-calculus format, generalising to encompass intuitionist arithmetic- ‘Heyting arithmetic’ (HA)- (thus r