Type Inference Verified: Algorithm W in Isabelle/HOL

被引：0
作者：
Wolfgang Naraschewski
Tobias Nipkow
机构：
[1] Technische Universität München,
[2] Institut für Informatik,undefined
[3] Technische Universität München,undefined
[4] Institut für Informatik,undefined
来源：
Journal of Automated Reasoning | 1999年 / 23卷
关键词：
type inference; machine-checked proof; Isabelle/HOL; Mini-ML;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This paper presents the first machine-checked verification of Milner's type inference algorithm W 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.
引用
收藏
页码：299 / 318
页数：19
相关论文
共 7 条
  • [1] de Bruijn N. G.(1972)Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem Indag. Math. 34 381-392
  • [2] Hindley J. R.(1969)The principal type-scheme of an object in combinatory logic Trans. AMS 146 29-60
  • [3] Milner R.(1978)A theory of type polymorphism in programming J. Comput. System Sci. 17 348-375
  • [4] Nipkow T.(1995)Type reconstruction for type classes J. Functional Programming 5 201-224
  • [5] Prehofer C.(1985)Verifying the unification algorithm in LCF Sci. of Computer Programming 5 143-169
  • [6] Paulson L. C.(1990)Type inference for polymorphic references Inform. and Comput. 89 1-34
  • [7] Tofte M.(undefined)undefined undefined undefined undefined-undefined
1