Logic todo learn: Open Logic Project – Open Source, Customizable, Advanced Logic Text Impredicativity Extensionality Intensional logic The significance of the Curry-Howard isomorphism – Richard Zach