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
{"_id":"vQ3DdT6JXJxY2vPJt","bibbaseid":"milner-atheoryoftypepolymorphisminprogramming","authorIDs":[],"author_short":["Milner, R."],"bibdata":{"bibtype":"article","type":"article","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":[{"propositions":[],"lastnames":["Milner"],"firstnames":["Robin"],"suffixes":[]}],"file":"/home/dimitri/Nextcloud/Zotero/storage/ALDIBIYT/Milner - 1978 - A theory of type polymorphism in programming.pdf","bibtex":"@article{milnerTheoryTypePolymorphism1978,\n title = {A Theory of Type Polymorphism in Programming},\n volume = {17},\n issn = {10902724},\n doi = {10.1016/0022-0000(78)90014-4},\n 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.},\n number = {3},\n journaltitle = {Journal of Computer and System Sciences},\n date = {1978},\n pages = {348--375},\n author = {Milner, Robin},\n file = {/home/dimitri/Nextcloud/Zotero/storage/ALDIBIYT/Milner - 1978 - A theory of type polymorphism in programming.pdf}\n}\n\n","author_short":["Milner, R."],"key":"milnerTheoryTypePolymorphism1978","id":"milnerTheoryTypePolymorphism1978","bibbaseid":"milner-atheoryoftypepolymorphisminprogramming","role":"author","urls":{},"downloads":0},"bibtype":"article","biburl":"https://raw.githubusercontent.com/dlozeve/newblog/master/bib/all.bib","creationDate":"2020-01-08T20:39:39.054Z","downloads":0,"keywords":[],"search_terms":["theory","type","polymorphism","programming","milner"],"title":"A Theory of Type Polymorphism in Programming","year":null,"dataSources":["3XqdvqRE7zuX4cm8m"]}