A Simple Algorithm and Proof for Type Inference. Wand, M. Fundamenta Infomaticae, 10:115-122, 1987.
A Simple Algorithm and Proof for Type Inference [link]Paper  abstract   bibtex   
We present a simple proof of Hindley's Theorem: that it is decidable whether a term of the untyped lambda calculus is the image under type-erasing of a term of the simply typed lambda calculus. The proof proceeds by a direct reduction to the unification problem for simple terms. This arrangement of the proof allows for easy extensibility to other type inference problems.
@Article{Wand87a,
  author = 	"Mitchell Wand",
  title = 	"A Simple Algorithm and Proof for Type Inference",
  journal = 	"Fundamenta Infomaticae",
  year = 	"1987",
  volume = 	"10",
  OPTnumber = 	"",
  pages = 	"115-122",
  OPTmonth = 	"",
  OPTnote = 	"",
  URL =  {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/fundamenta-87.dvi},
  abstract =    "We present a simple proof of Hindley's Theorem:  that it is decidable whether
a term of the untyped lambda calculus is the image under type-erasing of a
term of the simply typed lambda calculus.   The proof proceeds by a direct
reduction to the unification problem for simple terms.  This arrangement of
the proof allows for easy extensibility to other type inference problems."
}

Downloads: 0