Added links to documentation
Thu, 22 Feb 1996 18:35:16 +0100
changeset 1519 f999804f11ea
parent 1518 03b770044429
child 1520 5fee0fef5019
Added links to documentation
--- a/src/HOL/MiniML/README.html	Thu Feb 22 18:25:19 1996 +0100
+++ b/src/HOL/MiniML/README.html	Thu Feb 22 18:35:16 1996 +0100
@@ -1,44 +1,18 @@
-<H1>Type Inference for MiniML (without <kbd>let</kbd>)</H1>
+<H1>Type Inference for MiniML (without <kb>let<kb>)</H1>
-This theory formalizes the basic type inference algorithm underlying all
-typed functional programming languages. This algorithm is called
-<kbd>W</kbd>, its more imperative variant is called <kbd>I</kbd>. Both were
-first described in
-@article{Milner-Poly,author="Robin Milner",
-title="A Theory of Type Polymorphism in Programming",
-journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
-which also proves their correctness.  The first completeness proof was given
-@phdthesis{Damas-PhD,author={Luis Manuel Martins Damas},
-title={Type Assignment in Programming Languages},
-school={Department of Computer Science, University of Edinburgh},year=1985}
-The Isabelle proofs are based on
-@phdthesis{Nazareth-PhD,author={Dieter Nazareth},
-title={A Polymorphic Sort System for Axiomatic Specification Languages},
-school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
-year=1995,note={Technical Report {TUM-I9515}}}
+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 equivalent to <em>W</em> (one direction only).
-<H2>M.Sc./Diplom Project</H2>
-Task: extend MiniML with a <kbd>let</kbd>-construct and polymorphic types. We
-are looking for an enthusiastic student with some basic knowledge of
-functional programming who is not afraid of logic and proofs.  Sounds
-interesting? Then contact <A
-HREF="">Tobias Nipkow</A> or <A
-HREF="">Cornelia Pusch</A>.
+A report describing the theory is found here:<br>
+<A HREF = "">
+Formal Verification of Algorithm W: The Monomorphic Case</A>.