The Curry-Howard correspondence connects logic and typed programming: propositions correspond to types, and proofs correspond to programs inhabiting those types.

An implication

$$P\Rightarrow Q$$

corresponds to a function type

$$P\to Q.$$

A proof of the implication is a function that transforms any proof of $P$ into a proof of $Q$.

A conjunction $P\land Q$ means that both propositions hold. It corresponds to a product type:

$$P\land Q \quad\leftrightarrow\quad P\times Q,$$

because proving both propositions means supplying both pieces of evidence.

A disjunction $P\lor Q$ means that at least one alternative holds. It corresponds to a sum type:

$$P\lor Q \quad\leftrightarrow\quad P+Q,$$

because evidence identifies which alternative is proved and carries its proof.

The proposition True corresponds to a type with a trivial inhabitant; False corresponds to an empty type with no inhabitants. From a value of the empty type, any result can follow because such a value cannot actually be constructed in a consistent system.

Under this view, type checking resembles proof checking and program normalization resembles proof simplification. The correspondence explains why richer type systems can express increasingly strong logical specifications and provides the conceptual bridge from ordinary function types to proof assistants and dependent types.