New answers tagged


To add to varkor's answer: A context is just a function sending (some) variables to their types. So the rule is saying: "If $\Gamma$ assigns the type $\tau$ to variable $x$, then we can deduce $\Gamma \vdash x : \tau$."


$\Gamma$ here is overloaded notation. The meaning of the expression $\Gamma(x) = \tau$ above the inference line here is given under the "Type rules." section of A Short Introduction to Systems F and F Omega on page 5. In this setting, $\Gamma$ is an inductively-defined function sending variables (in $\Gamma$ considered as a context, i.e. a list of variables) ...

Top 50 recent answers are included