用語・記法・文献の概念地図

Gottlob Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Louis Nebert, Halle, 1879, 原著デジタル版。量化、関係、判断を 二次元記法で組織した原典。現代の ∀ 記法へ翻訳するだけでは、判断線など原体系の 構造を失うため、現代述語論理そのものとして読まない。

Richard Dedekind, Was sind und was sollen die Zahlen?, Vieweg, Braunschweig, 1888, ETHデジタル版。 自然数を単純無限系と写像により特徴づけ、再帰的定義と帰納的推論を基礎づける原典。 Leanの Nat 宣言の仕様書ではない。

Giuseppe Peano, Arithmetices principia, nova methodo exposita, Fratres Bocca, Turin, 1889, EuDML書誌・本文。 自然数算術を記号的公理体系として提示した原典。現在「Peano公理」と呼ばれる複数の 一階・二階定式化との差を確認して読む。

Ernst Zermelo, “Untersuchungen über die Grundlagen der Mengenlehre I,” Mathematische Annalen 65, 261–281, 1908, EuDML本文・書誌。最初の集合論公理化の原典。 本書の述語集合 α → Prop はZermelo集合論の集合概念の実装ではない。

Georg Cantor, “Ueber eine Eigenschaft des Inbegriffes aller reellen algebraischen Zahlen,” Journal für die reine und angewandte Mathematik 77, 258–262, 1874, EuDML本文・書誌。代数的数の可算性と 実数の非可算性を扱う最初期の原典。後世の一般的なCantorの定理や集合論公理系を同論文へ そのまま帰属させない。

Max Zorn, “A Remark on Method in Transfinite Algebra,” Bulletin of the American Mathematical Society 41, 667–670, 1935, DOI: 10.1090/S0002-9904-1935-06166-X。 後にZornの補題と呼ばれる極大原理を代数学の方法として提示した原典。選択公理との同値性は 集合論的背景を明示して別に扱う。

Alfred Tarski, “A Lattice-Theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5(2), 285–309, 1955, DOI: 10.2140/pjm.1955.5.285。完備格子上の 単調写像とその不動点集合を扱う基準文献。プログラム意味論における連続性や計算可能な反復近似は 追加の構造であり、この定理だけへ帰属させない。

Dana S. Scott, Outline of a Mathematical Theory of Computation, Technical Monograph PRG-2, Oxford University Computing Laboratory, 1970, Oxford書誌・公開版。データを 近似順序で捉え、再帰とラムダ計算の数学的意味論を構成する研究計画を提示する一次資料。

Dana S. Scott, “Continuous Lattices,” in Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, 97–136, 1972, DOI: 10.1007/BFb0073967。連続格子、位相、関数空間を 扱う基準文献。本書のω-CPOだけの定義を同論文の全理論と同一視しない。

Bertrand Russell, “Mathematical Logic as Based on the Theory of Types,” American Journal of Mathematics 30(3), 222–262, 1908, DOI: 10.2307/2272708。 分岐型理論の一次資料。Leanの宇宙階層の直接仕様ではない。

Alonzo Church, “A Set of Postulates for the Foundation of Logic,” Annals of Mathematics 33(2), 346–366, 1932, DOI: 10.2307/1968337。関数抽象と変換を含む初期の 論理体系。後に逆理が判明した体系全体と、現在いうラムダ計算の計算核を区別する。

Alonzo Church, “A Set of Postulates for the Foundation of Logic (Second Paper),” Annals of Mathematics 34(4), 839–864, 1933, DOI: 10.2307/1968702。1932年論文に続く第二論文。 二論文を一つの完成済みな現代的非型付きラムダ計算として遡及的に読まない。

Alonzo Church, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics 58(2), 345–363, 1936, DOI: 10.2307/2371045。ラムダ定義可能性を用いて 有効計算可能性を定式化し、決定不能性を示した一次資料。

Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic 5(2), 56–68, 1940, 原論文PDF。 単純型理論とラムダ変換を結びつけた基準文献。

