Page 19 says "we write s1 ⋈ s2 for concatenation of two stacks s1 and s2." But notably, the next use of ⋈ is actually for concatenating instructions/programs.
There is a usage of ⋈ with stacks in Lemma 4.3 for the expression "⟦e⟧⋈s", but since (1) it's only pushing a single value onto the stack, and (2) it's the only apparent usage of ⋈ on stacks, it seems like it would be simpler to just stick to the already introduced ⊳ operator here, and instead introduce ⋈ as operating on programs.
Page 19 says "we write s1 ⋈ s2 for concatenation of two stacks s1 and s2." But notably, the next use of ⋈ is actually for concatenating instructions/programs.
There is a usage of ⋈ with stacks in Lemma 4.3 for the expression "⟦e⟧⋈s", but since (1) it's only pushing a single value onto the stack, and (2) it's the only apparent usage of ⋈ on stacks, it seems like it would be simpler to just stick to the already introduced ⊳ operator here, and instead introduce ⋈ as operating on programs.