Semantics of programming languages are generally laid out in one of three popular styles: operational, denotational and axiomatic. Most popular texts cover only one of these topics, and the treatment is completely theoretical. We believe that it is important to provide exposure to multiple styles, comparing and contrasting them, so that the students can judiciously choose a style guided by the task at hand. Secondly, a completely theoretical treatment of this topic restricts the understanding and appreciation for this formalism as the students are not able to experiment. Some recent courses attempt to remedy the situation by allowing the students to build these semantics in popular languages like OCaml or Haskel; though an encouraging direction, regular programming languages are restrictive as they do not allow the students to prove properties about the language description—which is the primary purpose of formalizing the semantics of a language.

In this paper, we propose that proof assistants are an interesting tool for teaching and learning programming language semantics. We support our proposal by providing a complete encoding of the semantics of the W HILE language in operational, denotational, and axiomatic semantics in the F* proof assistant.

We show that once the program and its semantics are encoded, modern proof assistants are quite capable of proving interesting properties about the language features with minimal human assistance. In summary, we believe that proof assistants not only provide a more concrete understanding of the topic but also prepares programming language researchers to use theorem provers as basic tools in their research and not as an afterthought.