Per Martin-Löf, Intuitionistic Type Theory, notes by Giovanni Sambin, Bibliopolis, 1984, 公開PDF。 命題・型、Π型・Σ型、同一性型、帰納的対象を理解する歴史的基準点。Leanの型理論と 規則が全て一致するという意味ではない。

John Cartmell, Generalised Algebraic Theories and Contextual Categories, D.Phil. thesis, University of Oxford, 1978, 著者公開版。依存するsortを持つ一般化代数理論と、 文脈・代入を表すcontextual categoryを構築した一次資料。1986年の論文版と区別する。

Peter Dybjer, “Internal Type Theory,” in Types for Proofs and Programs, TYPES ’95, Lecture Notes in Computer Science 1158, 120–134, Springer, 1996, DOI: 10.1007/3-540-61780-9_66。 category with familiesを導入し、依存型の構文に近い圏論的モデルとcoherence問題を扱う一次論文。

N. G. de Bruijn, “Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church–Rosser Theorem,” Indagationes Mathematicae (Proceedings) 75(5), 381–392, 1972, DOI: 10.1016/1385-7258(72)90034-0。 束縛変数名を束縛子までの距離で置き換える記法の一次資料。

Gordon D. Plotkin, “Call-by-Name, Call-by-Value and the λ-Calculus,” Theoretical Computer Science 1(2), 125–159, 1975, DOI: 10.1016/0304-3975(75)90017-1。 名前呼び・値呼びの評価とプログラミング言語の対応を比較する基準文献。本書のLeanによる 一段実行関数を原論文の定義そのものとはみなさない。

Roberto M. Amadio and Luca Cardelli, “Subtyping Recursive Types,” ACM Transactions on Programming Languages and Systems 15(4), 575–631, 1993, DOI: 10.1145/155183.155231。再帰型の同値と 部分型を、規則、アルゴリズム、無限木の意味論の対応として研究する。本書のiso-recursive型の 小ステップ体系は同論文の部分型計算そのものではない。

Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to Type Soundness,” Information and Computation 115(1), 38–94, 1994, DOI: 10.1006/inco.1994.1093。 操作的意味論、subject reduction、進行型の議論をプログラミング言語の型健全性へ適用する 基準文献。本章の純粋STLCを同論文のStandard ML核と同一視しない。

William W. Tait, “Intensional Interpretations of Functionals of Finite Type I,” Journal of Symbolic Logic 32(2), 198–212, 1967, DOI: 10.2307/2271658。有限型の汎関数に対する 解釈を展開する一次資料。後世のreducibility candidatesや本章のLean定義と同一視せず、 正規化証明法の系譜を読む基準点とする。

John C. Reynolds, “Types, Abstraction and Parametric Polymorphism,” in Information Processing 83, IFIP, 513–523, 1983。 多相型の関係解釈と抽象化定理をプログラミング言語の文脈で展開する一次資料。後世の “theorems for free”という標語や本書のLean構造を同論文へそのまま帰属させない。

Philip Wadler, “Theorems for Free!,” in Proceedings of FPCA ’89, 347–359, ACM Press, 1989, DOI: 10.1145/99370.99404。Reynoldsの 抽象化定理から多相プログラムの方程式を導く方法を展開した基準文献。適用可能性は言語の 効果・部分性・型機構の仮定とともに読む。

Thierry Coquand and Gérard Huet, “The Calculus of Constructions,” Information and Computation 76(2–3), 95–120, 1988, DOI: 10.1016/0890-5401(88)90005-3。 構成計算（CoC）の基本理論を提示した基準文献。帰納型やLean固有のkernel機能を含む 現代の体系と同一ではない。

