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

Tristan Crolard, Emmanuel Polonowski

We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…