#proof The Curry-Howard correspondence is a fundamental principle in computer science and logic that establishes a deep connection between the [[Mathematical proof|proofs]] of mathematical theorems and [[Computer Program|programs]] in a computational language. It states that there is a correspondence between logical systems and type systems. In this correspondence, logical propositions are seen as types, and proofs of these propositions are seen as programs inhabiting those types. The correspondence was first formulated independently by logician [[Haskell Curry]] and computer scientist [[William Alvin Howard]] in the 1930s-1960s. The [[Curry-Howard-Lambek Isomorphism]] extends the Curry-Howard correspondence by incorporating syntactical rules. It establishes an isomorphism between typed lambda calculi (a formal system for expressing computation based on function abstraction and application) and Cartesian closed categories (a category with certain properties that allow modeling of computations). This isomorphism connects three different domains: logic, programming, and category theory. It provides a powerful framework for understanding the relationships between these domains and allows for insights into how computations can be understood as processes of proof construction. The [[Curry-Howard-Lambek Isomorphism]] has had a significant impact in various areas of computer science and mathematics. It has been instrumental in the development of programming languages with strong type systems, theorem provers, proof assistants, and functional programming techniques. The correspondence also highlights the deep connection between computation, logic, and category theory, enabling cross-pollination of ideas across these disciplines. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Curry-Howard Correspondence") or contains(subject, "Curry-Howard isomorphism") or contains(subject, "Curry-Howard Isomorphism") or contains(subject, "Curry-Howard correspondence") ```