| 英語 | 日本語 | 備考 |
|---|---|---|
| abbreviation | 省略形 | |
| abstraction | 抽象 | |
| angle bracket | 角括弧 | square bracketと同じ訳語にしているが、直後にコード例がある場合も多いため文脈で見分けられる想定 |
| annotation | 注釈 | |
| anonymous constructor | 匿名コンストラクタ | |
| assign | 割り当て | |
| accessible | （仮定のアクセス可否の文脈で）アクセス可能 | |
| associativity | 結合性 | |
| assumption | 仮定 | |
| at most | 高々 | |
| atomic | アトミック | |
| attribute | 属性 | |
| auto-bound | 自動的に束縛された | |
| backtrack | バックトラック | 後戻りと書かれる場合あり |
| base case | 基本ケース | |
| bijection | 全単射 | |
| binder | 束縛子 | |
| binding | 束縛 | |
| boolean | 真偽値 | |
| bound variable | 束縛変数 | |
| box | ボックス化 | |
| bullet | ブレット | |
| canonical | 標準 | |
| carriage return | CR | |
| case distinction | 場合分け | |
| chapter | 章 | |
| circular argument | 循環論法 | |
| clause | 節 | |
| closed term | 閉項 | |
| combinator | コンビネータ | |
| comma | カンマ | |
| command | コマンド | |
| command elaboration | コマンドエラボレーション | |
| compilation | コンパイル | |
| completion | 補完 | |
| configuration item | 設定項目 | |
| confluence | 合流性 | |
| conjunction | 連言 | |
| consistency | 一貫性 | |
| constant | 定数 | |
| construction | 構成 | |
| constructor | コンストラクタ | |
| content | 内容 | |
| context | （プログラム中のcontextの意で）コンテキスト、（文章中のcontextの意で）文脈 | |
| conversion | 変換 | |
| core language | コア言語 | |
| core type theory | コア型理論 | |
| curly brace | 波括弧 | |
| currying | カリー化 | |
| datatype | データ型 | |
| debugging trace | デバッグトレース | |
| declaration | 宣言 | |
| definition | 定義 | |
| definitional (η-)equality | 定義上の(η)等価性 | |
| definition-like | 定義に類する | |
| definitional proof irrelevance | 定義上の証明の irrelevance | |
| dependent | 依存的 | 後ろに何も続かない場合 |
| dependent function | 依存関数 | |
| dependent type theory | 依存型理論 | |
| derivation | 導出 | |
| deriving | 導出 | |
| desugar | 脱糖 | |
| disjointness | 不連結性 | |
| disjunction | 選言 | |
| domain | 定義域 | |
| double-struck | 重ね打ち体 | |
| effect | 作用 | |
| elaborate | エラボレート | |
| elaboration | エラボレーション | |
| elaborator | エラボレータ | |
| elimination rule | 除去則 | |
| encoding | エンコード | |
| English letter | 英語アルファベット | |
| enum inductive | 列挙的帰納 | |
| environment | 環境 | |
| environment extensions | 環境拡張 | |
| equational lemma | 等式の補題 | |
| equivalence | 同値性 | |
| equivalent | 同値 | |
| evaluate | 評価 | |
| evidence | 根拠 | |
| exception | 例外 | |
| exclamation mark | 感嘆符 | |
| executable | 実行ファイル | |
| expression | 式 | |
| extend | 拡張 | |
| field | （構造体・クラスのメンバの意味）フィールド | |
| field specifier | フィールド指定子 | |
| first-class | 第一級 | |
| fixed point operator | 不動点演算子 | |
| fixed-width integer | 固定幅 整数 | |
| formalization | 形式化 | |
| form feed | 改ページ | |
| functional programming language | 関数型プログラミング言語 | |
| function extensionality | 関数外延性 | |
| function type | 関数型 | |
| goal | ゴール | |
| grammar | 文法 | |
| guillemet | ギュメ | フランス語 |
| heap region | ヒープ領域 | |
| hierarchical identifier | 階層的識別子 | |
| hierarchy | 階層 | |
| higher-order function | 高階関数 | |
| hygiene | （マクロの）健全性 | |
| hypothese | 仮定 | |
| identically | 同一 | |
| identifier | 識別子 | |
| identifier component | 識別子要素 | |
| identifier continuation character | 識別子継続文字 | |
| identity function | 恒等関数 | |
| immediate value | 即値 | |
| imperative | 命令型 | |
| implicit parameter | 暗黙のパラメータ | |
| inaccessible | （仮定のアクセス可否の文脈で）アクセス不能 | |
| incompatible | 互換性 | |
| index, indices | 添字 | |
| induction | 帰納法 | |
| induction hypothese | 帰納法の仮定 | |
| inductively-defined | 帰納的に定義された | |
| inductive predicate | 帰納的述語 | |
| inductive type | 帰納型 | |
| info tree | 情報木 | |
| inhabitant | 住人 | |
| inheritance | 継承 | |
| initialization | 初期化 | |
| injectivity | 単射性 | |
| instance implicit parameter | インスタンスの暗黙のパラメータ | |
| instances synthesize | インスタンス合成 | |
| instantiate, instantiation | インスタンス化 | |
| intensional | 内包的 | |
| interactive theorem prover | 対話型定理証明器 | |
| interface | インタフェース | |
| interleave | 交互に実行する | |
| intermediate representation | 中間表現 | |
| interpolate | 補間 | |
| invariant | 不変量 | |
| kernel | カーネル | |
| keyword | キーワード | |
| kind | 種 | |
| laziness | 遅延 | |
| language server | 言語サーバ | |
| lawful | 合法 | |
| least upper bound | 最小上界 | |
| lemma | 補題 | |
| letter | 文字 | |
| letterlike | 文字様 | |
| level expression | レベル式 | |
| longest match | 最長一致 | |
| main goal | メインゴール | |
| macro | マクロ | |
| machine integer | 機械整数 | |
| machinery | 機構 | |
| macro Expansion | マクロ展開 | |
| map | 写像 | |
| mapping | マッピング | |
| memoization | メモ化 | |
| modifier | 修飾子 | |
| monad | モナド | |
| monomorphism | モノ射 | |
| motive | 動機 | |
| multi-threading | マルチスレッド | |
| mutually inductive | 相互帰納 | |
| namespace | 名前空間 | |
| nested | ネストされた | |
| newline | 改行 | |
| non-dependent | 非依存的 | |
| normal form | 正規形 | |
| notation | 記法 | |
| opaque | 不透明 | |
| operator | 演算子 | |
| open scope | 開いたスコープ | |
| packrat parse | パックラットパース | 一般的にはパックラット構文解析と呼ばれることが多いが、parseをパースと書くことに合わせた |
| panic | パニック | |
| parameter | パラメータ | |
| parse | パース | |
| parser | パーサ | |
| pattern matching | パターンマッチ | |
| polymorphic | 多相 | |
| precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
| predicate | 述語 | |
| pretty printer | プリティプリンタ | |
| primitive | プリミティブ | |
| primitive recursion | 原始再帰 | |
| procedure | 手続き | |
| product type | 直積型 | |
| projection function | 射影関数 | |
| proof checker | 証明チェッカ | |
| proof state | 証明状態 | |
| proof term | 証明項 | |
| qualification | 修飾 | |
| quantify | 量化 | |
| quantification | 量化子 | |
| question mark | 疑問符 | |
| quote | クォート | |
| quotient type | 商型 | |
| range | 値域 | |
| raw identifier | 生識別子 | Rust By Exampleの表現を利用 |
| reasoning | 推論 | |
| recovery | 回復 | |
| recursive-descent parser | 再帰下降パーサ | |
| reduction | 簡約 | |
| reference count | 参照カウント | |
| rename | リネーム | |
| representation | 表現 | |
| reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
| reserved word | 予約語 | |
| rewrite | 書き換え | |
| run-length encoding | 連長圧縮 | |
| run-time | ランタイム | |
| rule | 規則 | |
| saturated application | 完全な適用 | 固定訳は無いように思われ、飽和では意味が分かりづらいため |
| schematic definition | スキーマ的定義 | |
| scope | スコープ | |
| scrutinee | 被検査対象 | |
| separator | 区切り文字 | |
| set | （数学的な集合の場合）集合、（数学的な集合を意味しない場合でプログラミング上実体のある集まりの場合）セット、（それ以外）あつまり | |
| section | 節 | |
| serialize | シリアライズ | |
| shadow | （変数の隠蔽の意で）シャドーイング | |
| side effect | 副作用 | |
| signature | シグネチャ | |
| simplifier | 単純化器 | |
| simplify | 単純化 | |
| simp set | simp セット | |
| single quote | シングルクォート | |
| singleton | 単集合 | |
| soundness | 健全性 | |
| square bracket | 角括弧 | |
| specialization | 特殊化 | |
| statement | 文 | |
| strict implicit parameter | 厳格な暗黙のパラメータ | |
| strictly | （順序の意味で）狭義 | |
| strictness | 正格 | |
| strong induction | 強帰納法 | |
| structure | 構造体 | |
| subfield | サブフィールド | |
| subgoal | サブゴール | |
| subterm | 部分項 | |
| subtype | 部分型 | |
| subscript | 下付き文字 | |
| substitution | 置換 | |
| syntactically | 構文上 | |
| syntactic sugar | 構文糖衣 | |
| syntax | 構文 | |
| syntax category | 構文カテゴリ | |
| syntax former | 構文形成器 | |
| syntax trees | 構文木 | |
| syntax value | 構文の値 | |
| synthetic syntax | 統合的な構文 | |
| tactic | タクティク | |
| Technical Terminology | 専門用語 | |
| tail | 後続のリスト | 「末尾」だと「最後の1要素」というようにも読めるため |
| term | 項 | |
| term elaboration | 項エラボレーション | |
| termination | 停止 | |
| theorem | 定理 | |
| token | 字句 | |
| top-level | トップレベル | |
| totality | 全域性 | |
| transitive | 推移的 | |
| transitivity | 推移性 | |
| tree | 木 | |
| trivial | 自明な | |
| trust | 信頼 | |
| tuple | タプル | |
| turnstile | ターンスタイル | |
| type class | 型クラス | |
| type class instance synthesis | 型クラスインスタンス合成 | |
| type signature | 型シグネチャ | |
| unbox | ボックス化解除 | C#の用語を流用 |
| underscore | アンダースコア | |
| unification | 単一化 | |
| union | 合併 | |
| unit type | ユニット型 | |
| universe | 宇宙 | |
| universe level | 宇宙レベル | |
| universe-polymorphic | 宇宙多相 | |
| well-formed | 適格 | |
| well-founded | 整礎 | |
| whitespace | 空白 | |
| wrapper | ラッパ |
| 用語 | 備考 |
|---|---|
| choice node | |
| cumulative | |
| impredicativity, predicativity | |
| no confusion | |
| packed array | System Verilogという言語にこの名前の文法要素がある？ |
| strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 |
| prelude | |
| relevant, irrelevant | 直訳して「関係・無関係」はわかりづらいと判断 |
| subject reduction | TAPLに出てくる模様 |
| subsingleton | |
| type ascription | Scala、Rustに同じ用語あり |
| well-typed |