Part 5: Defining Type Systems

In this part of the tutorial we will show that defining type systems for languages is essentially no different from defining semantics. The major difference is that programs and fragments of programs now rewrite to their types, instead of to concrete values. In terms of K, we will learn how to use it for a certain particular but important kind of applications.