A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to. abstract interpretation. This is a survey of programming language semantics styles for a miniature example of a programming language, with their encoding in Coq, the proofs of equivalence of different styles, and the proof of soundess of tools obtained from axiomatic semantics or abstract interpretation. The tools can be run inside Coq, thus making them available for proof by reflection, and the code can also be extracted and connected to a yacc-based parser, thanks to the use of a functor parameterized by a module type of strings. A hand-written parser is also provided in Coq, but there are no proofs associated.
opam install coq-semantics.8.5.0