Curry-Howard isomorphism between typed terms of formal systems representing computable functions and deductions in certain logics.
Simply typed lambda calculus, Godel's system T and Girard's system F. Strong normalization. Semantics. Expressibility of these -- how higher order functions and polymorphism add to expressibility.
Connection with provably recursive functions in systems of arithmetic. Polynomial time logic.
J.-Y. Girard, Y. Lafont, and P. Taylor.Proofs and Types, Cambridge University Press, 1989.
Notes on HOL by MJC Gordon, et. al.
Other relevant literature.