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