Simply typed lambda calculus and higher order logic What is the relation between simply typed lambda calculus and higher order logic?

Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related to higher order logic? According to this tutorial by Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf the language of HOL seems to be STT. Shouldn't it be PROP? What does that mean?

Did Church have in mind HOL when defined STT?
The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.

Taking $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants
$$ \forall_\tau:(\tau\rightarrow \omicron)\rightarrow \omicron\quad \supset:\omicron\rightarrow\omicron\rightarrow \omicron$$

where $\tau$ is an arbitrary type (so one $\forall$ constant for each type). One possible set of axioms:

$$ \frac{\phi(x)}{\forall_\tau(\lambda x.\phi(x))}\mbox{$x:\tau$ not free in the hypotheses}$$

$$ \frac{\Large{\substack{[\psi]\\ \\ .\\ .\\ .\\ \\ \phi}}}{\psi\supset \phi}$$

where $[\psi]$ means that the hypothesis $\psi$ is discharged. Interesting fact: the other connectives $\exists_\tau, \vee$... can be derived from just those 2.

The subtlety is distinguishing between $\lambda$-terms as a way to represent proofs, as predicated by the Curry-Howard-de Bruijn (Martin-Löf) correspondence, or as a way to represent the terms you reason upon. The two views are not incompatible, of course.

In particular there is a typed $\lambda$-calculus that faithfully represents HOL (minus various axioms of course). This happens to be a sub-system of the Calculus of Constructions, and is described in detail by Geuvers in The Calculus of Constructions and Higher Order Logic. He also details the differences between the two (the CoC is not a conservative extension of HOL).