<![CDATA[
<BODY BACKGROUND="" TEXT="#000000" LINK="#0000FF" VLINK="#551A8B" ALINK="#FF0000" BGCOLOR="#C0C0C0">
NOTE: This is a frame enhanced page. Best viewed in a web browser that supports frames (e.g. Netscape).
<HR>
<H1><CENTER>Presenting Java Semantics in Nuprl</CENTER></H1>
<HR>
<H2>Table of Contents</H2>
<H4>Select slide or start at <A HREF="fslide1.htm">beginning</A>.</H4>
<UL>
<LI><A HREF="fslide1.htm">Presenting Formal Semantics for a</A>
<BR><LI><A HREF="fslide2.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide3.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide4.htm">J Fragment of Java</A>
<BR><LI><A HREF="fslide5.htm">J Fragment of Java</A>
<BR><LI><A HREF="fslide6.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide7.htm">J Semantics</A>
<BR><LI><A HREF="fslide8.htm">State of a J Virtual Machine</A>
<BR><LI><A HREF="fslide9.htm">class RecPair {int z; RecPair r}</A>
<BR><LI><A HREF="fslide10.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide11.htm">Reference Object Theory</A>
<BR><LI><A HREF="fslide12.htm">Reference Object Theory</A>
<BR><LI><A HREF="fslide13.htm">Reference Object Theory</A>
<BR><LI><A HREF="fslide14.htm">Reference Object Theory</A>
<BR><LI><A HREF="fslide15.htm">Reference Object Theory</A>
<BR><LI><A HREF="fslide16.htm">Type Theory + Object Theory = ?</A>
<BR><LI><A HREF="fslide17.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide18.htm">Verification Results</A>
<BR><LI><A HREF="fslide19.htm">Formal Verification</A>
<BR><LI><A HREF="fslide20.htm">Presenting Java in Nuprl</A>
<BR><LI><A HREF="fslide21.htm">De-formalization</A>
<BR><LI><A HREF="fslide22.htm">Formal Proof Structure</A>
<BR><LI><A HREF="fslide23.htm">Results</A>
</UL>
<P>
<H6><HR>
<CENTER>Send questions or comments to <A HREF="mailto:pavel@cs.cornell.edu">pavel@cs.cornell.edu</A></CENTER>
<CENTER><I>Last update: 3/8/98</I></CENTER>
</H6>
<CENTER><A HREF=http://www.wordperfect.com/><IMG SRC="prbox.gif" BORDER=0 width="34" height="44"></A></CENTER>
</BODY>
]]>