A type soundness proof for variables in LCF ML Article

Volpano, D, Smith, G. (1995). A type soundness proof for variables in LCF ML . Information Processing Letters, 56(3), 141-146. 10.1016/0020-0190(95)00146-4

cited authors

  • Volpano, D; Smith, G

abstract

  • We prove the soundness of a polymorphic type system for a language with variables, assignments, and first-class functions. As a corollary, this proves the soundness of the Edinburgh LCF ML rules for typing variables and assignments, thereby settling a long-standing open problem. © 1995.

authors

publication date

  • November 10, 1995

published in

Digital Object Identifier (DOI)

start page

  • 141

end page

  • 146

volume

  • 56

issue

  • 3