Chapter 3: The Curry-Howard Isomorphism
The third chapter of the Iowa Type Theory Commute is about the
Curry-Howard isomorphism, which is an amazing connection between
logic and programming. We start with constructive logic, since the
Curry-Howard isomorphism originated for this kind of logic.