在编程语言类型论中，定型环境（英语：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的类型，所以这句表达式的结果是假。