Henk Barendregt, “Introduction to Generalized Type Systems,” Journal of Functional Programming 1(2), 125–154, 1991, DOI: 10.1017/S0956796800020025。 型付きラムダ計算を一般化型システムとして統一し、CoCを八頂点のラムダ・キューブとして 分析した一次資料。

Martin Hofmann and Thomas Streicher, “The Groupoid Interpretation of Type Theory,” in Twenty-Five Years of Constructive Type Theory, Oxford Logic Guides 36, 83–111, 1998, DOI: 10.1093/oso/9780198501275.003.0008。 内包的型理論の同一性型を群oidで解釈し、同一性証明の一意性が一般には導けないことを示す 基準文献。後の一価性公理そのものを述べた文献ではない。

Steve Awodey and Michael A. Warren, “Homotopy Theoretic Models of Identity Types,” Mathematical Proceedings of the Cambridge Philosophical Society 146(1), 45–55, 2009, DOI: 10.1017/S0305004108001783。 model categoryにおけるMartin-Löf型理論のモデルを構成し、同一性型とホモトピー論の接続を 展開する。一価的基礎全体の標準教科書とは役割が異なる。

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013, 公式公開版。一価性、高次帰納型、ホモトピーレベルを 系統的に扱う共同執筆の標準文献。Lean 4の Eq : Prop の仕様書ではない。

Gerhard Gentzen, “Untersuchungen über das logische Schließen I–II,” Mathematische Zeitschrift 39, 176–210 and 405–431, 1935, Part I DOI: 10.1007/BF01201353, Part II DOI: 10.1007/BF01201363。自然演繹と シーケント計算を導入し、正規化とcut除去へ至る証明論的構造を扱う原典。現在のLeanの tactic状態や証明項をGentzenの原体系そのものとはみなさない。

Arend Heyting, “Die formalen Regeln der intuitionistischen Logik I–III,” Sitzungsberichte der Preußischen Akademie der Wissenschaften, 42–56, 57–71, 158–169, 1930, 書誌情報。 直観主義命題・述語論理の形式化。Brouwerの研究計画そのものとは区別する。

A. Kolmogorov, “Zur Deutung der intuitionistischen Logik,” Mathematische Zeitschrift 35, 58–65, 1932, EuDML本文・書誌。直観主義論理を問題と解法として読む 解釈の一次資料。後世の “BHK” という総称は同時代の固有名ではない。

H. B. Curry, “Functionality in Combinatory Logic,” PNAS 20(11), 584–590, 1934, DOI: 10.1073/pnas.20.11.584。 組合せ子の型と含意論理の対応の早い一次資料。

William A. Howard, “The Formulae-as-Types Notion of Construction,” in To H. B. Curry, 479–490, Academic Press, 1980, 原論文PDF。原稿は1969年。Curryの結果を 単に再掲したのではなく、自然演繹と構成の対応を広げる。

J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle,” Journal of the ACM 12(1), 23–41, 1965, DOI: 10.1145/321250.321253。resolution原理による 自動推論の一部として単一化アルゴリズムを提示した一次資料。後世の型推論器に現れる単一化だけを 切り出して原論文全体とみなさない。

J. Roger Hindley, “The Principal Type-Scheme of an Object in Combinatory Logic,” Transactions of the American Mathematical Society 146, 29–60, 1969, DOI: 10.2307/1995158。組合せ論理の 対象に対するprincipal type-schemeを扱う。MLの型推論アルゴリズムを記述した論文ではない。

Robin Milner, “A Theory of Type Polymorphism in Programming,” Journal of Computer and System Sciences 17(3), 348–375, 1978, DOI: 10.1016/0022-0000(78)90014-4。 プログラミング言語の多相型規律、Algorithm W、意味論的・構文的健全性を提示する一次資料。

Luís Damas and Robin Milner, “Principal Type-Schemes for Functional Programs,” POPL ’82, 207–212, 1982, DOI: 10.1145/582153.582176。関数型プログラムの principal type-schemeを研究する基準文献。依存型や型クラスを含むLeanのelaborationへ 完全性をそのまま移せるわけではない。

