Formal model for defender method resolution

Collin Fagan collin.fagan at
Thu Jan 20 06:01:35 PST 2011

Okay, I'm officially out of my depth. This looks like math and I was never
good at math. Is the English/java for this really so verbose as to require
this massively abbreviated syntax? It's a six page document, if the syntax
is ten time more expressive/terse then I can see not wanted to write 60
pages. But if it's only twice as abbreviated the would not a 12 page
document reach more people?


On Wed, Jan 19, 2011 at 11:48 AM, Brian Goetz <brian.goetz at>wrote:

> At
> I have posted a draft of a formal model for resolution of defender
> methods.  This is written in the style of "Featherweight Java"
> (Igarashi, Pierce, et al), in which a number of real-world language
> concerns are abstracted away, in order to simplify the formalism for the
> portion of the language of interest, notably the typing and resolution
> of defender methods.
> Hopefully this will serve as a basis for discussion of the proposal.
> The T- and S- rules are implemented by the compiler and are used for
> typing; the R- rules are implemented by the VM to do method selection.
> (The primary computed item of interest is mres(C), which is the method
> resolution for a given class -- while this is not used in any further
> production (it would be used if the operational semantics were
> specified), it is in fact the whole point of this exercise.)

More information about the lambda-dev mailing list