equal
deleted
inserted
replaced
|
1 Type inference for MiniML (without "let" for the time being). |
|
2 |
|
3 Algorithms W and I are based on |
|
4 |
|
5 @article{Milner-Poly,author="Robin Milner", |
|
6 title="A Theory of Type Polymorphism in Programming", |
|
7 journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"} |
|
8 |
|
9 which also proves their correctness. The first completeness proof was given |
|
10 in |
|
11 |
|
12 @phdthesis{Damas-PhD,author={Luis Manuel Martins Damas}, |
|
13 title={Type Assignment in Programming Languages}, |
|
14 school={Department of Computer Science, University of Edinburgh},year=1985} |
|
15 |
|
16 The Isabelle proofs are based on |
|
17 |
|
18 @phdthesis{Nazareth-PhD,author={Dieter Nazareth}, |
|
19 title={A Polymorphic Sort System for Axiomatic Specification Languages}, |
|
20 school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen}, |
|
21 year=1995,note={Technical Report {TUM-I9515}}} |