package rocq-semantics

This is a survey of programming language semantics styles for a miniature example of a programming language, with their encoding in Rocq (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 Rocq, 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 Rocq, but there are no proofs associated.

The current version is only compatible with a recent version of Rocq (tested with versions 9.0 to 9.1) but previous versions of this repository worked with older version of Rocq and Coq