src/HOL/MiniML/README.html
changeset 1753 88e0d3160909
parent 1752 7dfc3c217414
child 2523 0ccea141409b
equal deleted inserted replaced
1752:7dfc3c217414 1753:88e0d3160909
     4 <H1>Type Inference for MiniML (without <kb>let<kb>)</H1>
     4 <H1>Type Inference for MiniML (without <kb>let<kb>)</H1>
     5 
     5 
     6 This theory defines the type inference rules and the type inference algorithm
     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
     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
     8 soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized
     9 version <em>I</em> is shown equivalent to <em>W</em> (one direction only).
     9 version <em>I</em> is shown to implement <em>W</em>.
    10 
    10 
    11 <P>
    11 <P>
    12 
    12 
    13 A report describing the theory is found here:<br>
    13 A report describing the theory is found here:<br>
    14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
    14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">