Wrapping Up and Documenting LAMBDA++

In this lesson we wrap up and nicely document LAMBDA++. In doing so, we also take the freedom to reorganize the semantics a bit, to make it look better.

See the lambda.k file, which is self-explanatory.

Part 3 of the tutorial is now complete. Part 4 will teach you more features of the K framework, in particular how to exhaustively explore the behaviors of non-deterministic or concurrent programs.

MOVIE (out of date) [6'23"]