Type Theory and the Curry-Howard Isomorphism: The Profound Harmony of Propositions as Types and Proofs as Programs
