A high-level modular definition of the semantics of C♯

We propose a structured mathematical definition of the semantics of C♯ programs to provide a platform-independent interpreter view of the language for the C♯ programmer, which can also be used for a precise analysis of the ECMA standard of the language and as a reference model for teaching. The definition takes care to reflect directly and faithfully-as much as possible without becoming inconsistent or incomplete-the descriptions in the C♯ standard to become comparable with the corresponding models for Java in Stärk et al. (Java and Java Virtual Machine-Definition, Verification, Validation, Springer, Berlin, 2001) and to provide for implementors the possibility to check their basic design decisions against an accurate high-level model. The model sheds light on some of the dark corners of C♯ and on some critical differences between the ECMA standard and the implementations of the language.