柯里-霍华德同构是指计算机程序和数学证明之间的紧密联系；即函数的类型相当于命题，函数的实现相当于证明。这种对应也叫做柯里-霍华德对应、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·加里和逻辑学家William Alvin Howard独立发现的。Curry-Howard 同构显示了推理系统和程序语言之间的相似性，类型即命题，程序即证明。或表示了计算机程序与数理逻辑之间的直接联系(逻辑上的等价关系)，即我们可以利用数理逻辑中的某些东西来去表示程序中的特定逻辑。