カリーとハワードの書簡

最初は、カリーとフェイズが1958年に出版した組み合わせ論理に関する本の中で、次のような単純な指摘があった。組み合わせ論理の基本コンビネータKとSの最も単純なタイプは、ヒルベルト型の演繹システムで使用されるそれぞれの公理スキームα → ( β → α )と( α → ( β → γ )) → (( α → β ) → ( α → γ ))に驚くほど対応していた。このため、これらのスキームは現在では公理KとSと呼ばれることが多い。ヒルベルト型の論理で証明として見られるプログラムの例を以下に示す。

直観主義の含意断片に限定すれば、ヒルベルト流の論理を形式化する簡単な方法は次のようになる。Γ を仮説とみなされる有限個の論理式の集合とする。このとき、δ はΓ から導出可能であり、Γ ⊢ δ と表記される。ただし、次の場合である。

• δは仮説であり、Γの式である。
• δは公理体系の一例である。すなわち、最も一般的な公理体系の下では、次のようになる。
  • δ の形式はα → ( β → α )、または
  • δ の形式は ( α → ( β → γ )) → (( α → β ) → ( α → γ ))、
• δは演繹によって導かれる。つまり、あるαに対して、α → δとαの両方がΓから既に導出可能である（これはモーダス・ポネンスの規則である）。

これは、次の表の左列に示すように、推論規則を用いて形式化することができる。

型付き組み合わせ論理は、同様の構文を用いて定式化できます。Γ を型が注釈された変数の有限集合とします。項 T (これも型が注釈されています) は、次の場合にこれらの変数 [Γ ⊢ T: δ ] に依存します。

• TはΓの変数の1つであり、
• Tは基本コンビネータである。すなわち、最も一般的なコンビネータ基底の下では、次のようになる。
  • T は K: α → ( β → α ) [ここでαとβ はその引数の型を表す]、または
  • T は S:( α → ( β → γ )) → (( α → β ) → ( α → γ ))、
• TはΓの変数に依存する2つの部分項の合成である。

ここで定義される生成規則は、下の右側の列に示されています。カリーのコメントは、両方の列が1対1に対応していることを単純に述べています。この対応を直観主義論理に限定するということは、パースの法則（( α → β ) → α ) → αのような古典的な同義反復が対応から除外されることを意味します。

より抽象的なレベルで見ると、この対応関係は次の表のように言い換えることができる。特に、ヒルベルト論理に特有の演繹定理は、組み合わせ論理の抽象化除去のプロセスと一致する。

対応関係のおかげで、組み合わせ論理の結果をヒルベルト論理に、またその逆も可能になります。例えば、組み合わせ論理における項の簡約の概念はヒルベルト論理に転用でき、同じ命題の証明を別の証明に標準的に変換する方法を提供します。また、通常の項の概念を通常の証明の概念に転用することで、公理の仮定がすべて分離されている必要はないこと（そうでない場合は単純化が発生する可能性があるため）を表現できます。

逆に、直観主義論理におけるパースの法則の非証明可能性は、組み合わせ論理に逆変換できる。つまり、組み合わせ論理の型付き項で、型で型付け可能なものは存在しない。

(( α → β ) → α ) → α。

組み合わせ子や公理の集合の完全性に関する結果も転用できる。例えば、組み合わせ子X が(外延的) 組み合わせ論理の1 点基底を構成するという事実は、単一の公理体系が

((( α → ( β → γ )) → (( α → β ) → ( α → γ ))) → (( δ → ( ε → δ )) → ξ )) → ξ、

これはXの主要なタイプであり、公理図式の組み合わせの適切な代替物である。

α → ( β → α ) および

( α → ( β → γ )) → (( α → β ) → ( α → γ ))。

カリーが直観主義ヒルベルト型の演繹と型付き組み合わせ論理との構文的対応関係を強調した後、ハワードは1969年に、単純な型付きラムダ計算のプログラムと自然演繹の証明との間の構文的類似性を明示した。以下では、左側が直観主義含意自然演繹を暗黙の弱化を伴うシーケントの計算として形式化し（シーケントの使用は、演繹規則をより簡潔に記述できるため、カリー-ハワード同型性の議論では標準である）、右側はラムダ計算の型付け規則を示している。左側では、Γ、Γ ₁、Γ _2は順序付き式のシーケンスを表し、右側では、名前がすべて異なる名前付き（つまり型付き）式のシーケンスを表す。

対応関係を言い換えると、Γ ⊢ αを証明するということは、Γ にリストされている型の値が与えられたときに、型αのオブジェクトを生成するプログラムを持つことを意味します。公理/仮説は、新しい制約のない型を持つ新しい変数の導入に対応し、→ I ルールは関数の抽象化に対応し、→ E ルールは関数の適用に対応します。コンテキスト Γ を式の集合とみなすと、対応関係は厳密には成り立たないことに注意してください。たとえば、型α → α → αのλ 項 λ x .λ y . xと λ x .λ y . yは、対応関係では区別されません。例を以下に示します。

ハワードは、この対応関係が論理の他の結合子や単純型付きラムダ計算の他の構成にも及ぶことを示した。抽象的なレベルで見ると、この対応関係は次の表のように要約できる。特に、ラムダ計算における正規形の概念が、プラウィッツの自然演繹における正規演繹の概念と一致することも示されており、そこから型占有問題のアルゴリズムを直観主義的証明可能性を判定するアルゴリズムに変換できることが導かれる。

ハワードの書簡は、当然ながら自然演繹法や単純型付きラムダ計算の他の拡張にも及ぶ。以下はその一部である。

• ジラール・レイノルズシステムFは、2階命題論理と多相ラムダ計算の両方に共通する言語である。
• 高階論理とジラールのシステム_Fω
• 代数的データ型としての帰納型
• 必要性${\displaystyle \Box }$様相論理と段階的計算において^{[ 12 ]}
• 可能性${\displaystyle \Diamond }$様相論理と効果のためのモナド型^{[ 11 ]}
• λ _I計算 (抽象化はλx . Eに制限され、xはEに少なくとも 1 つの自由出現を持つ)とCL _{I計算は、}関連する論理に対応します。^{[ 13 ]}
• グロタンディーク位相における局所真理（∇）様相、またはベントン、ビアマン、デ・パイヴァ（1998）の同等の「緩い」様相（◯）は、「計算型」を記述するCL論理に対応する。^{[ 14 ]}

カリーの時代もハワードの時代も、証明とプログラムの対応関係は直観主義論理、すなわち特にパースの法則が演繹できない論理のみを対象としていました。この対応関係がパースの法則、ひいては古典論理にまで拡張されることは、グリフィンが、与えられたプログラム実行の評価コンテキストを捉える型演算子に関する研究から明らかになりました。これにより、この評価コンテキストを後で復元することが可能になります。古典論理におけるカリー・ハワード式の基本的な対応関係を以下に示します。古典証明を直観主義論理にマッピングするために使用される二重否定変換と、制御を含むラムダ項を純粋ラムダ項にマッピングするために使用される継続渡しスタイルの変換との間の対応関係に注目してください。より具体的には、名前呼び出し継続渡しスタイルの翻訳はコルモゴロフの二重否定翻訳に関連し、値呼び出し継続渡しスタイルの翻訳は黒田による一種の二重否定翻訳に関連します。

古典論理を、パースの法則のような公理を追加するのではなく、シーケントに複数の結論を許容することによって定義すれば、より精緻なカリー・ハワード対応が古典論理にも存在する。古典的な自然演繹の場合、証明とパリゴのλμ計算の型付きプログラムとの間に、プログラムとしての対応関係が存在する。

ゲンツェンのシーケント計算として知られる形式体系においては、証明とプログラムの対応関係を確立することができるが、それはヒルベルト流や自然演繹の場合のように、明確に定義された既存の計算モデルとの対応関係ではない。

シーケント計算は、左導入規則、右導入規則、および削除可能なカット規則の存在によって特徴付けられます。シーケント計算の構造は、いくつかの抽象機械の構造に近い計算体系と関連しています。非公式な対応関係は次のとおりです。

1970 年に発表された論文（ただし、1968 年にオーボ/トゥルクで開催された第 1 回スカンジナビア論理シンポジウムでの講演に基づく）の中で、ダグ・プラヴィッツは、最小および直観主義一階述語論理の自然演繹導出と、型付きラムダ計算に非常によく似た言語の構成項との間の準同型を定義した（この対応関係は、構成項の言語上でのこれらの論理の健全性の証明に由来する）。^{[ 15 ]}プラヴィッツの準同型はカリー・ハワード同型よりも強力ではないが、より強力な型言語では、依存型は欠けているものの、これも同型になる。プラヴィッツはおそらくハワードの研究を知らなかったと思われる。特に、彼の 1970 年の論文の基となった講演は、ハワードの原稿が出回る 1 年前に行われたからである。

NG de Bruijn は、定理チェッカーAutomathの証明を表すためにラムダ記法を使用し、命題を証明の「カテゴリ」として表現しました。これは 1960 年代後半、ハワードが原稿を書いたのと同じ時期のことでした。de Bruijn はハワードの研究を知らなかった可能性が高く、独自にこの対応関係を述べました。^{[ 16 ]}一部の研究者は、Curry–Howard 対応の代わりに Curry–Howard–de Bruijn 対応という用語を使用する傾向があります。

BHK解釈は直観主義的証明を関数として解釈するが、解釈に関連する関数のクラスを特定しない。この関数のクラスにラムダ計算を用いると、BHK解釈はハワードの自然演繹とラムダ計算の対応関係と同じことを示している。

クリーネの再帰的実現可能性は、直観主義算術の証明を、再帰関数と、その再帰関数が「実現する」、つまり、初期式の選言と存在量化子を正しくインスタンス化して式が真になることを表す式の証明のペアに分割する。

クライゼルの修正された実現可能性は直観主義高階述語論理に適用され、証明から帰納的に抽出された単純な型付きラムダ項が元の式を実現することを示している。命題論理の場合、これはハワードの主張と一致する。抽出されたラムダ項は証明自体（型なしラムダ項として見なされる）であり、実現可能性の主張は、抽出されたラムダ項が式が意味する型（型として見なされる）を持つという事実の言い換えである。

ゲーデルの弁証法解釈は、計算可能な関数を用いた直観主義算術（の拡張）を実現する。自然演繹の場合でさえ、ラムダ計算との関連性は不明瞭である。

ヨアヒム・ランベックは1970年代初頭に、直観主義命題論理の証明と型付き組み合わせ論理のコンビネータが、共通の等式理論であるデカルト閉圏の理論を共有していることを示した。現在、直観主義論理、型付きラムダ計算、デカルト閉圏の関係を指すのに、カリー・ハワード・ランベック対応という表現が使われることがある。この対応の下では、デカルト閉圏の対象は命題（型）として解釈でき、射は仮定の集合（型付けコンテキスト）を有効な帰結（型付き項）に写像する演繹として解釈できる。^{[ 17 ]}

ランベックの対応は等式理論の対応であり、ベータ還元や項正規化といった計算のダイナミクスを抽象化したもので、カリーやハワードの対応のように構造の構文的同一性を表すものではありません。つまり、デカルト閉圏における明確に定義された射の構造は、ヒルベルト型論理や自然演繹における対応する判断の証明の構造とは比較できません。例えば、射が正規化的であることを述べたり証明したり、チャーチ＝ロッサー型の定理を確立したり、「強く正規化する」デカルト閉圏について語ったりすることはできません。この区別を明確にするために、デカルト閉圏の根底にある構文構造を以下に言い換えます。

オブジェクト（命題／型）には以下が含まれます

• ${\displaystyle \top }$オブジェクトとして
• 与えられた${\displaystyle \alpha }$そして${\displaystyle \beta }$オブジェクトとして、${\displaystyle \alpha \times \beta }$そして${\displaystyle \alpha \rightarrow \beta }$オブジェクトとして。

形態（演繹/項）には以下が含まれる

• アイデンティティ:${\displaystyle {\text{id}}_{\alpha }:\alpha \to \alpha }$
• 構成: もし${\displaystyle t:\alpha \to \beta }$そして${\displaystyle u:\beta \to \gamma }$射である${\displaystyle u\circ t:\alpha \to \gamma }$射である
• 終端射：${\displaystyle \star _{\alpha }:\alpha \to \top }$
• 製品: もし${\displaystyle t:\alpha \to \beta }$そして${\displaystyle u:\alpha \to \gamma }$射は、${\displaystyle (t,u):\alpha \to \beta \times \gamma }$射である
• 予測:${\displaystyle \pi _{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha }$そして${\displaystyle \pi _{\alpha ,\beta ,2}:\alpha \times \beta \to \beta }$
• 評価：${\displaystyle {\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta }$
• カレー風味の場合:${\displaystyle t:\alpha \times \beta \to \gamma }$射である、${\displaystyle \lambda t:\alpha \to \beta \to \gamma }$これは射である。

上記の注釈と同様に、任意のデカルト閉圏における明確に定義された射（型付き項）は、以下の型付け規則に従って構築できます。通常の圏論的射の表記法${\displaystyle f:\alpha \to \beta }$入力コンテキスト表記に置き換えられます${\displaystyle \alpha \vdash f:\beta }$。

身元：

${\displaystyle {\frac {}{\alpha \vdash {\text{id}}:\alpha }}}$

構成：

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \beta \vdash u:\gamma }{\alpha \vdash u\circ t:\gamma }}}$

ユニットタイプ（端末オブジェクト）：

${\displaystyle {\frac {}{\alpha \vdash \star$ :\top }}}

直積：

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \alpha \vdash u:\gamma }{\alpha \vdash (t,u):\beta \times \gamma }}}$

左投影と右投影：

${\displaystyle {\frac {}{\alpha \times \beta ~\vdash ~\pi _{1}:\alpha }}\qquad {\frac {}{\alpha \times \beta ~\vdash ~\pi _{2}:\beta }}}$

カレー：

${\displaystyle {\frac {\alpha \times \beta ~\vdash ~t:\gamma }{\alpha \vdash \lambda t:\beta \to \gamma }}}$

応用：

${\displaystyle {\frac {}{(\alpha \rightarrow \beta )\times \alpha \vdash {\text{eval}}:\beta }}}$

最後に、このカテゴリーの方程式は次のようになります。

• ${\displaystyle {\text{id}}\circ t=t}$
• ${\displaystyle t\circ {\text{id}}=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star ={\text{id}}}$ （正しく入力されている場合）
• ${\displaystyle \star \circ u=\star }$
• ${\displaystyle \pi _{1}\circ (t,u)=t}$
• ${\displaystyle \pi _{2}\circ (t,u)=u}$
• ${\displaystyle (\pi _{1},\pi _{2})=id}$
• ${\displaystyle (t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)}$
• ${\displaystyle {\text{eval}}\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda {\text{eval}}={\text{id}}}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))}$

これらの式は以下を意味する。${\displaystyle \eta }$-法律:

• ${\displaystyle (\pi _{1}\circ t,\pi _{2}\circ t)=t}$
• ${\displaystyle \lambda ({\text{eval}}\circ (t\circ \pi _{1},\pi _{2}))=t}$

さて、あるtが存在して、${\displaystyle \alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta }$もし${\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta }$含意直観主義論理では証明可能である。

例として、定理α → αの証明を考えてみましょう。ラムダ計算では、これは恒等関数I = λx . xの型であり、組み合わせ論理では、恒等関数はK = λxy . xにS = λfgx . fx ( gx ) を 2 回適用することによって得られます。つまり、I = (( S K ) K )です。証明の説明として、これはα → αを証明するために以下の手順を使用できることを示しています。

• 式α、β → αおよびαを使用して 2 番目の公理スキームをインスタンス化し、( α → (( β → α ) → α )) → (( α → ( β → α )) → ( α → α ))の証明を取得します。
• 最初の公理スキームをαとβ → αで一度インスタンス化してα → (( β → α ) → α )の証明を得る。
• 最初の公理スキームをαとβで 2 回インスタンス化してα → ( β → α )の証明を得る。
• モーダス・ポネンスを2回適用して、 α → αの証明を得る。

一般的に、プログラムに（P Q）の形式のアプリケーションが含まれている場合は、以下の手順に従う必要があります。

1. まず、 PとQの型に対応する定理を証明します。
2. PがQに適用されているため、 Pの型はα → βの形である必要があり、 Qの型はαの形である必要があり、αとβはそれぞれ異なる値をとる。したがって、モーダス・ポネンス規則を用いて結論βを分離することができる。

より複雑な例として、 B関数に対応する定理を見てみましょう。B の型は( β → α ) → ( γ → β ) → γ → αです。Bは( S ( K S ) K )と同等です。これが定理( β → α ) → ( γ → β ) → γ → αの証明のロードマップです。

最初のステップは ( K S ) を構築することです。K 公理の前件を S 公理のように見せるために、 αを( α → β → γ ) → ( α → β ) → α → γに等しくし、βをδに等しくします(変数の衝突を避けるため)。

K  : α → β → α

