Type Inference Verified: Algorithm W in Isabelle/HOL

Wolfgang Naraschewski and Tobias Nipkow

This paper presents the first machine-checked verification of Milner's type inference algorithm W for computing the most general type of an untyped lambda-term enriched with let-expressions. This term language is the core of most typed functional programming languages and is also known as Mini-ML. We show how to model all the concepts involved, in particular types and type schemes, substitutions, and the thorny issue of ``new'' variables. Only a few key proofs are discussed in detail. The theories and proofs are developed in Isabelle/HOL, the HOL instantiation of the generic theorem prover Isabelle.

Short version: ps

BibTeX: 

@inproceedings{Naraschewski-Nipkow-TYPES96,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
booktitle={Types for Proofs and Programs: Intl. Workshop TYPES '96},
editor={E. Gim\'enez and C. Paulin-Mohring},
publisher=Springer,series=LNCS,volume=1512,pages={317--332},year=1998}

Long version: dvi

BibTeX: 

@article{NaraschewskiN-JAR,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
journal={Journal of Automated Reasoning},
year=1999,volume=23,pages={299--318}}
The corresponding Isabelle theories.

This work is based on the earlier work of Nazareth and Nipkow which did not include let.