Categorical logic

Summary

Categorical logic is the branch of mathematics that studies logic with the tools of category theory. A logical theory is matched with a category built from its syntax. A model of the theory is then a structure-preserving functor from that category to another category, such as the category of sets. Typical correspondences match the simply typed lambda calculus with Cartesian closed categories, and higher-order intuitionistic logic with toposes. These correspondences let one transfer results between logic, algebra, geometry and the semantics of programming languages.