K [ α = ( α → β → γ ) → ( α → β ) → α → γ , β = δ]  : (( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ

ここでの前件は単にSであるため、後件はモーダス・ポネンスを用いて分離することができる。

KS  : δ → ( α → β → γ ) → ( α → β ) → α → γ

これは ( K S )のタイプに対応する定理です。次に、この式にSを適用します。Sを次のようにします。

S  : ( α → β → γ ) → ( α → β ) → α → γ、

α = δ、β = α → β → γ、およびγ = ( α → β ) → α → γを代入すると、次のようになります。

S [ α = δ , β = α → β → γ , γ = ( α → β ) → α → γ ]  : ( δ → ( α → β → γ ) → ( α → β ) → α → γ ) → ( δ → ( α → β → γ )) → δ → ( α → β ) → α → γ

そして、後続項を切り離します。

S (KS)  : ( δ → α → β → γ ) → δ → ( α → β ) → α → γ

これは ( S ( K S ))型の公式です。この定理の特殊なケースはδ = ( β → γ )です。

S (KS) [ δ = β → γ ]  : (( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ

この最後の式はKに適用する必要があります。Kを再度特殊化し、今度はα を( β → γ )に、βをαに置き換えます。

K  : α → β → α

K [ α = β → γ , β = α ]  : ( β → γ ) → α → ( β → γ )

これは前の式の前件と同じなので、後件を切り離すと次のようになります。

S (KS) K  : ( β → γ ) → ( α → β ) → α → γ

変数αとγの名前を入れ替えると、

( β → α ) → ( γ → β ) → γ → α

それが、残された証明すべき点だった。

以下の図は、自然演繹における( β → α ) → ( γ → β ) → γ → αの証明を示し、それが( β → α ) → ( γ → β ) → γ → αという型のλ 式λ a .λ b .λ g .( a ( b g ))としてどのように解釈できるかを示しています。

 a:β → α、b:γ → β、g:γ ⊢ b : γ → β a:β → α、b:γ → β、g:γ ⊢ g : γ ——————————————————————————————————— ———————————————————————————————————————————————————————————————————— a:β → α、b:γ → β、g:γ ⊢ a : β → α a:β → α、b:γ → β、g:γ ⊢ bg : β ———————————————————————————————————————————————————————————————————————— a:β → α、b:γ → β、g:γ ⊢ a (bg) : α ———————————————————————————————————— a:β → α、b:γ → β ⊢ λ g. a (bg) : γ → α ———————————————————————————————————————— a:β → α ⊢ λ b. λ g. a (bg) : (γ → β) → γ → α ———————————————————————————————————— ⊢ λ a. λ ｂ． λ g. a (bg) : (β → α) → (γ → β) → γ → α

認知科学者は、高速で直感的な「システム 1」思考と、低速で熟慮的な「システム 2」思考を対比する二重過程理論を、大規模言語モデル(LLM) がどのように推論し、意思決定を行うかを分析するための枠組みとして使用してきました。^{[ 20 ]}また、一般的なエンジニアリング技術では、モデルが問題に取り組みながらコンピュータ コードを記述して実行することができます。テキストで直接答えを予測するのではなく、モデルは短いプログラムを記述し、外部のインタプリタがそれを実行し、モデルは結果を読み戻します。このように計算をインタプリタに委任すると、算術的および論理的エラーが減少することが示されています。^{[ 21 ] [ 22 ]}

カリー・ハワード対応は、実行中のコードが確立できることとできないことを明確にする。この対応の下では、証明は型付けされたプログラムであり、証明される命題はそのプログラムの型であるため、証明をチェックすることはプログラムの型チェックに相当する。論理的な内容は実行ではなく型システムにある。^{[ 23 ]} Python、SQL、JavaScriptなどの汎用言語は証明システムとして設計されたものではなく、形式化された数学の研究者は、証明とプログラムは根本的に異なる認識論的役割を果たすと主張しており、コーディングと証明の間の類似性は実際には限定的である。^{[ 24 ]}さらに、様相演算子□（必然性）と◇（可能性）は、主流のプログラミング言語にはない特殊な様相型システムでのみ計算解釈を得る。^{[ 11 ]}

Rocq、Lean、Agdaなどの証明支援システムは、対応関係に基づいて構築されています。定理は型として記述され、機械検証された証明はその型のプログラムです。LLMをこれらのシステム（Sympyなどの証明システムとともに、すべてコード実行として実行可能）と組み合わせることで、単に実行されるのではなく検証される推論が生成されます。Google DeepMindが開発したシステムAlphaProofは、強化学習を使用して、自動的に形式化された数千万の問題文のカリキュラムでLean証明を作成するモデルを訓練しました。生成されたすべての証明はLeanによって検証され、このシステムは2024年の国際数学オリンピックで銀メダルに相当するスコアを獲得しました。^{[ 25 ]}高階様相論理における機械検証された推論は、既存の証明システムの論理に様相論理を埋め込むことによっても実現できます。このアプローチは、ゲーデルの存在論的証明を形式的に検証するために使用されました。^{[ 26 ]}残された障害は自動形式化、つまり自然言語から形式言語への数学的記述の確実な翻訳である。^{[ 27 ] [ 28 ]}

一部の研究者は、この対応関係をLLM推論に直接適用することを提案している。2025年の提案の一つでは、モデルの思考連鎖の各ステップを型付き論理推論として扱い、型付き証明に変換される推論トレースが、その正しさの検証可能な証明書として機能する。^{[ 29 ]}しかし、この分野のレビューでは、証明生成はコード生成よりもLLMにとってかなり脆弱であることが判明しており、対応関係の優雅さだけではこのギャップを埋めることはできないと警告している。^{[ 24 ]}

• Curry, HB (1934-09-20). "組み合わせ論理における機能性" .米国科学アカデミー紀要. 20 (11): 584–90 . Bibcode : 1934PNAS...20..584C . doi : 10.1073/pnas.20.11.584 . ISSN 0027-8424 . PMC 1076489 . PMID 16577644 .   
• カリー、ハスケル B; フェイズ、ロバート (1958)。クレイグ、ウィリアム (編)。組み合わせ論理。論理学と数学の基礎に関する研究。第 1 巻。ノース ホランド出版。LCCN a59001593 ; クレイグ、ウィリアムによる 2 つのセクションを含む。9E 項を参照。 {{cite book}}: CS1 maint: postscript (リンク)
• De Bruijn, Nicolaas (1968), Automath, a language for mathematics , Department of Mathematics, Eindhoven University of Technology , TH-report 68-WSK-05. 改訂版として、2ページの解説付きで、Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970 , Springer Verlag, 1983, pp.  159–200 に再録。
• ハワード、ウィリアム A. (1980 年 9 月) [1969 年の原稿]、「構成における式を型として捉える概念」(PDF)、セルディン、ジョナサン P.、ヒンドリー、J. ロジャー(編)、『HB カリーへ：組み合わせ論理、ラムダ計算、形式主義に関するエッセイ』、アカデミック プレス、 479–490ページ、ISBN  978-0-12-349050-6
• Martin-Löf, Per ( 1975)、「直観主義型理論のモデルと定義的等価性の概念について」、Kanger, Stig (編)『第3回スカンジナビア論理シンポジウム議事録』、Elsevier、pp. 81–109 
• プラヴィッツ、ダグ（1970）「構成的意味論」、第1回スカンジナビア論理シンポジウム議事録、 96-114頁 

• モッジ、エウジェニオ（1991）「計算とモナドの概念」（PDF）、『情報と計算』、93（1）：55–92、doi：10.1016/0890-5401(91)90052-4
• Davies, Rowan; Pfenning, Fr​​ank (2001)、「段階的計算のモード解析」（PDF）、Journal of the ACM、48（3）：555–604、CiteSeerX 10.1.1.3.5442、doi：10.1145/382780.382785、S2CID 52148006  
• Pfenning, Fr​​ank; Davies, Rowan (2001)、「A Judgmental Reconstruction of Modal Logic」（PDF）、Mathematical Structures in Computer Science、11（4）：511–540、CiteSeerX 10.1.1.43.1611、doi：10.1017/S0960129501003322、S2CID 16467268  
• Benton、Bierman、de Paiva (1998)、「論理的観点からの計算型」、Journal of Functional Programming、8 (2): 177–193、CiteSeerX 10.1.1.258.6004、doi : 10.1017/s0956796898002998、S2CID 6149614  
• Griffin, Timothy G. (1990)、「制御の型としての式概念」、第17回ACMプログラミング言語原理シンポジウム（POPL '90）会議録、米国カリフォルニア州サンフランシスコ、1990年1月17～19日、pp. 47～ 57、doi : 10.1145/96709.96714、ISBN  978-0-89791-343-0S2CID 3005134​ 
• Parigot, Michel (1992)、「ラムダμ計算：古典的自然演繹のアルゴリズム的解釈」、国際論理プログラミングおよび自動推論会議：LPAR '92 議事録、ロシア、サンクトペテルブルク、Lecture Notes in Computer Science、第 624巻、Springer-Verlag、pp. 190–201、ISBN  978-3-540-55727-2
• Herbelin, Hugo (1995)、「Gentzen スタイルのシーケント計算構造と同型なラムダ計算構造」、Pacholski, Leszek、Tiuryn, Jerzy 編、『コンピュータサイエンス論理、第 8 回国際ワークショップ、CSL '94、ポーランド、カジミエシュ、1994 年 9 月 25 ～ 30 日、選集』、Lecture Notes in Computer Science、第 933 巻、Springer-Verlag、pp. 61～ 75、ISBN  978-3-540-60017-6
• Gabbay, Dov; de Queiroz, Ruy ( 1992 ). 「Curry–Howard 解釈を線形、関連、その他のリソース論理に拡張する」。Journal of Symbolic Logic。第 57 巻。Association  for Symbolic Logic。pp. 1319–1365。doi : 10.2307 /2275370。JSTOR 2275370。S2CID 7159005。   （ヘルシンキで開催されたLogic Colloquium '90で発表された論文の全文。要旨はJSL 56(3):1139–1140、1991年に掲載。）
• de Queiroz, Ruy; Gabbay, Dov (1994)、「ラベル付き演繹システムにおける等価性と命題等価性の機能的解釈」、Dekker, Paul; Stokhof, Martin (編)、『第9回アムステルダム・コロキウム議事録』、ILLC/アムステルダム大学哲学部、pp. 547–565、ISBN  978-90-74795-07-4
• de Queiroz, Ruy; Gabbay, Dov (1995)、「存在量化子の機能的解釈」、純粋および応用論理学研究会報、3 ( 2–3 ): 243–290、doi : 10.1093/jigpal/3.2-3.243（ 1991年ウプサラで開催された論理学コロキウムで発表された論文の全文。要旨はJSL 58(2):753–754、1993年に掲載。）
• de Queiroz, Ruy; Gabbay, Dov (1997)、「様相必然性の機能的解釈」、de Rijke, Maarten (編)、Advances in Intensional Logic、Applied Logic Series、vol.  7、Springer-Verlag、pp. 61–91、ISBN  978-0-7923-4711-8
• de Queiroz, Ruy; Gabbay, Dov (1999)、「ラベル付き自然演繹」、Ohlbach, Hans-Juergen; Reyle, Uwe (編)、Logic, Language and Reasoning. Essays in Honor of Dov Gabbay、Trends in Logic、第 7巻、Kluwer、pp. 173–250、ISBN  978-0-7923-5687-5
• de Oliveira, Anjolina; de Queiroz, Ruy (1999)、「ラベル付き自然演繹の等式断片の正規化手順」、Logic Journal of the Interest Group in Pure and Applied Logics、第7巻 、Oxford University Press、pp . 173–215 （レシフェで開催された第2回WoLLIC'95で発表された論文の全文。抄録はJournal of the Interest Group in Pure and Applied Logics 4(2):330–332、1996年に掲載。）
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Adapting Proofs-as-Programs: The Curry–Howard Protocol , Monographs in Computer Science, Springer , ISBN 978-0-387-23759-6本論文は、著者らが「カリー・ハワード・プロトコル」と呼ぶ手法を用いて、証明をプログラムとして扱うプログラム合成を、粗粒度かつ命令型のプログラム開発問題に適用する方法について論じている。また、コンピュータサイエンスの観点からカリー・ハワード対応関係についても考察している。
• de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011)、「直接計算の関数的解釈」、Electronic Notes in Theoretical Computer Science、269、Elsevier、19–40、doi：10.1016/j.entcs.2011.03.003（ブラジル、ナタールで開催されたLSFA 2010で発表された論文の全文。）

• de Queiroz, Ruy JGB (1994)、「正規化と言語ゲーム」、Dialectica、48 (2): 83–123、doi : 10.1111/j.1746-8361.1994.tb00107.x、JSTOR 42968904 （初期バージョンはパドヴァで開催されたLogic Colloquium '88で発表された。要旨はJSL 55:425、1990年に掲載。）
• de Queiroz, Ruy JGB (2001)、「意味、機能、目的、有用性、結果 ― 相互に関連する概念」、『純粋および応用論理学研究会誌』、第9巻、 693～ 734 ページ （初期版は、1989年8月13日～20日にキルヒベルク/ヴェクセルで開催された第14回国際ウィトゲンシュタイン・シンポジウム（生誕100周年記念）で発表された。）
• de Queiroz, Ruy JGB (2008)、「還元規則、使用としての意味、および証明論的意味論について」、Studia Logica、90 (2): 211–247、doi : 10.1007/s11225-008-9150-5、S2CID 11321602 
• Wadler, Philip (2015), Propositions as types , Communications of the ACM, 58(12), pp. 75–84.

• De Bruijn、Nicolaas Govert (1995)、「数学における型の役割について」(PDF)、Groote、Philippe de (編)、De Groote 1995  、 27–54ページ、de Bruijn 自身による寄稿。
• Geuvers, Herman (1995)、「構成の計算と高階論理」、De Groote 1995、pp.  139–191本書には、カリーとハワードの往復書簡に関する簡潔な序論が含まれている。
• Gallier, Jean H. (1995)、「証明とラムダ項の対応関係について」（PDF）、De Groote 1995、pp.  55–138、2017年7月5日にオリジナル（PDF）からアーカイブ済み本書には、カリーとハワードの往復書簡に関する簡潔な序論が含まれている。
• ゴールドブラット、ロバート（2006）。「直観主義的様相としてのグロタンディーク位相」（PDF）。ドヴ・M・ギャベイ、ジョン・ウッズ編『論理学史ハンドブック』第7巻： 20世紀の論理と様相アムステルダム：エルゼビア。76 ～ 81ページ。ISBN  978-0-444-51622-0。
• Wadler, Philip (2014)、「型としての命題」（PDF）、Communications of the ACM、58（12）：75–84、doi：10.1145/2699407、S2CID 11957500 

• コッケ、ボブ；キッシンジャー、アレックス（2017）。量子過程の図解。ケンブリッジ大学出版局。ISBN 978-1-107-10422-8。
• ケネディ、ジュリエット、コサック、ローマン編 (2011) 『集合論、算術、数学の基礎：定理、哲学』ケンブリッジ大学出版局。ISBN 978-1-107-00804-5。
• Baez, John C.; Stay, Mike (2011). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF) . In Coecke, Bob (ed.). New Structures for Physics . Lecture Notes in Physics. Vol.  813. Berlin: Springer. pp. 95– 174. arXiv : 0903.0340 . 
• カサディオ、クラウディア；スコット、フィリップ・J. (2021).ヨアヒム・ランベック：数学、論理学、言語学の相互作用. シュプリンガー. ISBN 978-3-030-66545-6。
• ランベック、ヨアヒム；スコット、PJ（1989）。高階範疇論理入門。ケンブリッジ、ニューヨーク、ポートチェスターほか：ケンブリッジ大学出版局。ISBN 0521356539。
• デ・グルーテ、フィリップ編（1995）、「The Curry-Howard Isomorphism」、Cahiers du Centre de Logique (Université catholique de Louvain)、vol.  8、アカデミア-ブリュイラン、ISBN 978-2-87209-363-2本書は、カリー＝フェイズとハワードの先駆的な論文、デ・ブルインの論文、その他いくつかの論文を収録している。
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998],カリー・ハワード同型性に関する講義, 論理学と数学の基礎に関する研究, 第 149巻, Elsevier Science , CiteSeerX 10.1.1.17.7385 , ISBN  978-0-444-52077-7証明論と型理論に関するノート。これには、カリー・ハワード対応の解説が含まれており、特に式を型として扱う対応に焦点を当てている。
• ジラール、ジャン＝イヴ（1987–1990）、『証明と型』、ケンブリッジ理論計算機科学叢書、第 7巻、イヴ・ラフォンとポール・テイラーによる翻訳および付録、ケンブリッジ大学出版局、ISBN 0-521-37181-32008年4月18日にオリジナルからアーカイブされました証明論に関する注釈と、カリー・ハワード間の通信の紹介。
• トンプソン、サイモン（1991）、『型理論と関数型プログラミング』、アディソン・ウェスリー、ISBN 0-201-41667-0
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Adapting Proofs-as-Programs: The Curry–Howard Protocol , Monographs in Computer Science, Springer , ISBN 978-0-387-23759-6本論文は、著者らが「カリー・ハワード・プロトコル」と呼ぶ手法を用いて、証明をプログラムとして扱うプログラム合成を、粗粒度かつ命令型のプログラム開発問題に適用する方法について論じている。また、コンピュータサイエンスの観点からカリー・ハワード対応関係についても考察している。
• Binard, F.; Felty, A. (2008)、「多相型と高階関数を用いた遺伝的プログラミング」（PDF）、第10回遺伝的および進化的計算に関する年次会議議事録、Association for Computing Machinery、pp. 1187–94、doi : 10.1145/1389095.1389330、ISBN  9781605581309S2CID 3669630​ 
• de Queiroz, Ruy JGB; de Oliveira, Anjolina G.; Gabbay, Dov M. (2011), The Functional Interpretation of Logical Deduction , Advances in Logic, vol.  5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1