ジャン＝イヴ・ジラール

System Fと強正規化性

ジラールは1970年代初頭、型についての全称量化をそなえた多相型付きラムダ計算の体系を研究した。この体系はSystem F、または二階ラムダ計算と呼ばれる。ジョン・C・レイノルズも独立に同種の体系を発見しており、現在では両者の仕事が多相型システムの初期の研究として位置づけられている^[9]。

ジラールはSystem Fの型が付く項について強正規化性を証明した。強正規化性とは、対象となる項から始まる簡約の列が、簡約をどの順序で選んでも無限には続かないという性質である。この研究は、二階論理におけるカット除去や型付き計算の停止性を扱う証明論の発展に関係している^[6][9]。

また1972年には、System Fとは異なる型体系System Uで矛盾を導けることを示した。この結果は「ジラールのパラドックス」（Girard's paradox）として知られ、強力な型の宇宙を導入した体系の無矛盾性を考える際に参照される^[10]。

順序数と証明論

ジラールは、証明の複雑さを順序数によって解析する研究にも取り組んだ。1981年の論文「Π₂¹-logic. I: Dilators」では、順序数上の関手に関する構成であるdilatorを用いた証明論を展開した。この方向の研究では、序数記法と順序数の演算を関手的に取り扱う方法が検討された^[11][3]。

1984年にはジャクリーヌ・ヴォジエイユ（Jacqueline Vauzeilles）との共著論文で、証明論に用いられるヴェブレン階層の関手的構成を論じた。dilatorによる順序数の扱いは、その後も証明論と関連する研究の対象となっている^[12][3]。

整合空間と線形論理

1980年代には、型付きラムダ計算の表示的意味論にも取り組んだ。特に整合空間（coherence space）を用いた意味論の研究は、後に線形論理の成立につながった。1986年の論文「The system F of variable types, fifteen years later」では、System Fの意味論を再検討している^[13][2]。

1987年、論文「Linear logic」において線形論理を導入した。通常の古典論理や直観主義論理では、証明の前提を複製して使う縮約規則や、使わない前提を付加する弱化規則が広く認められる。線形論理では、これらの構造規則をすべての論理式に無条件で適用することはせず、指数演算子（!、?）によってその使用を制御する。その結果、従来の論理では同一視されていた乗法的結合子と加法的結合子が区別される^[14][2]。

線形論理は、前提となる式を証明中でどのように使用するかを明示的に扱うための体系であり、論理学だけでなく、プログラミング言語の型システム、論理プログラミング、計算資源の解析などにも応用されている^[2]。

証明ネット

ジラールは線形論理の研究で、証明ネット（proof net）も導入した。シーケント計算では、互いに独立した推論規則を適用する順序が違うだけでも異なる証明図となる。証明ネットは、そのような規則の適用順序に由来する差異の一部を捨象し、証明をグラフ状の対象として表現する方法である^[14][2]。とりわけ線形論理の乗法的断片については、グラフが適切な証明を表しているかを判定する条件や、グラフ上での局所的なカット除去が研究されてきた。後年、ヴィンセント・ダノス（Vincent Danos）とローラン・レニエ（Laurent Regnier）らによって、その正当性判定の研究が発展した^[2][15]。

相互作用の幾何

1980年代末から、ジラールは相互作用の幾何（geometry of interaction、GoI）と呼ばれる研究を進めた。これは証明のカット除去に伴う計算を、証明図を書き換える操作だけでなく、作用素の合成やフィードバックを用いた相互作用として捉える意味論的な研究である。1989年の「Geometry of Interaction I: Interpretation of System F」では、System Fの解釈が提示された^[16]。

その後も相互作用の幾何に関する論文を発表し、2011年の「Geometry of Interaction V: Logic in the hyperfinite factor」では、作用素環を用いた枠組みを展開している^[17]。

ルディクス

2001年の論文「Locus Solum: From the rules of logic to the logic of rules」で、ルディクス（ludics）と呼ばれる証明論へのアプローチを提案した。ルディクスでは、デザイン（design）と呼ばれる対象の相互作用や、その直交性（orthogonality）にもとづいて定められる振る舞い（behaviour）を用い、論理式や証明の構造を扱う^[18][19]。ジラールは2003年の「From foundations to ludics」で、この構想を数学基礎論の問題と関連づけて論じている。ルディクスは、線形論理や証明ネット、相互作用にもとづく論理の研究と関係する一方、それらと同一の形式体系ではない^[19]。

超越論的シンタクス

2010年代以降には、「超越論的シンタクス」（transcendental syntax）と題した研究を発表している。2017年刊行の「Transcendental syntax I: deterministic case」では、イマヌエル・カントの分析的／総合的という区別にも言及しつつ、証明ネットなどを手がかりとして、論理的帰結や証明の正当性をいかなる構文論的構造から説明できるかを検討している^[20]。