Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.
Хаскелл Карри[1] и Уильям Ховард[англ.][2] заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — интерпретация Брауэра — Гейтинга — Колмогорова[англ.] (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория реализуемости[англ.] Клини (1945).
Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, логика высказываний второго порядка[англ.] — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами.
В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные: