In this lecture we study types and relations in types in programming languages, and discuss the motivation for having types.
Next we look at the way type systems are formalized. In particular, we look at the inference rules in the ChocoPy reference manual.
Finally, we start our study of the Statix meta-language for the specification of type systems. Ending with a demonstration of the Chicago project (available on github), as an example of the use of Statix.
There are no papers that give concrete examples of Statix code, but the PEPM 2016 paper gives a good introduction to the use of constraints and scope graphs, albeit in a somewhat more limited language than Statix.
This is a recording of a tutorial on Statix at the PLDI conference.