The Curry-Howard Correspondence reveals a close correspondence between the constituents of Logic and of Programming. Also known as the Formulas as Types and the Proofs as Programs interpretations.

Existential Quantification (∃) of Logic corresponds to the Generalized Disjoint Sum Type (∑) of Programming. Universal Quantification (∀) of Logic corresponds to the Generalized Cartesian Product Type (∏) of Programming. Conjunction (⋀) of Logic corresponds to the Product type (×) of Programming. Disjunction (⋁) of Logic corresponds to the Sum type (+) of Programming.

There are associations between the Curry-Howard Correspondence and the fourfolds of the Square of Opposition, Attraction and Repulsion, and of course Linear Logic.

Further Reading:

http://en.wikipedia.org/wiki/Curry-Howard_correspondence

<>