I am confused about Church's simply typed lambda calculus and the Curry-Howard isomorphism.
Church's simply typed lambda calculus in the paper cited above is given a classical proof theory, in that on p. 4 of the PDF above (p. 58 of the original article) we have the classical definitions of disjunction, conjunction and existential quantification.
Later authors (Henkin in Completeness in the Theory of Types and A Theory of Propositional Types) follow suit; section §4 of the latter article building up the connectives via $\top$ and $\bot$ with a classical disjunction (see 4.5 of section §4). Henkin's type theory is classical in its proof rules and its semantics.
However, the simply typed lambda calculus is usually taken to correspond syntactically via the Curry Howard isomorphism to intuitionistic propositional logic.
Given the classical behaviour, proof-theoretically, of Church's original simply typed lambda calculus in the above article, how is this correspondence achieved with intuitionistic logic? Do the simply typed lambda calculi of Henkin and Church correspond to the Intuitionistic propositional calculus? Can we have the simply typed lambda calculus with classical proof rules and a classical semantics corresponding to intuitionistic propositional logic.
What would the law of the excluded middle in the simply typed lambda calculus of the Church or Henkin variety described correspond to on the logic side of the Curry Howard isomorphism?
If someone could clarify where I am going wrong I would be very happy.