The paper by W. H. Howard, "The Formulae-as-Types Notion of Construction," published in 1969, explores the development of a notion of construction suitable for interpreting intuitionistic mathematics. The author aims to bridge the gap between axioms of positive implicational propositional logic and basic combinators, inspired by H. Curry's observations and W. Tait's work on cut elimination and λ-term reduction. In Part I, the intuitionistic propositional calculus is discussed, focusing on the sequent calculus and the correspondence between axioms and basic combinators. The notion of construction is introduced, where a construction of a sequent is a term of a specific type that respects the occurrences of free variables in the sequent. The axioms and rules of inference of the calculus are shown to correspond exactly to the rules of term formation. In Part II, the concepts are applied to Heyting arithmetic, specifically the subsystem \(\mathbf{H}(\supset, \wedge, \forall)\). The paper defines constructions in this context, which are terms built from prime terms using specific rules of term formation. The axioms and rules of inference of Heyting arithmetic are interpreted as the existence of certain terms and the rules of term formation, respectively. The interpretation of terms is extended to include sets and functions, with a detailed definition of how each term is associated with an object. The paper also discusses the normalization of terms and cut elimination, showing that the reduction of terms to normal form is equivalent to cut elimination in the sequent calculus. Additionally, it introduces special terms for negation, conjunction, and universal quantification, and provides theorems to support these constructions and interpretations.The paper by W. H. Howard, "The Formulae-as-Types Notion of Construction," published in 1969, explores the development of a notion of construction suitable for interpreting intuitionistic mathematics. The author aims to bridge the gap between axioms of positive implicational propositional logic and basic combinators, inspired by H. Curry's observations and W. Tait's work on cut elimination and λ-term reduction. In Part I, the intuitionistic propositional calculus is discussed, focusing on the sequent calculus and the correspondence between axioms and basic combinators. The notion of construction is introduced, where a construction of a sequent is a term of a specific type that respects the occurrences of free variables in the sequent. The axioms and rules of inference of the calculus are shown to correspond exactly to the rules of term formation. In Part II, the concepts are applied to Heyting arithmetic, specifically the subsystem \(\mathbf{H}(\supset, \wedge, \forall)\). The paper defines constructions in this context, which are terms built from prime terms using specific rules of term formation. The axioms and rules of inference of Heyting arithmetic are interpreted as the existence of certain terms and the rules of term formation, respectively. The interpretation of terms is extended to include sets and functions, with a detailed definition of how each term is associated with an object. The paper also discusses the normalization of terms and cut elimination, showing that the reduction of terms to normal form is equivalent to cut elimination in the sequent calculus. Additionally, it introduces special terms for negation, conjunction, and universal quantification, and provides theorems to support these constructions and interpretations.