The Curry-Howard correspondence relates formal proofs in logic and computer programs in a typed functional programming language. It is the underlying theory behind Coq, one of the major systems today for verifying correctness of proofs using computers. The theory is further extended by Vladimir Voevodsky in the univalent foundations program. In this talk I will describe the original correspondence and give some of the simpler examples.