Applications
In cartesian closed categories, a "function of two variables" (a morphism f:X×Y → Z) can always be represented as a "function of one variable" (the morphism λf:X → ZY). In computer science applications, this is known as currying; it has led to the realization that simply-typed lambda calculus can be interpreted in any cartesian closed category.
The Curry-Howard-Lambek correspondence provides a deep isomorphism between intuitionistic logic, simply-typed lambda calculus and cartesian closed categories.
Certain cartesian closed categories, the topoi, have been proposed as a general setting for mathematics, instead of traditional set theory.
The renowned computer scientist John Backus has advocated a variable-free notation, or Function-level programming, which in retrospect bears some similarity to the internal language of cartesian closed categories. CAML is more consciously modelled on cartesian closed categories.
Read more about this topic: Cartesian Closed Category