Jana Dunfield and Neelakantan R. Krishnaswami, “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism,” ICFP ’13, 429–442, 2013, DOI: 10.1145/2500365.2500582。 高階ランク多相を対象に、証明論に基づく双方向型付けと健全・完全なアルゴリズムを与える。 本書の単相の合成・検査判断は、その情報流を理解するための限定された例である。

Tim Freeman and Frank Pfenning, “Refinement Types for ML (Extended Abstract),” PLDI ’91, 268–277, 1991, 著者側書誌。 “refinement types” をMLの型システムとして定式化した代表的な初期文献。Leanの Subtype と同じ型検査方式ではない。

Peter Dybjer, “Inductive Families,” Formal Aspects of Computing 6, 440–465, 1994, DOI: 10.1007/BF01211308。 Martin-Löf型理論における一般化された帰納族の形成・導入・再帰を扱う。

Philip Wadler and Stephen Blott, “How to Make Ad-hoc Polymorphism Less Ad Hoc,” POPL ’89, 60–76, 1989, DOI: 10.1145/75277.75283。 Hindley–Milner系に型クラスを導入した一次資料。Leanのインスタンス探索はこの発想を 発展させているが、同じ推論系ではない。

Samuel Eilenberg and Saunders Mac Lane, “General Theory of Natural Equivalences,” Transactions of the American Mathematical Society 58, 231–294, 1945, AMS原論文PDF。 圏、関手、自然同値を体系的に導入した一次資料。現在の教科書的な普遍性・随伴・極限の 全体系をこの一論文へ遡及的に帰属させない。

Nobuo Yoneda, “On the Homology Theory of Modules,” Journal of the Faculty of Science, University of Tokyo, Section I 7, 193–227, 1954, Stacks Project書誌。 加群のホモロジー理論を主題とする一次資料で、その中の補題が後に米田の補題として 一般圏論の中心定理になった。論文全体を現代の米田埋め込みだけへ還元しない。

Alexander Grothendieck, “Sur quelques points d'algèbre homologique,” Tôhoku Mathematical Journal, Second Series 9(2), 119–183, 1957, DOI: 10.2748/tmj/1178244839。アーベル圏と 導来関手の一般理論を構築し、アーベル群の層を主要例として扱う一次資料。後のサイトと Grothendieckトポスの全理論を、この論文へ遡及的に帰属させない。

Daniel M. Kan, “Adjoint Functors,” Transactions of the American Mathematical Society 87, 294–329, 1958, DOI: 10.1090/S0002-9947-1958-0131451-0。 随伴関手と後にKan拡張と呼ばれる構成を導入した一次資料。現代の単位・余単位による 定式化との記法差は [MAC98] と照合する。

Saunders Mac Lane, “Natural Associativity and Commutativity,” Rice University Studies 49(4), 28–46, 1963, 原論文PDF。 自然な結合性・可換性とその整合条件を研究した一次資料。現在のモノイダル圏の定義全体や mathlibの正規化手続を同論文へそのまま遡及させない。

Samuel Eilenberg and G. M. Kelly, “Closed Categories,” in Proceedings of the Conference on Categorical Algebra, La Jolla 1965, Springer, 421–562, 1966, DOI: 10.1007/978-3-642-99902-4。 閉圏と内部homを体系化した一次資料。後の [KEL82] における豊穣圏論全体の定式化とは時期と範囲を区別する。

Heinrich Kleisli, “Every Standard Construction Is Induced by a Pair of Adjoint Functors,” Proceedings of the American Mathematical Society 16, 544–546, 1965, DOI: 10.1090/S0002-9939-1965-0177024-4。 当時standard constructionなどと呼ばれた構造から随伴を構成する一次資料。

