#proof The [[Curry-Howard-Lambek isomorphism]] is a fundamental concept in mathematics and computer science that establishes a deep connection between [[Logic|logic]], [[Type Theory|type theory]], and [[Category Theory|category theory]]. It was named after logicians [[Haskell Curry]] and [[William Howard]], along with mathematician [[Joachim Lambek]]. At its core, the isomorphism explores the similarities between formal systems of logic and systems of computation. It states that there is a correspondence between [[Mathematical proof|proofs]] in logical systems and [[Computer Program|algorithms]] in computational systems. In other words, logical propositions can be seen as types, and logical proofs can be seen as programs that inhabit those types. This connection between logic and computation has profound implications. It allows us to reason about programs using logical principles and vice versa. By representing logical propositions as types, we can use type theory to analyze the correctness of programs. Similarly, we can use logical rules to guide program construction. Furthermore, the Curry-Howard-Lambek isomorphism also connects [[Type Theory]] with [[Category Theory]]. Category theory provides a framework for studying mathematical structures and their relationships. The isomorphism shows that there are parallels between categories and types, where objects in categories correspond to types, morphisms correspond to functions between types, and so on. The insights provided by the Curry-Howard-Lambek isomorphism have had significant impacts on various fields. In computer science, it has influenced the development of programming languages with strong type systems like [[Haskell]], [[Coq]], and [[Lean]]. It has also led to advancements in automated proof assistants that allow for formal verification of software correctness. # Structural, Procedural, and Historical I came up with a triplet term to explain [[Curry-Howard-Lambek isomorphism]]. It can be roughly divided into: 1. [[Structural Integrity]] 2. [[Procedural Efficiency]] 3. [[Historical Evidence]] ![[Computational Trinitarian Table#The Second Table]] ## Role of Joachim Lambek See [[Differences between CH and CHL Isomorphism]] # Conclusion In summary, the [[Curry-Howard-Lambek isomorphism]] underscores the deep connections between logic, computation, type theory, and category theory. It provides a unified perspective on these areas of study and offers valuable tools for reasoning about both mathematical proofs and computational programs. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Curry-Howard Correspondence") or contains(subject, "Curry-Howard-Lambek") ```