# Type Inference for MiniML (without `let`)

This theory formalizes the basic type inference algorithm underlying all
typed functional programming languages. This algorithm is called
`W`, its more imperative variant is called `I`. Both were
first described in
`
@article{Milner-Poly,author="Robin Milner",
title="A Theory of Type Polymorphism in Programming",
journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
`

which also proves their correctness. The first completeness proof was given
in

`
@phdthesis{Damas-PhD,author={Luis Manuel Martins Damas},
title={Type Assignment in Programming Languages},
school={Department of Computer Science, University of Edinburgh},year=1985}
`

The Isabelle proofs are based on

`
@phdthesis{Nazareth-PhD,author={Dieter Nazareth},
title={A Polymorphic Sort System for Axiomatic Specification Languages},
school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
year=1995,note={Technical Report {TUM-I9515}}}
`

## M.Sc./Diplom Project

Task: extend MiniML with a `let`-construct and polymorphic types. We
are looking for an enthusiastic student with some basic knowledge of
functional programming who is not afraid of logic and proofs. Sounds
interesting? Then contact Tobias Nipkow or Cornelia Pusch.