An unboxed operational semantics for an ML-style polymorphic language is presented. Different from the conventional formalisms, the proposed semantics accounts for actual representations of run-time objects of various types, and supports a refined notion of polymorphism that allows polymorphic functions to be applied directly to values of various different representations. The ML type system is shown to be sound with respect to the operational semantics realized by the translation.
ASJC Scopus subject areas
- Computer Science(all)