================================================================================ The Curry-Howard Correspondence ================================================================================ Proof Scripts ================================================================================ Quantifiers, Implications, Functions ================================================================================ Programming with Tactics ================================================================================ Logical Connectives as Inductive Types ================================================================================ Conjunction -------------------------------------------------------------------------------- Disjunction -------------------------------------------------------------------------------- Existential Quantification -------------------------------------------------------------------------------- True and False -------------------------------------------------------------------------------- Equality ================================================================================ Inversion, Again --------------------------------------------------------------------------------