@inproceedings{c572d7d7fd2142009cc89f093f0f7bd8,
title = "Formal verification of algorithm W: The monomorphic case",
abstract = "A formal verification of the soundness and completeness of Milner's type inference algorithm W for simply typed lambda-terms is presented. Particular attention is paid to the notorious issue of “new” variables. The proofs are carried out in Isabelle/HOL, the HOL instantiation of the generic theorem prover Isabelle.",
author = "Dieter Nazareth and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1996 ; Conference date: 26-08-1996 Through 30-08-1996",
year = "1996",
doi = "10.1007/bfb0105414",
language = "English",
isbn = "9783540615873",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "332--345",
editor = "\{von Wright\}, Joakim and Jim Grundy and John Harrison",
booktitle = "Theorem Proving in Higher Order Logics - 9th International Conference, TPHOLs 1996, Proceedings",
}