A Simple Algorithm and Proof for Type Inference. Wand, M. *Fundamenta Infomaticae*, 10:115-122, 1987. 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

{"_id":"Lzc2LtEHmeJWzTNuK","bibbaseid":"wand-asimplealgorithmandprooffortypeinference-1987","downloads":0,"creationDate":"2017-04-23T20:31:12.549Z","title":"A Simple Algorithm and Proof for Type Inference","author_short":["Wand, M."],"year":1987,"bibtype":"article","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]}],"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.","bibtex":"@Article{Wand87a,\n author = \t\"Mitchell Wand\",\n title = \t\"A Simple Algorithm and Proof for Type Inference\",\n journal = \t\"Fundamenta Infomaticae\",\n year = \t\"1987\",\n volume = \t\"10\",\n OPTnumber = \t\"\",\n pages = \t\"115-122\",\n OPTmonth = \t\"\",\n OPTnote = \t\"\",\n URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/fundamenta-87.dvi},\n abstract = \"We present a simple proof of Hindley's Theorem: that it is decidable whether\na term of the untyped lambda calculus is the image under type-erasing of a\nterm of the simply typed lambda calculus. The proof proceeds by a direct\nreduction to the unification problem for simple terms. This arrangement of\nthe proof allows for easy extensibility to other type inference problems.\"\n}\n\n","author_short":["Wand, M."],"key":"Wand87a","id":"Wand87a","bibbaseid":"wand-asimplealgorithmandprooffortypeinference-1987","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/fundamenta-87.dvi"},"downloads":0,"html":""},"search_terms":["simple","algorithm","proof","type","inference","wand"],"keywords":[],"authorIDs":[],"dataSources":["zM8mNPR4ZkAHKtvDs"]}