The paper by W. H. Howard (1969) explores the relationship between formulae-as-types and constructive mathematics, particularly in the context of intuitionistic logic and Heyting arithmetic. It introduces a notion of "construction" as a term in a λ-calculus system, where each term has a type symbol. The paper shows that the axioms and rules of inference of positive implicational propositional logic (P(⊃)) correspond exactly to the rules of term formation in λ-calculus. This correspondence allows for the interpretation of logical derivations as constructions, with each derivation corresponding to a term that can be reduced to normal form. The paper discusses the normalization of terms and its connection to cut elimination in sequent calculus. It shows that the reduction of terms to normal form corresponds to the elimination of cuts in proofs. This is demonstrated by replacing the rule (1.3) of P(⊃) with a more direct rule that allows for the construction of irreducible terms. The paper also extends the system to include logical connectives such as negation, conjunction, and disjunction, and discusses the interpretation of these in terms of set theory and functionals. In the context of Heyting arithmetic, the paper defines constructions as terms built from prime terms using rules of term formation. It shows that derivations in Heyting arithmetic can be interpreted as constructions, and that these constructions can be reduced to normal form. The paper also provides an interpretation of terms in terms of sets and functions, and discusses the normalization of terms in this context. The paper concludes by showing that the normalization of terms in Heyting arithmetic corresponds to the elimination of cuts in proofs, and that this provides a foundation for the study of constructive mathematics. The paper also discusses the interpretation of terms in terms of set theory and functionals, and the relationship between the normalization of terms and the elimination of cuts in proofs.The paper by W. H. Howard (1969) explores the relationship between formulae-as-types and constructive mathematics, particularly in the context of intuitionistic logic and Heyting arithmetic. It introduces a notion of "construction" as a term in a λ-calculus system, where each term has a type symbol. The paper shows that the axioms and rules of inference of positive implicational propositional logic (P(⊃)) correspond exactly to the rules of term formation in λ-calculus. This correspondence allows for the interpretation of logical derivations as constructions, with each derivation corresponding to a term that can be reduced to normal form. The paper discusses the normalization of terms and its connection to cut elimination in sequent calculus. It shows that the reduction of terms to normal form corresponds to the elimination of cuts in proofs. This is demonstrated by replacing the rule (1.3) of P(⊃) with a more direct rule that allows for the construction of irreducible terms. The paper also extends the system to include logical connectives such as negation, conjunction, and disjunction, and discusses the interpretation of these in terms of set theory and functionals. In the context of Heyting arithmetic, the paper defines constructions as terms built from prime terms using rules of term formation. It shows that derivations in Heyting arithmetic can be interpreted as constructions, and that these constructions can be reduced to normal form. The paper also provides an interpretation of terms in terms of sets and functions, and discusses the normalization of terms in this context. The paper concludes by showing that the normalization of terms in Heyting arithmetic corresponds to the elimination of cuts in proofs, and that this provides a foundation for the study of constructive mathematics. The paper also discusses the interpretation of terms in terms of set theory and functionals, and the relationship between the normalization of terms and the elimination of cuts in proofs.