The course will focus on the so-called Curry-Howard Correspondence, or Isomorphism, and the associated "Proposition-as-types notion of constructivity". This is a framework which was developed by William Howard in the late Sixties of the last century, and which realized a confluence of many theoretical threads. Curry's Combinatory Logic, of course, but also Church's Lambda-Calculus, and the elaboration of the semantics for intuitionistic logic too. In the background, dominant was the role played by Hilbert, in turning the notion of "proof" into an object of mathematical study in itself, and of Gentzen, in starting the machinery of Structural Proof Theory.
The basic idea is that for each proposition in a given logic there is a type of objects, the proofs of the proposition, so that a proposition is to be considered as the type of its proofs. In other words, a type, or set, simply is the type, or set, of proofs of the proposition that labels that type, and, reciprocally, a proposition is just the type, or set, labeled by that same proposition, of its proofs. Howard was able to extend to first-order predicate logic the correspondence between the combinators and the implicational fragment of intuitionistic logic.
Topics related to this course can be found here. Here are the slides.