Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/W0/README.html
author nipkow
Fri, 17 Jan 1997 13:21:54 +0100 (1997-01-17)
changeset 2518 bee082efaa46
child 15283 f21466450330
permissions -rw-r--r--
This is the old version og MiniML for the monomorphic case. The new version is now in MiniML.
<HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
<BODY>

<H1>Type Inference for MiniML (without <tt>let</tt>)</H1>

This theory defines the type inference rules and the type inference algorithm
<em>W</em> for simply-typed lambda terms due to Milner. It proves the
soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized
version <em>I</em> is shown to implement <em>W</em>.

<P>

A report describing the theory is found here:<br>
<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
Formal Verification of Algorithm W: The Monomorphic Case</A>.

<P>

<B>NOTE:</B> This theory has been superseded by a more recent development
which formalizes type inference for a language including <tt>let</tt>. For
details click <A HREF="../MiniML/index.html">here</A>.
</BODY>
</HTML>
isabelle