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);
nipkow@1519
     1
<HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
nipkow@1519
     2
<BODY>
nipkow@1519
     3
nipkow@2523
     4
<H1>Type Inference for MiniML</H1>
nipkow@1337
     5
nipkow@1519
     6
This theory defines the type inference rules and the type inference algorithm
nipkow@2531
     7
<em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
nipkow@2531
     8
Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
nipkow@2531
     9
rules.
nipkow@1519
    10
nipkow@1345
    11
<P>
nipkow@1345
    12
nipkow@1519
    13
A report describing the theory is found here:<br>
nipkow@2523
    14
<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">
nipkow@2523
    15
Type Inference Verified: Algorithm <i>W</i> in Isabelle/HOL</A>.
nipkow@1345
    16
nipkow@1345
    17
</BODY>
nipkow@1345
    18
</HTML>