TY - JOUR
T1 - Type Inference Verified
T2 - Algorithm script W sign in Isabelle/HOL
AU - Naraschewski, Wolfgang
AU - Nipkow, Tobias
PY - 1999/11
Y1 - 1999/11
N2 - This paper presents the first machine-checked verification of Milner's type inference algorithm script D sign for computing the most general type of an untyped λ-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.
AB - This paper presents the first machine-checked verification of Milner's type inference algorithm script D sign for computing the most general type of an untyped λ-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.
KW - Isabelle/HOL
KW - Machine-checked proof
KW - Mini-ML
KW - Type inference
UR - http://www.scopus.com/inward/record.url?scp=0033345017&partnerID=8YFLogxK
U2 - 10.1023/A:1006277616879
DO - 10.1023/A:1006277616879
M3 - Article
AN - SCOPUS:0033345017
SN - 0168-7433
VL - 23
SP - 299
EP - 318
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 3
ER -