A theory of type polymorphism in programming
作者： Robin Milner
DOI: 10.1016/0022-0000(78)90014-4
关键词:
摘要: The aim of this work is largely a practical one. A widely employed style programming, particularly in structure-processing languages which impose no discipline types, entails defining procedures well on objects wide variety. We present formal type for such polymorphic the context simple programming language, and compile time type-checking algorithm w enforces discipline. Semantic Soundness Theorem (based semantics language) states that well-type programs cannot “go wrong” Syntactic if fl accepts program then it typed. also discuss extending these results to richer languages; based fact already implemented working, metalanguage ML Edinburgh LCF system,
core.ac.uk
ed.ac.uk
diku.dk
elsevier.com
uchicago.edu 参考文章(19)
William H. Burge, Recursive Programming Techniques ,(1975)
Wm. A. Wulf, Ralph L. London, Mary Shaw, Abstraction and Verification in Alphard: Introduction to Language and Methodology Springer, New York, NY. pp. 15- 60 ,(1976) , 10.1007/978-1-4612-5979-4_4
Robin Milner, Models of LCF. Mathematisch Centrum. pp. 49- 63 ,(1973) , 10.21236/AD0758645
John C. Reynolds, Towards a theory of type structure Programming Symposium, Proceedings Colloque sur la Programmation. pp. 408- 423 ,(1974) , 10.1007/3-540-06859-7_148
Adi Shamir, William W. Wadge, Data Types as Objects international colloquium on automata, languages and programming. pp. 465- 479 ,(1977) , 10.1007/3-540-08342-1_36
R. D. Tennent, On a new approach to representation independent data classes Acta Informatica. ,vol. 8, pp. 315- 324 ,(1977) , 10.1007/BF00271340
M. Gordon, R. Milner, L. Morris, M. Newey, C. Wadsworth, A Metalanguage for interactive proof in LCF Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '78. pp. 119- 130 ,(1978) , 10.1145/512760.512773
B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, G. J. Popek, Report on the programming language Euclid Sigplan Notices. ,vol. 12, pp. 1- 79 ,(1977) , 10.1145/954666.971189
R. Hindley, The Principal Type-Scheme of an Object in Combinatory Logic Transactions of the American Mathematical Society. ,vol. 146, pp. 29- 60 ,(1969) , 10.1090/S0002-9947-1969-0253905-6
David Gries, Narain Gehani, Some ideas on data types in high-level languages Communications of the ACM. ,vol. 20, pp. 414- 420 ,(1977) , 10.1145/359605.359624