Γ 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.
god dammit this is actually good 😭. i literally did semantics of programming languages last term too
Would you be up for explaining it please?
Γ 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