Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES).\xa0 Initial consideration of Curry-Howard for first-order and higher-order logic.\xa0 Dependent types.