diff -r 03b770044429 -r f999804f11ea src/HOL/MiniML/README.html --- a/src/HOL/MiniML/README.html Thu Feb 22 18:25:19 1996 +0100 +++ b/src/HOL/MiniML/README.html Thu Feb 22 18:35:16 1996 +0100 @@ -1,44 +1,18 @@ -HOL/MiniML/ReadMe -

Type Inference for MiniML (without `let`)

+HOL/MiniML/README + + +

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}}} - +This theory defines the type inference rules and the type inference algorithm +W for simply-typed lambda terms due to Milner. It proves the +soundness and completeness of W w.r.t. to the rules. An optimized +version I is shown equivalent to W (one direction only). +

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. +A report describing the theory is found here:
+ +Formal Verification of Algorithm W: The Monomorphic Case.