src/HOL/W0/README.html
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 2518 bee082efaa46
child 15283 f21466450330
permissions -rw-r--r--
import -> imports
     1 <HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
     2 <BODY>
     3 
     4 <H1>Type Inference for MiniML (without <tt>let</tt>)</H1>
     5 
     6 This theory defines the type inference rules and the type inference algorithm
     7 <em>W</em> for simply-typed lambda terms due to Milner. It proves the
     8 soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized
     9 version <em>I</em> is shown to implement <em>W</em>.
    10 
    11 <P>
    12 
    13 A report describing the theory is found here:<br>
    14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
    15 Formal Verification of Algorithm W: The Monomorphic Case</A>.
    16 
    17 <P>
    18 
    19 <B>NOTE:</B> This theory has been superseded by a more recent development
    20 which formalizes type inference for a language including <tt>let</tt>. For
    21 details click <A HREF="../MiniML/index.html">here</A>.
    22 </BODY>
    23 </HTML>