Samuel Eilenberg and John C. Moore, “Adjoint Functors and Triples,” Illinois Journal of Mathematics 9, 381–398, 1965, DOI: 10.1215/ijm/1256068141。 tripleとその代数の圏を随伴との関係から研究した一次資料。後代の “monad” という名称と 現行記法は [MAC98] と区別して読む。

Jonathan Mock Beck, Triples, Algebras and Cohomology, PhD thesis, Columbia University, 1967; reprinted in Reprints in Theory and Applications of Categories 2, 1–59, 2003, TAC公開版。 tripleによるコホモロジーと代数を展開する一次資料。2003年版の編集者序文が1964年草稿の 流通を記録するため、原稿年、学位論文年、再刊年を区別する。現代のBeck型定理の諸版は 仮定が異なるので、単一の現行定式化を無注釈で同論文へ帰属させない。

Joachim Lambek, “A Fixpoint Theorem for Complete Categories,” Mathematische Zeitschrift 103, 151–161, 1968, DOI: 10.1007/BF01110627。 圏論的な不動点定理を扱う一次資料。始代数の構造射が同型になる、現在Lambekの補題と 呼ばれる主張を、後代のデータ型意味論だけへ限定して読まない。

Alexander Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Lecture Notes in Mathematics 224, Springer, 1971, Stacks Project書誌。第VI exposé “Catégories fibrées et descente” はファイバー圏、Cartesian射、降下を代数幾何の文脈で 体系化する一次資料。セミナー実施時期と刊行年、および後の型理論的解釈を区別する。

Jean Bénabou, “Fibered Categories and the Foundations of Naive Category Theory,” Journal of Symbolic Logic 50(1), 10–37, 1985, DOI: 10.2307/2273784。ファイバー圏を圏論の 基礎づけと結びつけて展開する一次論文。Grothendieckの幾何学的使用と目的を区別して読む。

R. A. G. Seely, “Locally Cartesian Closed Categories and Type Theory,” Mathematical Proceedings of the Cambridge Philosophical Society 95(1), 33–48, 1984, DOI: 10.1017/S0305004100061284。 局所デカルト閉圏とMartin-Löf型理論の対応を体系的に論じる一次論文。後続研究による coherence条件の修正や双圏同値の精密化を、原論文の主張と区別して読む。

Jean-Yves Girard, “Linear Logic,” Theoretical Computer Science 50(1), 1–102, 1987, DOI: 10.1016/0304-3975(87)90045-4。 線形論理を、乗法的・加法的・指数的結合子、線形否定、cut除去、coherent space意味論とともに 導入した一次論文。後世の資源解釈だけへ論文全体を還元せず、証明論と意味論の構成を区別して読む。

R. A. G. Seely, “Linear Logic, *-Autonomous Categories and Cofree Coalgebras,” in Categories in Computer Science and Logic, Contemporary Mathematics 92, 371–382, American Mathematical Society, 1989, DOI: 10.1090/conm/092/1003210。 *-自律圏と余自由余代数による線形論理の圏論モデルを論じる一次資料。後続研究で修正・精密化された Seely categoryの定義と、原論文の定式化を同一視しない。

P. N. Benton, “A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models,” in Computer Science Logic, CSL ’94, Lecture Notes in Computer Science 933, 121–135, Springer, 1995, DOI: 10.1007/BFb0022251。 デカルト閉な非線形世界と対称モノイダル閉な線形世界を随伴で結ぶLNL体系の一次論文。1994年の 会議と1995年の選集刊行、および同題の長い技術報告を区別する。

Eugenio Moggi, “Notions of Computation and Monads,” Information and Computation 93(1), 55–92, 1991, DOI: 10.1016/0890-5401(91)90052-4。 値と計算を区別する計算的ラムダ計算を導入し、複数の計算概念を強いモナドの圏論的意味論で 統一した一次論文。1989年の会議論文と1991年の拡張誌上版、および後代の言語APIを区別する。

