src/HOL/MiniML/README.html
author nipkow
Sat, 18 Nov 1995 15:35:24 +0100
changeset 1345 d4e26f632bca
parent 1337 ad834f39d878
child 1519 f999804f11ea
permissions -rw-r--r--
Better!
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1337
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
     1
<HTML><HEAD><TITLE>HOL/MiniML/ReadMe</TITLE></HEAD><BODY>
1345
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
     2
<H1>Type Inference for MiniML (without <kbd>let</kbd>)</H1>
1337
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
     3
1345
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
     4
This theory formalizes the basic type inference algorithm underlying all
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
     5
typed functional programming languages. This algorithm is called
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
     6
<kbd>W</kbd>, its more imperative variant is called <kbd>I</kbd>. Both were
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
     7
first described in
1337
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
     8
<P>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
     9
<KBD>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    10
@article{Milner-Poly,author="Robin Milner",
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    11
title="A Theory of Type Polymorphism in Programming",
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    12
journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    13
</KBD>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    14
<P>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    15
which also proves their correctness.  The first completeness proof was given
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    16
in
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    17
<P>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    18
<KBD>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    19
@phdthesis{Damas-PhD,author={Luis Manuel Martins Damas},
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    20
title={Type Assignment in Programming Languages},
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    21
school={Department of Computer Science, University of Edinburgh},year=1985}
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    22
</KBD>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    23
<P>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    24
The Isabelle proofs are based on
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    25
<P>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    26
<KBD>
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    27
@phdthesis{Nazareth-PhD,author={Dieter Nazareth},
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    28
title={A Polymorphic Sort System for Axiomatic Specification Languages},
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    29
school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    30
year=1995,note={Technical Report {TUM-I9515}}}
ad834f39d878 README -> README.html
nipkow
parents:
diff changeset
    31
</KBD>
1345
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    32
<P>
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    33
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    34
<H2>M.Sc./Diplom Project</H2>
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    35
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    36
Task: extend MiniML with a <kbd>let</kbd>-construct and polymorphic types. We
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    37
are looking for an enthusiastic student with some basic knowledge of
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    38
functional programming who is not afraid of logic and proofs.  Sounds
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    39
interesting? Then contact <A
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    40
HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    41
HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    42
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    43
</BODY>
d4e26f632bca Better!
nipkow
parents: 1337
diff changeset
    44
</HTML>