PRL Seminars
Reasoning about Java Classes in Nuprl (continued)
Pavel Naumov
September 16, 1997
Abstract
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.