Complex sentence: Type Theory is based on the identification of propositions and types: a proposition is identified with the type of its proofs, this identification is usually called the Curry Howard isomorphism, which was originally formulated for propositional logic and simply typed lambda calculus.
Split into simpler sentences: Type Theory is based on the identification of propositions and types: a proposition is identified with the type of its proofs. This identification is usually called the Curry Howard isomorphism, which was originally formulated for propositional logic and simply typed lambda calculus.