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