帮助理解类型系统的学术符号

I'm trying to understand an academic paper (pdf) about programming language design. In particular, it describes a lightweight version of Java called Featherweight Java. It has typing rules with notation like this: (pdf