In type theory, the paradigm of propositions as types says that a proposition and a type are the same thing. A proposition is identified with its type of proofs, and a type is identified with the proposition that it has an element. Not all type theories follow this paradigm; among those that do, those of Per Martin-Löf? are the most famous.
Even when the paradigm is not adopted, however, there is still a close relationship between logical and type-theoretic operations, called the Curry–Howard isomorphism or (if it is not clear in which category this isomorphism is supposed to exist) the Curry–Howard correspondence. This correspondence is most precise and well-developed for intuitionistic logic.