Gordon Plotkin and John Power, “Algebraic Operations and Generic Effects,” Applied Categorical Structures 11(1), 69–94, 2003, DOI: 10.1023/A:1023064908962。 代数的演算とgeneric effectの対応を、強いモナドと豊穣圏論の設定で研究した一次論文。 2001年の先行会議論文と、題名・範囲を同一視しない。

Gordon Plotkin and Matija Pretnar, “Handling Algebraic Effects,” Logical Methods in Computer Science 9(4), article 23, 2013, DOI: 10.2168/LMCS-9(4:23)2013。 自由モデルと準同型によって例外処理を一般の代数的効果ハンドラへ拡張した一次論文。2009年の “Handlers of Algebraic Effects” 会議版と、題名・内容・刊行年を区別する。

Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, eds., Théorie des topos et cohomologie étale des schémas, Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964, Lecture Notes in Mathematics 269, 270, 305, Springer, 1972–1973, Tome 2, DOI: 10.1007/BFb0061319。サイト、トポス、 降下、エタール・コホモロジーを展開する複数巻の基準的な一次資料。各 exposé の著者と 巻を確認し、全内容を単著の一時点の定義として引用しない。

F. William Lawvere, “Quantifiers and Sheaves,” in Actes du Congrès International des Mathématiciens, Nice 1970, vol. 1, 329–334, Gauthier-Villars, 1971。量化を再添字付けの随伴として捉え、層と論理を結ぶ一次資料。 1970年の講演と1971年の会議録刊行を区別する。

Myles Tierney, “Sheaf Theory and the Continuum Hypothesis,” in Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, 13–42, Springer, 1972, DOI: 10.1007/BFb0073963。層トポスの内部論理を 集合論の独立性へ応用する一次資料。後代に整理された初等トポスの標準定義全体を、この論文だけへ帰属させない。

Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright, “Initial Algebra Semantics and Continuous Algebras,” Journal of the ACM 24(1), 68–95, 1977, DOI: 10.1145/321992.321997。始代数意味論を 連続代数と結び、代数的仕様とプログラム意味論へ展開した一次資料。Leanの帰納型生成機構や 依存除去原理を、この論文の定式化とそのまま同一視しない。

J. J. M. M. Rutten, “Universal Coalgebra: A Theory of Systems,” Theoretical Computer Science 249(1), 3–80, 2000, CWI書誌・著者公開版。状態遷移系、双模倣、終余代数を 普遍余代数の枠組みで統一する基準的な研究論文。Leanの再帰定義機構の仕様ではない。

M. B. Smyth and G. D. Plotkin, “The Category-Theoretic Solution of Recursive Domain Equations,” SIAM Journal on Computing 11(4), 761–783, 1982, DOI: 10.1137/0211062。CPO上の連続写像の最小不動点を、 順序豊穣圏上の連続関手と埋込みの圏へ拡張する一次論文。1979年の投稿と1982年の刊行を区別する。

Peter J. Freyd, “Algebraically Complete Categories,” in Category Theory: Proceedings of the International Conference Held in Como, Italy, July 22–28, 1990, Lecture Notes in Mathematics 1488, 95–104, Springer, 1991, 会議録DOI: 10.1007/BFb0084207。代数的完備性を 一般の圏論的条件として研究する一次資料。1990年の会議と1991年の刊行を区別する。

Nicola Gambino and Martin Hyland, “Wellfounded Trees and Dependent Polynomial Functors,” in Types for Proofs and Programs, TYPES 2003, Lecture Notes in Computer Science 3085, 210–225, Springer, 2004, DOI: 10.1007/978-3-540-24849-1_14。 W型を局所デカルト閉圏の依存多項式関手と結び、その始代数を研究する一次論文。本書の Type 上の一変数多項式関手は、この一般理論の全てを形式化するものではない。

