CurryHoward Correspondence
There is a relationship between computer programs and mathematical proofs, this is known as the CurryHoward correspondence.
A type in λcalculus has the same mathematical structure as a proposition in intuitionistic logic.
A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:
Proposition  Type 

true formula  unit type 
false formula  empty type 
implication  function type 
conjunction  product type 
disjunction  sum type 
universal quantification  generalised product type (Π type) 
existential quantification  generalised sum type (Σ type) 
For more information about the CurryHoward correspondence see the page here.
λcalculus Structure
There is more information about λcalculus on page here but here we are interested in its basic type structure.
We can start with some predefined type.  T 
A function type goes from one type to another  T>S 
We can have higher order function types which go from a function to another function.  (T>S)>(P>Q) 
... and so on. 
Intuitionistic Logic Structure
There is more information about Intuitionistic Logic on page here but here we are interested in its basic structure.
We can start with a simple proposition.  A 
Predicate calculus allows us to have conditional predicates.  if A then B 
Again we han have higher order versions of this to any level.  if (if A then B) then (if C then D) 
... and so on. 
Curry–Howard–Lambek Correspondence
We can extend this correspondence to include cartesian closed categories (CCC) in category theory. 

More information about:
 Cartesian Closed Categories (CCC) on page here.
 λcalculus on page here.
 Intuitionistic Logic on page here.
Cartesian Closed Category  λcalculus  intuitionistic logic 

objects  types 
proposition p = proposition P = proof of p 
Operator Types 

function type 
implication A implies B 

product type <a,b>:A/\B 
conjunction if A is proof of 'a' and B is proof of 'b' then A/\B is proof of <a,b> 

sum type a+b:A\/B 
disjunction if A is proof of 'a' and B is proof of 'b' then A\/B is proof of a+b 

Dependant Types 

dependent product type The type of the result B(a) depends on the value a . 
universal quantification (a:A).B(a) 

dependent sum type 
existential quantification (a:A).B(a) 

unit type  true formula T 

bottom type  false formula __ 

Inductive Types 

recursive function  inductive proof  
morphisms  terms  proof 
variable  axiom  
constructor  introduction rule  
destructor  elimination rule  
normal form  normal deduction  
weak normalisation  normalisation of deductions  
type inhabitation problem  provability  
inhabited type  intuitionistic tautology  
function application  
substitution  