Reasoning about Java Classes in Nuprl (continued)

by Pavel Naumov
1997-1998

This Tuesday I will continue my September 9 talk on types with recursive elements. This time I will deal with only one such type - RecPair - that corresponds to Java class:

class RecPair {int z; RecPair r;}

After reminding inference rules for this type I will present its encoding into the existing Nuprl Type Theory and, therefore, will prove consistency of my new inference rules with the existing rules in Nuprl.

The same encoding can be applied to a much wider collection of types with recursive elements that I discussed on September 9.

Reasoning about Java Classes in Nuprl (continued)

by Pavel Naumov 1997-1998

by Pavel Naumov
1997-1998