A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables

Abstract We formally specified the type system and operational semantics of Loop , comes from the treatment of parameter passing. Indeed, since Ott does not currently fully support!-conversion, we rephrased the operational semantics with explicit aliasing in order to implement theoutparameter passing mode.