changeset 1345 d4e26f632bca
parent 1337 ad834f39d878
child 1519 f999804f11ea
--- a/src/HOL/MiniML/README.html	Sat Nov 18 14:55:44 1995 +0100
+++ b/src/HOL/MiniML/README.html	Sat Nov 18 15:35:24 1995 +0100
@@ -1,8 +1,10 @@
-<H2>Type Inference for MiniML</H2>
-<H3>(without "let" for the time being)</H3>
+<H1>Type Inference for MiniML (without <kbd>let</kbd>)</H1>
-Algorithms W and I are based on
+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",
@@ -27,4 +29,16 @@
 school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
 year=1995,note={Technical Report {TUM-I9515}}}
+<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>.