Formally describing the specification of a programming language is a challenging task. Specifications that use imperative features, such as state or exceptions, or that manipulate continuations are very difficult to describe in usual operational semantics, such as natural semantics or SOS.In addition, these descriptions are not objects that can be used to derive interpreters, mechanized semantics, or analyses. We present ways to represent programming languages semantics in Skel, a minimal, purely functional, strongly-typed setting for writing Skeletal Semantics. The purpose of this talk is to show that a very simple language may capture complex features in a readable, maintainable, and usable way. We proceed by refinement, considering more and more involved language features. We first provide an arithmetic language formalization in Skel. Then, we extend it step by step, introducing new language constructs such as exceptions, state, and delimited computations. Our approach is to define and exploit the power of monads and their combination for writing concise formal programming language specifications. We claim we write the semantics of a programming language in a way that is systematic, easy to read, and easy to maintain.
