Curry-Howard對應

喺程式語言論同證明論入面，Curry-Howard對應（粵拼：koe1 ri1 haau1 woet1 deoi3 jing3，亦稱Curry-Howard同構；英文：Curry-Howard correspondence；華文：柯里-霍華德對應）就係講緊電腦程式同埋數學證明之間嘅直接關連。

佢係generalize咗形式邏輯系統（formal logic）同公式計算（computational calculus）之間嘅關連，係由發現美國數學家Haskell Curry同埋邏輯師William Alvin Howard嘅。 邏輯同運算呢個𪐀褦先至係Curry同Howard嘅貢獻，其他嘅同直觀主義邏輯（institutional logic）有關嘅operational interpretation（睇Brouwer-Heyting-Kolmogorov演繹同埋可實現性）。呢個𪐀褦亦都可以延伸去同包埋範疇論（category theory），噉就而形成Curry-Howard-Lambek對應嘞。