Take the 2-minute tour ×

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!

share|improve this question
You could grab a image snip of the text instead of trying to mimic the notation and use an <img> tag. –  Augusto Radtke Feb 12 '09 at 1:59
add comment

3 Answers

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

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.

share|improve this answer
add comment

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.)

share|improve this answer
add comment

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

share|improve this answer
Actually this looks like a natural-deduction semantics not a denotational semantics. From the ASCII art alone I can't tell much more. –  Norman Ramsey Feb 12 '09 at 3:32
It's a type rule. –  Dave Clarke Feb 19 '11 at 11:03
add comment

Your Answer

