Towards proving type safety of C#C#

We consider a substantial subset of C#C#, named C#C#SS. We develop a mathematical specification for C#C#SS by formalizing its abstract syntax, execution environment, well-typedness conditions, and operational evaluation semantics. Based on this specification, we prove that C#C#SS is type-safe by showing that the execution of C#C#SS programs preserves the types, up to a subtype relationship.