Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 299-318 |
| Number of pages | 20 |
| Journal | Journal of Automated Reasoning |
| Volume | 23 |
| Issue number | 3 |
| DOIs | |
| State | Published - Nov 1999 |
Keywords
- Isabelle/HOL
- Machine-checked proof
- Mini-ML
- Type inference
Fingerprint
Dive into the research topics of 'Type Inference Verified: Algorithm script W sign in Isabelle/HOL'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver