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 Cartesian Product type (∑) of Programming. Universal Quantification (∀) of Logic corresponds to the Generalized Function Space 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.

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

<>

### Like this:

Like Loading...

This entry was posted on August 21, 2012 at 9:00 PM and is filed under Computation, fourfolds, linear logic, logic. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply