This repo contains a mechanization of IMP. The mechanization is partly based on the formal definition given in the book Semantics with Applications-A Formal Introduction by H. Nielson and F. Nielson.
The language we call IMP here is named While in the book.