Jiří Adámek, Stefan Milius, and Lawrence S. Moss, Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors, Cambridge Tracts in Theoretical Computer Science 62, Cambridge University Press, 2025, DOI: 10.1017/9781108884112。標準鎖による始代数・ 終余代数の構成、関手の不動点、完備半順序や距離空間との接続を研究書として追う文献。

Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989, corrected reprint 1990, 著者公開PDF。自然演繹、正規化、 単純型付きラムダ計算、System Fをproof theory側から読む標準文献。

Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, 出版社書誌。 構文、操作的意味論、型判断、保存・進行を論文標準の推論規則で学ぶための教科書。

Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016, DOI: 10.1017/CBO9781316576892。 判断と規則を中心にプログラミング言語の静的・動的意味論を構成する研究書。第2版は type refinementsも扱う。

J. Lambek and P. J. Scott, Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics 7, Cambridge University Press, 1986, 書誌情報。 型付きラムダ計算・高階論理とCartesian closed categoryの対応を学ぶ標準文献。

Bart Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North-Holland, Elsevier, 1999, 著者書誌。ファイブレーションを統一概念として、 述語論理・依存型理論・圏論的意味論を体系化する標準研究書。原典ではなく現代的定式化の参照に用いる。

Martin Hofmann, “Syntax and Semantics of Dependent Types,” in Andrew M. Pitts and Peter Dybjer, eds., Semantics and Logics of Computation, 79–130, Cambridge University Press, 1997, DOI: 10.1017/CBO9780511526619.004。 依存型構文と抽象的意味論、型形成子、外延的・内包的構成の関係を読む標準的な章。

Saunders Mac Lane, Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics 5, Springer, 1998。圏論の標準的な研究語彙と 普遍構成を参照する文献。初版は1971年であり、版を区別する。

G. M. Kelly, Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Note Series 64, Cambridge University Press, 1982; corrected reprint, Reprints in Theory and Applications of Categories 10, 1–136, 2005, TAC公開版。豊穣圏、 豊穣化されたend・coend、Kan拡張を体系的に扱う研究書。1982年版と訂正を含む2005年再刊を区別する。

Saunders Mac Lane and Ieke Moerdijk, Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Universitext, Springer, 1992。前層、篩、 Grothendieck位相、層化、トポスを現代的な圏論の記法で結び直す標準研究書。SGA 4の 一次資料としてではなく、定義間の同値と論理への接続を学ぶために用いる。

Tom Leinster, Basic Category Theory, Cambridge Studies in Advanced Mathematics 143, Cambridge University Press, 2014, DOI: 10.1017/CBO9781107360068。 普遍性を随伴・表現可能関手・極限の三方向から読み直すための導入的研究書。

Lean project, Theorem Proving in Lean 4, “Dependent Type Theory,” 公式文書。 Leanの依存関数型、宇宙階層、宇宙多相を説明する。歴史的CoCの仕様書ではない。

Lean project, “Is Lean just like Rocq?”, Frequently Asked Questions, 公式文書。LeanとRocqの宇宙累積性、 証明無関係性、再帰のkernel上の扱いなどの差を確認する現行資料。

Lean project, The Lean Language Reference, 公式文書。関数型、Prop、宇宙、帰納型、 商、elaborationを現行Lean 4の仕様として確認する。歴史的由来や一般の型理論の定義は このマニュアルだけから推論しない。

Lean project, The Lean Language Reference, “Recursive Definitions,” 公式文書。 構造再帰、整礎再帰、部分不動点、帰納的・余帰納的述語、partial の論理上の差を確認する。 圏論的な始代数・終余代数の一般理論はこの仕様だけから推論しない。

Lean community, Mathlib Documentation, CategoryTheory.Category.Basic。 mathlibの圏、射の宇宙、型クラスによる圏構造の現行APIを確認する入口。圏論の数学的定義は 先に定義と定理を数学的記法で理解し、API設計と区別して読む。