> Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory.

Thanks! For the interested, Girard's book focuses on the Curry-Howard isomorphism, another great result linking computer programs (actually, the typed lambda-calculus) to mathematical proofs.