Type theory is a theory of mathematical constructions. Types represent various possible ways of constructing objects rather than collections of objects as seen in set theory. Terms of a type are not only determined by their inhabitation of that type but also by their construction. Intuitionistic logic is a system in which validity of a statement is not determined by its value but rather by the existence of a construction, or a proof, of that statement. As it turns out, there exists a natural connection between the two systems, called Curry-Howard correspondence or Curry-Howard isomorphism, that maps logical propositions to types, and their respective proofs into terms of corresponding types.
|
