what are meta variables in this static analysis book's explanation about types?
A metavariable is a variable that denotes some hypothetical chunk of a program. This distinction is important in the theory of programming languages, where we need to distinguish variables representing program fragments from the variables contained in those programs.
The terminology, I think, comes from logic: if you're defining a logic, you need to define it in some language that's distinct from the thing you're defining. This is the &quot;meta-language&quot;, and the variables it uses are metavariables. The history of formal logic and programming languages are deeply intertwined via the Curry-Howard correspondence, so the terminology carried over.