The discussion of proofs as objects and Heyting semantics Heyting's semantics in section 2 suggested treating proofs as objects and propositions as the types they inhabit. True propositions are those inhabited by proofs. But there were several questions left open in section 2.14 about the details of carrying out this idea.
The type theory of this section can answer these questions, and in so doing it provides a semantics of proofs. The basic idea is to consider a proposition as the type of all of its proofs and to take proof expressions to denote objects of these types. Based on Heyting's semantics we have a good idea of how to assign a type to compound propositions in terms of types assigned to the components. For atomic propositions there are several possibilities, but the simple one will turn out to provide a good semantics. The idea is to consider only those atomic propositions which can plausibly have atomic proofs and to denote the canonical atomic proofs by the term axiomaxiom. We will assign types to the compound propositions in such a way that the canonical elements will represent what we will call canonical proofs. Moreover, the reduction relation on the objects assigned to proof expressions will correspond to meaningful reductions on proofs. Proofs corresponding to noncanonical objects will be called noncanonical proofs. The correspondence will guarantee that noncanonical proofs p' of a proposition P will reduce to canonical proofs of P.
We now define the correspondence between propositions and types and between proofs and objects. Sometimes this correspondence is called the Curry-Howard isomorphism.