Abstract

A rigorous language definition is often a necessary requirement for a language to be accepted by the community it was designed for. Whether you are an implementer, programmer, teacher or researcher, knowing the formal definition of a language can have a profound impact on how you use it. But what exactly does such a formal specification look like? This talk aims to explore the static semantics of the Standard ML core language as a case study of successful language design. We present an overview of the structure of the official Definition of Standard ML and focus on two particular issues addressed in it: polymorphism and user-defined types. Finally, we make the case that, although necessary, a formal specification alone is seldom sufficient to achieve acceptance by the community.