K Tutorial

This tutorial will provide participants with a basic knowledge of the K framework, as well as hands-on experience with using K to define a real programming language. Time will be spent showing how one can write a formal (but quite intuitive) definition of a language, and use that to automatically generate an interpreter, debugger, state space search, and a model checker. After attending the tutorial, participants will be able to use K to define their own languages or calculi and then derive similar tools from their semantics for free.