在程式語言類型論中，定型環境（英語：typing environment）是變量名與其類型的列表，用 Γ {\displaystyle \Gamma } （Gamma）（伽瑪）來做表示。在靜態類型程式語言中，類型規則（英語：type rules）利用定型環境確定變量的類型，進行類型檢查。
如果x的類型是int，則寫作 x : i n t {\displaystyle x:int} 。如果定型環境裏有x,y,z三個變量名，類型分別為int, bool, string，則寫作 Γ = x : i n t , y : b o o l , z : s t r i n g {\displaystyle \Gamma =x:int,y:bool,z:string} 。
x : i n t , y : b o o l , z : s t r i n g ⊢ a : c h a r {\displaystyle x:int,y:bool,z:string\vdash a:char} 判斷類型為char的變量a是否在定型環境裏面，由於定型環境裏只記錄了x,y,z的類型，所以這句表達式的結果是假。
（Gamma）（伽瑪）來做表示。在靜態類型程式語言中，類型規則利用定型環境確定變量的類型，進行類型檢查。
。如果定型環境裏有x,y,z三個變量名，類型分別為int, bool, string，則寫作
。
判斷類型為char的變量a是否在定型環境裏面，由於定型環境裏只記錄了x,y,z的類型，所以這句表達式的結果是假。
