Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages