3

This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over. Apparently you are in the parts that define variable bindings. $\mathcal{B}[\mathcal{X}]_s$ appears to be the set of terms, or binding structures at sort $s$ whose free variables are among $\...


Only top voted, non community-wiki answers of a minimum length are eligible