Completing and Documenting IMP

We here learn no new concepts, but it is a good moment to take a break and contemplate what we learned so far.

Let us add lots of formal annotations to imp.k.

Once we are done with the annotations, we kompile with the documentation option and then take a look at the produced document. We often call these documents language posters. Depending on how much information you add to these language posters, they can serve as standalone, formal presentations of your languages. For example, you can print them as large posters and post them on the wall, or in poster sessions at conferences.

This completes our second tutorial. The next tutorials will teach us more features of the K framework, such as how to define languages with complex control constructs (like callcc), languages which are concurrent, and so on.

MOVIE (out of date) [03'45"]