Typing environment とは

型理論では、型付け環境(または型付きコンテキスト)は、変数名とデータ型の間の関連を表します。
より正式には、環境 Γ {\displaystyle \Gamma } はペア x , τ {\displaystyle \langle x,\tau \rangle } の集合または順序リストであり、 x : τ {\displaystyle x:\tau } と書かれ、 x {\displaystyle x} は変数、 τ {\displaystyle \tau } はそのタイプです。
判断
Γe:τ
「eは文脈Γにおいてタイプτを有する」と読み取られる。
静的型プログラミング言語では、これらの環境は型ルールによって使用され、維持され、与えられたプログラムや式を型チェックします。