1 <HTML><HEAD><TITLE>HOL/MiniML/ReadMe</TITLE></HEAD><BODY> |
1 <HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD> |
2 <H1>Type Inference for MiniML (without <kbd>let</kbd>)</H1> |
2 <BODY> |
3 |
3 |
4 This theory formalizes the basic type inference algorithm underlying all |
4 <H1>Type Inference for MiniML (without <kb>let<kb>)</H1> |
5 typed functional programming languages. This algorithm is called |
5 |
6 <kbd>W</kbd>, its more imperative variant is called <kbd>I</kbd>. Both were |
6 This theory defines the type inference rules and the type inference algorithm |
7 first described in |
7 <em>W</em> for simply-typed lambda terms due to Milner. It proves the |
8 <P> |
8 soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized |
9 <KBD> |
9 version <em>I</em> is shown equivalent to <em>W</em> (one direction only). |
10 @article{Milner-Poly,author="Robin Milner", |
10 |
11 title="A Theory of Type Polymorphism in Programming", |
|
12 journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"} |
|
13 </KBD> |
|
14 <P> |
|
15 which also proves their correctness. The first completeness proof was given |
|
16 in |
|
17 <P> |
|
18 <KBD> |
|
19 @phdthesis{Damas-PhD,author={Luis Manuel Martins Damas}, |
|
20 title={Type Assignment in Programming Languages}, |
|
21 school={Department of Computer Science, University of Edinburgh},year=1985} |
|
22 </KBD> |
|
23 <P> |
|
24 The Isabelle proofs are based on |
|
25 <P> |
|
26 <KBD> |
|
27 @phdthesis{Nazareth-PhD,author={Dieter Nazareth}, |
|
28 title={A Polymorphic Sort System for Axiomatic Specification Languages}, |
|
29 school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen}, |
|
30 year=1995,note={Technical Report {TUM-I9515}}} |
|
31 </KBD> |
|
32 <P> |
11 <P> |
33 |
12 |
34 <H2>M.Sc./Diplom Project</H2> |
13 A report describing the theory is found here:<br> |
35 |
14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W0.html"> |
36 Task: extend MiniML with a <kbd>let</kbd>-construct and polymorphic types. We |
15 Formal Verification of Algorithm W: The Monomorphic Case</A>. |
37 are looking for an enthusiastic student with some basic knowledge of |
|
38 functional programming who is not afraid of logic and proofs. Sounds |
|
39 interesting? Then contact <A |
|
40 HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A |
|
41 HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>. |
|
42 |
16 |
43 </BODY> |
17 </BODY> |
44 </HTML> |
18 </HTML> |