1980年正式发表在Seldin和Hindley辑的纪念Curry的文集中的Curry Howard同构的原始文章。

实际上Curry的手稿里早在1930年之前，Curry就发现了这个现象；在1958年的组合子逻辑第一卷里，有一节题目是Analogy with Propositional Algebra，里面使用的词语是FP transformation。

1969年Howard写了这篇文章把直觉主义和构造数学和类型联系在一起，正式提出了「formulae as types」的计算机科学顺口溜，并广为流传。

很重要的一点是Martin Löf充分发掘了这个想法对于构造数学的价值，定理证明器先驱De Bruijn也几乎是连夜上车奔向直觉主义类型论。他们的工作开启了类型论，辅助定理证明器，和类型驱动的计算机语言理论与程序开发的大发展。