Curry-Howard同構

對應可以在兩個層面上看到，首先是類比層次，它聲稱一個函數計算出的值的類型的斷言類比於一個邏輯定理，計算這個值的程序類比於這個定理的證明。在理論計算機科學中，這是連接lambda 演算和類型論的毗鄰領域的一個重要的底層原理。它被經常以下列形式陳述為證明是程序。一個可選擇的形式化為命題為類型。其次，更加正式的，它指定了在兩個數學領域之間的同構，就是以一種特定方式形式化的自然演繹，和簡單類型 lambda 演算之間是雙射，首先是證明和項，其次是證明歸約步驟和 beta 歸約。

有多種方式考慮 Curry-Howard 對應。在一個方向上，它工作於編譯證明為程序級別上。這裏的證明，最初被限定為構造性邏輯 — 典型的是直覺邏輯系統中的證明。而程序是在常規的函數式編程的意義上的；從語法的觀點上看，這種程序是用某種 lambda 演算表達的。所以 Curry-Howard 同構的具體實現是詳細研究如何把來自直覺邏輯的證明寫成 lambda 項。(這是 Howard 的貢獻；Curry 貢獻了組合子，它是相對於是高級語言的 lambda 演算是能寫所有東西的機器語言)。最近，同樣處理經典邏輯的 Curry-Howard 對應的擴展可被公式化了，通過對經典有效規則比如雙重否定除去和 Peirce 定律關聯上明確的用續體比如 call/cc 處理的一類項。

還有一個相反的方向，對一個程序的正確性關聯上證明提取的可能性。這在非常豐富的類型論環境中是可行的。實際上理論家對非常豐富類型的函數式編程語言的開發，已經部分的被希望帶給 Curry-Howard 對應更加顯著的地位的動機所推動。