src/HOL/W0/README.html
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 15582 7219facb3fd0
permissions -rw-r--r--
avoid rebinding of existing facts;
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
webertj@15582
     3
<!-- $Id$ -->
webertj@15582
     4
webertj@15582
     5
<HTML>
webertj@15582
     6
webertj@15582
     7
<HEAD>
webertj@15582
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     9
  <TITLE>HOL/W0/README</TITLE>
webertj@15582
    10
</HEAD>
webertj@15582
    11
nipkow@2518
    12
<BODY>
nipkow@2518
    13
nipkow@2518
    14
<H1>Type Inference for MiniML (without <tt>let</tt>)</H1>
nipkow@2518
    15
nipkow@2518
    16
This theory defines the type inference rules and the type inference algorithm
nipkow@2518
    17
<em>W</em> for simply-typed lambda terms due to Milner. It proves the
nipkow@2518
    18
soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized
nipkow@2518
    19
version <em>I</em> is shown to implement <em>W</em>.
nipkow@2518
    20
nipkow@2518
    21
<P>
nipkow@2518
    22
nipkow@2518
    23
A report describing the theory is found here:<br>
nipkow@2518
    24
<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
nipkow@2518
    25
Formal Verification of Algorithm W: The Monomorphic Case</A>.
nipkow@2518
    26
nipkow@2518
    27
<P>
nipkow@2518
    28
nipkow@2518
    29
<B>NOTE:</B> This theory has been superseded by a more recent development
nipkow@2518
    30
which formalizes type inference for a language including <tt>let</tt>. For
nipkow@2518
    31
details click <A HREF="../MiniML/index.html">here</A>.
nipkow@2518
    32
</BODY>
nipkow@2518
    33
</HTML>