src/HOL/MiniML/README.html
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 2531 7cfa1a9c744d
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 <HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
     2 <BODY>
     3 
     4 <H1>Type Inference for MiniML</H1>
     5 
     6 This theory defines the type inference rules and the type inference algorithm
     7 <em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
     8 Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
     9 rules.
    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/W.html">
    15 Type Inference Verified: Algorithm <i>W</i> in Isabelle/HOL</A>.
    16 
    17 </BODY>
    18 </HTML>