This is a case study formalizing a toy compiler and proving its correctness. There are two versions given below. The first version is presented in the paper Double WP: vers une preuve automatique d'un compilateur and is compatible with Why3 0.88. The second version is adapted to the future major release of Why3 (currently available as the 'new_system' branch of the git repository). This second version makes use of type invariants.
Topics: Semantics of languages
see also the index (by topic, by tool, by reference, by year)
The version compatible with Why3 0.88 is described there.
The version compatible with the new Why3 system is described there.