<![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>References in Type Theory</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">References in Type Theory</A>
<BR><LI><A HREF="fslide2.htm">References in Type Theory</A>
<BR><LI><A HREF="fslide3.htm">Java class RecPair</A>
<BR><LI><A HREF="fslide4.htm">Element Constructor</A>
<BR><LI><A HREF="fslide5.htm">Element Constructor</A>
<BR><LI><A HREF="fslide6.htm">Element Destructors</A>
<BR><LI><A HREF="fslide7.htm">Operation updatez(x,z)</A>
<BR><LI><A HREF="fslide8.htm">Operation updatez(x,z)</A>
<BR><LI><A HREF="fslide9.htm">Operation updatez(x,z)</A>
<BR><LI><A HREF="fslide10.htm">Operation updatez(x,z)</A>
<BR><LI><A HREF="fslide11.htm">updatez(x,z,y) := updatez(x,z) y </A>
<BR><LI><A HREF="fslide12.htm">updatez(x,z,y) := updatez(x,z) y </A>
<BR><LI><A HREF="fslide13.htm">Operation updater(x,r)</A>
<BR><LI><A HREF="fslide14.htm">updater(x,r,y) := updater(x,r) y </A>
<BR><LI><A HREF="fslide15.htm">updater(x,r,y) := updater(x,r) y </A>
<BR><LI><A HREF="fslide16.htm">The Model</A>
<BR><LI><A HREF="fslide17.htm">eq(u,v)</A>
<BR><LI><A HREF="fslide18.htm">Lemma</A>
<BR><LI><A HREF="fslide19.htm">prz(u) and prr(u)</A>
<BR><LI><A HREF="fslide20.htm">Main Theorem</A>
<BR><LI><A HREF="fslide21.htm">Consistency</A>
</UL>
<P>
<H6><HR>
<CENTER>(c) Pavel Naumov</CENTER>
<CENTER>Send questions or comments to <A HREF="mailto:pavel@cs.cornell.edu">pavel@cs.cornell.edu</A></CENTER>
<CENTER><I>Last update: 11/23/97</I></CENTER>
</H6>
<CENTER><A HREF=http://www.wordperfect.com/><IMG SRC="prbox.gif" BORDER=0 width="34" height="44"></A></CENTER>
</BODY>
]]>