# Variable rule in dependent type theory

This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely.

$$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau} {\phi; \Gamma \vdash x : \tau} \textsf{(ty-var)}$$

The first thing in antecedent looks like it's stating that $\Gamma$ is well-formed under the context $\phi$, is that right? What does the second thing in antecedent mean? I have a feeling of this but I am unable to get this simple rule.

• What's $\phi$ here? – Gilles 'SO- stop being evil' Mar 31 '16 at 10:28
• Actually that was from ML0,pi (C) so that's called "sort type" or type of the constraint domain where type index objects are drawn. – Pushpa Mar 31 '16 at 18:01
• i'm new to type theory and have verification(Model checking) background. So it's really new thing to me. I'm reading paper "Dependent Types in practical programming". – Pushpa Mar 31 '16 at 18:18
• Please ask your follow-up question as a separate question. It's a completely different issue. (An interesting one, too, so I do encourage you to ask it, but please ask one question at a time.) – Gilles 'SO- stop being evil' Mar 31 '16 at 18:43

Essentially, $\Gamma$ is a store that maps variables to types.
• @Pushpa, jmite: Dependent types are in the second volume ATTAPL (both good books by the way). While the basic principle is common to most type systems, dependent types does make the formuation more complex (an introduction to type theory would just have $\dfrac{\Gamma(x)=\tau}{\Gamma \vdash x:\tau}$ because that's all you need with simple types). – Gilles 'SO- stop being evil' Mar 31 '16 at 10:25