A Theory of Type Polymorphism in Programming

Robin Milner, 1978, Journal of Computer and System Sciences

About this paperEnglishbeside English

This paper is under a licence that does not allow it to be reproduced, so what is here is its front matter and a short abstract. Read it at the publisher's page.

Trích dẫn cho phiên bản đã xuất bản:

Milner, R 1978, 'A theory of type polymorphism in programming', Journal of Computer and System Sciences, vol. 17, no. 3, pp. 348-375. https://doi.org/10.1016/0022-0000(78)90014-4

Mã định danh đối tượng số (DOI):

10.1016/0022-0000(78)90014-4

Liên kết:

Liên kết tới bản ghi xuất bản trong Edinburgh Research Explorer

Phiên bản tài liệu:

PDF của nhà xuất bản, còn được gọi là phiên bản chính thức

Được xuất bản trong:

Journal of Computer and System Sciences

Quyền chung

Bản quyền đối với các ấn phẩm được cung cấp thông qua Edinburgh Research Explorer thuộc về tác giả và / hoặc các chủ sở hữu bản quyền khác và là điều kiện để người dùng các ấn phẩm này công nhận và tuân thủ các yêu cầu pháp lý liên quan đến các quyền này.

Chính sách gỡ xuống

Đại học Edinburgh đã nỗ lực hợp lý để đảm bảo rằng Edinburgh Research Explorer tuân thủ luật pháp Vương quốc Anh. Nếu bạn tin rằng việc công khai tệp này vi phạm bản quyền, vui lòng liên hệ openaccess@ed.ac.uk và cung cấp chi tiết, chúng tôi sẽ gỡ quyền truy cập và điều tra vấn đề.

ROBIN MILNER

Khoa Khoa học Máy tính, Đại học Edinburgh, Edinburgh, Scotland

Nhận ngày 10 tháng 10 năm 1977; sửa đổi ngày 19 tháng 4 năm 1978

Mục tiêu của công trình này phần lớn mang tính thực tiễn. Một phong cách lập trình được sử dụng rộng rãi, đặc biệt trong các ngôn ngữ xử lý cấu trúc không áp đặt kỷ luật về kiểu, bao hàm việc định nghĩa các thủ tục hoạt động tốt trên các đối tượng thuộc nhiều loại khác nhau. Chúng tôi trình bày một kỷ luật kiểu hình thức cho các thủ tục đa hình như vậy trong ngữ cảnh của một ngôn ngữ lập trình đơn giản, cùng với một thuật toán kiểm tra kiểu tại thời điểm biên dịch W\mathcal{W} thực thi kỷ luật này.

References

  1. W. H. Burge, "Recursive Programming Techniques," Addison-Wesley, Reading, Mass., 1975.
  2. M. Gordon, R. Milner, and C. Wadsworth, "Edinburgh LCF," CSR-11-77, Computer Science Dept., Edinburgh University, 1977.
  3. M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth, A metalanguage for interactive proof in LCF, in "Proc. 5th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Tucson, Arizona, 1978."
  4. D. Gries and N. Gehani, Some ideas on data type in high-level languages, Comm. ACM. 20 (1977), 414–420.
  5. R. Hindley, The principal type-scheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969), 29–60.
  6. B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, and G. L. Popek, Report on the programming language Euclid, SIGPLAN Notices (ACM) 12, 2 (1977).
  7. P. J. Landin, The next 700 programming languages, Comm. ACM 9 (1966), 157–164.
  8. B. H. Liskov and S. Zilles, Programming with abstract data types, in “Proc. of ACM SIGPLAN conference on Very High Level Languages,” SIGPLAN Notices (ACM) 9 (1974), 50–59.
  9. R. Milner, “Models of LCF,” Mathematical Centre, Amsterdam, Tracts, Vol. 82, pp. 49–63, 1976.
  10. J. H. Morris, “Lambda-Calculus Models of Programming Languages,” Ph.D. Thesis, MAC-TR-57, MIT, 1968.
  11. G. Plotkin, A power-domain construction, SIAM J. Comput. 5 (1976), 452–487.
  12. J. C. Reynolds, “Towards a Theory of Type Structure,” Systems and Inform. Sci., Syracuse University, 1974.
  13. J. C. Reynolds, Syntactic control of interference, in “Proc. 5th ACM Symposium on Principles of Programming Languages, Tucson, Arizona, 1978,” pp. 39–46.
  14. J. A. Robinson, A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach. 12 (1965), 23–41.
  15. D. Scott, Lattice theoretic models for various type-free calculi, in “Proc. 4th International Congress for Logic, Methodology and Philosophy of Science, Bucharest, Rumania, 1972.”
  16. D. Scott and C. Strachey, Towards a mathematical semantics for computer languages, in “Proc. Symposium on Computers and Automata,” Vol. 21, Microwave Res. Inst. Symposia Series, Polytech. Inst. of Brooklyn, 1971.
  17. D. Scott, Data types as lattices, SIAM J. Comput. 5 (1976), 522–587.
  18. A. Shamir and W. Wadge, Data types as objects, in “Proc. 4th ICALP Conference, Turku, Finland, 1977.”
  19. C. Strachey, Fundamental concepts in programming languages, Notes for the International Summer School in Computer Programming, Copenhagen, 1967.
  20. R. D. Tennent, On a new approach to representation-independent data classes, Acta Inform. 8 (1977), 315–324.
  21. B. Wegbreit, The treatment of types in EL1, Comm. ACM 17 (1974), 251–264.
  22. A. van Wijngaarden et al., Revised report on the algorithmic language ALGOL 68, Acta Informatica 5 (1975), 1–236.
  23. R. A. Wulf, R. L. London, and M. Shaw, “Abstraction and Verification in ALPHARD: Introduction to Language and Methodology,” ISI/RR-76-46, Univ. of California, 1976.

Read off the page by a vision model reading the page images using olmOCR-2-7B-1025-FP8. Translated into Tiếng Việt by gpt-5, against glossary version 7. Translated from the English.