New answers tagged


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 $\...

Top 50 recent answers are included