Γ is typically used to denote the context, or the type environment for an expression. It is a mapping from variables to types. for example we could have

Γ = x:A, y:B, z:C

then

Γ |- y: B

is a typing judgment. Means "In the context of Γ, y has type B."

Type derivation is a process where you start with an expression and an empty context and then figure out what the type of that expression is by building it up from scratch using typing rules. It's what compilers do to figure out whether your program is correct.

https://feddit.it/comment/20528152