The Curry Howard isomorphism

The Curry Howard Isomorphism said that types are propositions and programs are their proofs. A proposition is an assertion (declarative statement), which is either true or false (but not both).

Examples of propositions

Consider the following examples of propositions:

• The equation 2 * 3 = 5

• If it is storming outside, then I take an Uber to class; otherwise, I walk, and if it is sunny, then I ride my bicycle:

Variable	Clause
a	It is storming outside
b	I take an Uber to class
c	I walk
d	It is sunny
e	I ride my bicycle

 

The following is the written logic version:

a implies b and ((not a) implies (c and (d implies e)))

The following is the logical symbols version:

(a ⇒ b) ∧ (¬a ⇒  (c ∧ (d⇒  e)))

Not propositions

The following are the examples of not propositions:

• x = 5  (this is not an assertion of truth, it's an assignment)
• x + y = 5 (not enough information to be an assertion, answer depends on missing data)

Propositions can combine terms using connectives (and, or not).

Lambda calculus

Alonzo...