The verification algorithm compresses types that are logically equivalent, since they cannot lead to memory safety violations. The types used by the verification algorithm are specified in §III.1.8.1.2.1, the type compatibility rules are specified in §III.1.8.1.2.2, and the rules for merging stack states are in §III.1.8.1.3.