src/HOL/MiniML/README.html
changeset 2523 0ccea141409b
parent 1753 88e0d3160909
child 2531 7cfa1a9c744d
equal deleted inserted replaced
2522:a1a18530c4ac 2523:0ccea141409b
     1 <HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
     1 <HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
     2 <BODY>
     2 <BODY>
     3 
     3 
     4 <H1>Type Inference for MiniML (without <kb>let<kb>)</H1>
     4 <H1>Type Inference for MiniML</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.
     9 version <em>I</em> is shown to implement <em>W</em>.
       
    10 
     9 
    11 <P>
    10 <P>
    12 
    11 
    13 A report describing the theory is found here:<br>
    12 A report describing the theory is found here:<br>
    14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
    13 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">
    15 Formal Verification of Algorithm W: The Monomorphic Case</A>.
    14 Type Inference Verified: Algorithm <i>W</i> in Isabelle/HOL</A>.
    16 
    15 
    17 </BODY>
    16 </BODY>
    18 </HTML>
    17 </HTML>