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