Help understanding academic notation for type system

Question

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:

x_ : C_, this : C |- e0 : E0         E0 <: C0
class C extends D {...}
if mtype(m,D) = D_->D0, then C_ = D_ and C0 = D0
---------------------------------------------------------------------------
C0 m(C_ x_){ return e0; } OK IN C

That is my best attempt at reproducing it in text, anyways. However, the paper, seems to assume that such notation is familiar, and barely explains it. Could anyone point me in the direction of a better explanation? Thanks!

Answer 1

Looks like formal semantics, and in this case of syntax probably denotational semantics, but some symbols look pretty much cryptic.

Answer 2

Benjamin Pierce's undergraduate textbook Types and Programming Languages will teach you everything you need to know to understand the notations used in the Featherweight Java paper. (I think Pierce may be coauthor of that paper as well.)

Answer 3

This is a particularly complicated example, and a few separate things are going on inside it.

The horizontal bar notation is usually used for inference rules. Above the line are premises (usually separated by whitespace on a single line), below the line is a conclusion. E.g.,

P0   P1   ...   Pn
------------------
        C

means "if P0 through Pn all hold, then we may conclude that C holds as well."

The turnstile notation (⊦) is usually used for entailment relations. In type systems, this usually means "if we assume the types on the left-hand side, we can derive the types on the right-hand side." The colon is conventionally used to associate a variable or expression with a type, so

x_ : C_, this : C ⊦ e0 : E0

means "assuming x_ has type C_ and this has type C, we can derive that e0 has type E0."¹

The symbol <: is conventionally used for sub-typing relations, but this should be defined explicitly in the paper.

The "class C extends D" bit seems to be referring to the syntax of the source program. I.e., the intended premise is "C is explicitly declared to extend D".

The rest of it is hard to grok without wading into the paper. I heartily second Norman Ramsey's recommendation of Pierce as a good introduction to type theory.

¹ Note that the difference between "inference" and "entailment" is either subtle or non-existent—which one to use where is a matter of convention, taste, and/or fine distinctions.