Chapter 8: Curry-Howard Correspondence

Curry-Howard correspondence is all about correspondencing between types and logic.

• \[\Sigma\]

  : exists

• \[\Pi\]

  : forall

• \[\rightarrow\]

  : implies

By this correspondence, we can write constructive proof by the program.