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.