Relation between Cartesian closed category and Lambda Calculus I am programmer (from the object oriented world) and currently getting my head around functional programming. I was looking to get some basics right.
I understand what category theory and lambda calculus try and tell . I did read that lambda calculus can be modelled in any Cartesian closed category. and this is the how the 2 ideas can combine. But this is where i lost my way.
1) What is a Cartesian closed category ? (dint understand the mathematical semantics given , so wanted to know in simple English with some examples if possible).
2) How can Lambda calculus express this Cartesian closed category? 
 A: I see that this question has an already accepted answer. Nonetheless I would like to give an alternative answer: sometimes seeing
things from different perspective can help getting a better understanding of the subject.
There are many possible definitions/characterization of cartesian closed category (CCC in what follows), one of them is the following.
A CCC is a category $\mathbf C$ with:


*

*an object $1 \in \mathbf C$ such that for   each object $X \in \mathbf C$ there is one and only one morphism $t \colon X \to 1$
(you can think of $1$ as a generalization of the singleton set,  the set with only one element)

*for every    pair of object $X$ and $Y$ you have an object $X \times Y$ with two projection morphisms
$$\pi_X \colon X \times Y \to X \ \pi_Y \colon X \times Y \to Y$$
and an operation, called pairing, that for every pair   $(f,g) \in \mathbf C[T,X] \times \mathbf C[T,Y]$ gives you a morphism
$$\langle f,g \rangle \in \mathbf C[T,X \times Y]$$
with the requirement that $\pi_X \circ \langle f,g\rangle=f$ and $\pi_Y \circ \langle f,g \rangle=g$ 

*for each pair of objects $X$ and $Y$ an object $Z^Y \in \mathbf C$ with a morphism $\epsilon \colon Z^Y \times Y \to Z$
such that the mapping 
$$\mathbf C[T,Z^Y] \to \mathbf C[T \times Y,Z]$$
$$f \colon T \to Z^Y \mapsto \epsilon \circ (f\circ \pi_T, \pi_Y) \colon T \times Y \to Z$$
is a bijection.


If you reguard a category as some sort of generalized system of types and function between them then:


*

*the object $1$ become the unit type, the type with only one element, and the unique function $t \colon T \to 1$ is the constant function;

*for each pair of objects/types $X$ and $Y$, the object $X \times Y$ is nothing but the product type (the type of tuples) with projections $\pi_X$ and $\pi_Y$ playing the role of ...... well projections and the pairing $\langle,\rangle$ generalizing the pairing constructor for ordered pairs

*the object $Z^Y$ is the type of functions from $Y$ to $Z$, the morphism $\epsilon \colon Z^Y \times Y \to Z$ is the evaluation, and the mapping 
$$\mathbf C[X,Z^Y] \to \mathbf C[X \times Y,Z]$$
is the uncurrying.


This parallelism makes arise a notion of interpretation of simply typed $\lambda$-calculus in cartesian closed categories: where an interpretation is nothing but a way to associate objects of a CCC to types and morphisms to $\lambda$-terms (functions).
Giving the details of this construction would be very long so I would rather avoid to give it here, by the way I think you can find different references on the subject: try googling categorical semantics of simply typed lambda-calculus.
I hope this helps.
A: In imperative programming there is a tendency to distinguish between data and methods, whereas in functional programming, for example, they are identical. A closed category is a category that makes this identification: hom-sets (methods) correspond to certain objects (data).
More concretely, the category is closed if it has a binary operation on objects $(X,Y) \mapsto Y^X$ such that
it is actually the data version of methods:
$$∀ X, Y, Z \;\;•\;\; (Z ⊕ X ⟶ Y) ≅ (Z ⟶ Y ^ X) \;\text{ natural in } Z, Y$$
The Cartesian part says that we can form any finite record ---in the programming sense. That is, if we have $n$ records of interest $R_1, \ldots, R_n$ then we can amalgamate them into one record $\Pi_{i \in 1..n} R_i$ and that this is their product means that any function/method to it is precisely $n$ methods to the individual factors! 
$$
\forall X \;\bullet\; (X \to \Pi_{i \in 1..n} R_i) \cong \Pi_{i \in 1..n} (X \to R_i) 
$$
The left-hand $\Pi$ is the object in the category, while the right-hand $\Pi$ is the usual set-theoretic. The case $n = 0$ gives us the empty-tuple aka the terminal object. With this and the ability to construct a product of two records, we can construct all finite products ---this is the usual presentation of cartesian.
Defining type := object, these together say that: if a,b are types then (a -> b), a x b, and 1 are all types, which are the usual type-constructions expected when working in type theory.
Hope this help :-)
