A Theory of Type Polymorphism in Programming. Milner, R. 17(3):348–375.
doi  abstract   bibtex   
The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot "go wrong" and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system. ?? 1978.
@article{milnerTheoryTypePolymorphism1978,
  title = {A Theory of Type Polymorphism in Programming},
  volume = {17},
  issn = {10902724},
  doi = {10.1016/0022-0000(78)90014-4},
  abstract = {The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot "go wrong" and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system. ?? 1978.},
  number = {3},
  journaltitle = {Journal of Computer and System Sciences},
  date = {1978},
  pages = {348--375},
  author = {Milner, Robin},
  file = {/home/dimitri/Nextcloud/Zotero/storage/ALDIBIYT/Milner - 1978 - A theory of type polymorphism in programming.pdf}
}

Downloads: 0